- ::: now has support for second-order structure selection.

4 files changed, 104 insertions, 27 deletions

diff --git a/stdlib/source/lux/type.lux b/stdlib/source/lux/type.lux
index a721c0926..1fb0afa6f 100644
--- a/stdlib/source/lux/type.lux
+++ b/stdlib/source/lux/type.lux
@@ -25,15 +25,10 @@
     (^template [<tag>]
       (<tag> left right)
       (<tag> (beta-reduce env left) (beta-reduce env right)))
-    ([#;SumT] [#;ProdT])
+    ([#;SumT] [#;ProdT]
+     [#;LambdaT] [#;AppT])
     
     (^template [<tag>]
-      (<tag> left right)
-      (<tag> (beta-reduce env left) (beta-reduce env right)))
-    ([#;LambdaT]
-     [#;AppT])
-
-    (^template [<tag>]
       (<tag> old-env def)
       (case old-env
         #;Nil
@@ -45,11 +40,9 @@
      [#;ExQ])
     
     (#;BoundT idx)
-    (default type (list;at idx env))
+    (default (error! (Text/append "Unknown type var: " (Nat/encode idx)))
+      (list;at idx env))
     
-    (#;NamedT name type)
-    (beta-reduce env type)
-
     _
     type
     ))
diff --git a/stdlib/source/lux/type/auto.lux b/stdlib/source/lux/type/auto.lux
index aa7074d4a..d2b8cb1e5 100644
--- a/stdlib/source/lux/type/auto.lux
+++ b/stdlib/source/lux/type/auto.lux
@@ -171,6 +171,20 @@
     _
     (tc;fail (format "Invalid function type: " (%type func)))))
 
+(def: (concrete-type type)
+  (-> Type (Check [(List Nat) Type]))
+  (case type
+    (#;UnivQ _)
+    (do Monad<Check>
+      [[id var] tc;create-var
+       [ids final-output] (concrete-type (default (undefined)
+                                           (type;apply-type type var)))]
+      (wrap [(#;Cons id ids)
+             final-output]))
+    
+    _
+    (:: Monad<Check> wrap [(list) type])))
+
 (def: (check-apply member-type input-types output-type)
   (-> Type (List Type) Type (Check []))
   (do Monad<Check>
@@ -190,17 +204,16 @@
                       (set@ #tc;bindings (dict;from-list number;Hash<Nat> (get@ #;mappings type-vars))))]
       (#;Right [compiler context]))))
 
-(def: (test-alternatives sig-type member-idx input-types output-type alts)
-  (-> Type Nat (List Type) Type (List [Ident Type]) (Lux (List Ident)))
+(def: (test-provision context dep alts)
+  (-> tc;Context Type (List [Ident Type]) (Lux (List Ident)))
   (do Monad<Lux>
-    [context compiler-type-context]
+    [compiler compiler;get-compiler]
     (case (|> alts
               (list;filter (lambda [[alt-name alt-type]]
                              (case (tc;run context
                                            (do Monad<Check>
-                                             [_ (tc;check alt-type sig-type)
-                                              member-type (find-member-type member-idx alt-type)]
-                                             (check-apply member-type input-types output-type)))
+                                             [_ (tc;check dep alt-type)]
+                                             (wrap [])))
                                (#;Left error)
                                false
 
@@ -208,13 +221,69 @@
                                true)))
               (List/map product;left))
       #;Nil
-      (compiler;fail "No alternatives.")
+      (compiler;fail (format "No candidates for provisioning: " (%type dep)))
+
+      found
+      (wrap found))))
+
+(def: (provision compiler context dep)
+  (-> Compiler tc;Context Type (Check Ident))
+  (case (compiler;run compiler
+                      ($_ compiler;either
+                          (do Monad<Lux> [alts local-env] (test-provision context dep alts))
+                          (do Monad<Lux> [alts local-structs] (test-provision context dep alts))
+                          (do Monad<Lux> [alts import-structs] (test-provision context dep alts))))
+    (#;Left error)
+    (tc;fail error)
+
+    (#;Right candidates)
+    (case candidates
+      #;Nil
+      (tc;fail (format "No candidates for provisioning: " (%type dep)))
+
+      (#;Cons winner #;Nil)
+      (:: Monad<Check> wrap winner)
+
+      _
+      (tc;fail (format "Too many candidates for provisioning: " (%type dep) " --- " (%list %ident candidates))))
+    ))
+
+(def: (test-alternatives sig-type member-idx input-types output-type alts)
+  (-> Type Nat (List Type) Type (List [Ident Type]) (Lux (List [Ident (List Ident)])))
+  (do Monad<Lux>
+    [compiler compiler;get-compiler
+     context compiler-type-context]
+    (case (|> alts
+              (List/map (lambda [[alt-name alt-type]]
+                          (case (tc;run context
+                                        (do Monad<Check>
+                                          [[tvars alt-type] (concrete-type alt-type)
+                                           #let [[deps alt-type] (type;flatten-function alt-type)]
+                                           _ (tc;check alt-type sig-type)
+                                           member-type (find-member-type member-idx alt-type)
+                                           _ (check-apply member-type input-types output-type)
+                                           =tvars (mapM @ tc;deref tvars)
+                                           context' tc;get-context
+                                           =deps (mapM @ (provision compiler context') deps)]
+                                          (wrap =deps)))
+                            (#;Left error)
+                            (list)
+
+                            (#;Right =deps)
+                            (list [alt-name =deps]))))
+              List/join)
+      #;Nil
+      (compiler;fail (format "No alternatives."
+                             "\n"
+                             (|> alts
+                                 (List/map product;left)
+                                 (%list %ident))))
 
       found
       (wrap found))))
 
 (def: (find-alternatives sig-type member-idx input-types output-type)
-  (-> Type Nat (List Type) Type (Lux (List Ident)))
+  (-> Type Nat (List Type) Type (Lux (List [Ident (List Ident)])))
   (let [test (test-alternatives sig-type member-idx input-types output-type)]
     ($_ compiler;either
         (do Monad<Lux> [alts local-env] (test alts))
@@ -248,15 +317,21 @@
         #;Nil
         (compiler;fail (format "No structure option could be found for member: " (%ident member)))
 
-        (#;Cons chosen #;Nil)
-        (wrap (list (` (:: (~ (ast;symbol chosen))
-                           (~ (ast;local-symbol (product;right member)))
-                           (~@ (List/map ast;symbol args))))))
+        (#;Cons [chosen deps] #;Nil)
+        (let [chosen-inst (case deps
+                            #;Nil
+                            (ast;symbol chosen)
+
+                            _
+                            (` ((~ (ast;symbol chosen)) (~@ (List/map ast;symbol deps)))))]
+          (wrap (list (` (:: (~ chosen-inst)
+                             (~ (ast;local-symbol (product;right member)))
+                             (~@ (List/map ast;symbol args)))))))
 
         _
-        (compiler;fail (format "Too many available options: "
+        (compiler;fail (format "Too many options available: "
                                (|> chosen-ones
-                                   (List/map %ident)
+                                   (List/map (. %ident product;left))
                                    (text;join-with ", ")
                                    )))))
 
diff --git a/stdlib/source/lux/type/check.lux b/stdlib/source/lux/type/check.lux
index b9a1301bc..97a01d8ce 100644
--- a/stdlib/source/lux/type/check.lux
+++ b/stdlib/source/lux/type/check.lux
@@ -128,7 +128,7 @@
       #;None
       (#;Left (format "Unknown type-var: " (%n id))))))
 
-(def: (deref id)
+(def: #export (deref id)
   (-> Id (Check Type))
   (lambda [context]
     (case (|> context (get@ #bindings) (dict;get id))
@@ -516,3 +516,8 @@
 
     (#;Right _)
     true))
+
+(def: #export get-context
+  (Check Context)
+  (lambda [context]
+    (#;Right [context context])))
diff --git a/stdlib/test/test/lux/type/auto.lux b/stdlib/test/test/lux/type/auto.lux
index cb58514bf..f759827f0 100644
--- a/stdlib/test/test/lux/type/auto.lux
+++ b/stdlib/test/test/lux/type/auto.lux
@@ -32,5 +32,9 @@
                      (L/= (list;n.range +1 +10)
                           (::: map n.inc (list;n.range +0 +9)))
                      )))
-
+      
+      (assert "Can automatically select second-order structures."
+              (::: =
+                   (list;n.range +1 +10)
+                   (list;n.range +1 +10)))
       ))