- Updated tests for lux/type.

- Added tests for lux/type/check and lux/type/auto.

6 files changed, 99 insertions, 39 deletions

diff --git a/stdlib/source/lux.lux b/stdlib/source/lux.lux
index de985db95..b834649e8 100644
--- a/stdlib/source/lux.lux
+++ b/stdlib/source/lux.lux
@@ -3254,8 +3254,8 @@
        _
        (list type)))]
 
-  [flatten-sum  #;SumT]
-  [flatten-prod #;ProdT]
+  [flatten-variant  #;SumT]
+  [flatten-tuple #;ProdT]
   [flatten-lambda    #;LambdaT]
   [flatten-app  #;AppT]
   )
@@ -3264,7 +3264,7 @@
   (-> Type (Maybe (List Type)))
   (case type
     (#ProdT _)
-    (#Some (flatten-prod type))
+    (#Some (flatten-tuple type))
 
     (#AppT fun arg)
     (do Monad<Maybe>
@@ -4059,10 +4059,10 @@
     "Unit"
 
     (#SumT _)
-    ($_ Text/append "(| " (|> (flatten-sum type) (map Type/show) (interpose " ") reverse (fold Text/append "")) ")")
+    ($_ Text/append "(| " (|> (flatten-variant type) (map Type/show) (interpose " ") reverse (fold Text/append "")) ")")
     
     (#ProdT _)
-    ($_ Text/append "[" (|> (flatten-prod type) (map Type/show) (interpose " ") reverse (fold Text/append "")) "]")
+    ($_ Text/append "[" (|> (flatten-tuple type) (map Type/show) (interpose " ") reverse (fold Text/append "")) "]")
 
     (#LambdaT _)
     ($_ Text/append "(-> " (|> (flatten-lambda type) (map Type/show) (interpose " ") reverse (fold Text/append "")) ")")
diff --git a/stdlib/source/lux/control/effect.lux b/stdlib/source/lux/control/effect.lux
index 16605e1c7..379a28d76 100644
--- a/stdlib/source/lux/control/effect.lux
+++ b/stdlib/source/lux/control/effect.lux
@@ -300,7 +300,7 @@
                            (if (tc;checks? (clean-effect effect) eff0)
                              (#;Some idx)
                              #;None))
-                         (|> unfoldT1 type;flatten-sum (List/map un-apply) list;enumerate))
+                         (|> unfoldT1 type;flatten-variant (List/map un-apply) list;enumerate))
               (#;Some idx)])
         (wrap (list (` (#;;Effect (:: (~ g!functor) (~' map) (~' wrap) ((~ (ast;int (nat-to-int idx)))
                                                                         (~ (ast;symbol var))))))))
diff --git a/stdlib/source/lux/macro/poly.lux b/stdlib/source/lux/macro/poly.lux
index 0973eece6..8c3a5b288 100644
--- a/stdlib/source/lux/macro/poly.lux
+++ b/stdlib/source/lux/macro/poly.lux
@@ -91,8 +91,8 @@
            (:: compiler;Monad<Lux> wrap members)
            (compiler;fail (format "Not a " ($AST$ <tag>) " type: " (%type :type:)))))))]
 
-  [sum    sum+    type;flatten-sum      #;SumT]
-  [prod   prod+   type;flatten-prod     #;ProdT]
+  [sum    sum+    type;flatten-variant #;SumT]
+  [prod   prod+   type;flatten-tuple   #;ProdT]
   )
 
 (def: #export func
diff --git a/stdlib/source/lux/type.lux b/stdlib/source/lux/type.lux
index c16c8217b..91b44bfd8 100644
--- a/stdlib/source/lux/type.lux
+++ b/stdlib/source/lux/type.lux
@@ -128,11 +128,11 @@
     _
     [(list) type]))
 
-(def: #export (flatten-apply type)
+(def: #export (flatten-application type)
   (-> Type [Type (List Type)])
   (case type
     (#;AppT left' right)
-    (let [[left rights] (flatten-apply left')]
+    (let [[left rights] (flatten-application left')]
       [left (List/append rights (list right))])
 
     _
@@ -148,8 +148,8 @@
        _
        (list type)))]
 
-  [flatten-sum  #;SumT]
-  [flatten-prod #;ProdT]
+  [flatten-variant #;SumT]
+  [flatten-tuple   #;ProdT]
   )
 
 (def: #export (apply-type type-fun param)
@@ -197,8 +197,8 @@
     (^template [<tag> <macro> <flattener>]
       (<tag> left right)
       (` (<macro> (~@ (List/map to-ast (<flattener> type))))))
-    ([#;SumT  | flatten-sum]
-     [#;ProdT & flatten-prod])
+    ([#;SumT  | flatten-variant]
+     [#;ProdT & flatten-tuple])
 
     (#;NamedT name sub-type)
     (ast;symbol name)
@@ -236,8 +236,8 @@
               (list;interpose " ")
               (List/fold Text/append ""))
           <close>))
-    ([#;SumT  "(| " ")" flatten-sum]
-     [#;ProdT "["   "]" flatten-prod])
+    ([#;SumT  "(| " ")" flatten-variant]
+     [#;ProdT "["   "]" flatten-tuple])
 
     (#;LambdaT input output)
     (let [[ins out] (flatten-function type)]
@@ -259,7 +259,7 @@
     ($_ Text/append "⟨e:" (Nat/encode id) "⟩")
 
     (#;AppT fun param)
-    (let [[type-fun type-args] (flatten-apply type)]
+    (let [[type-fun type-args] (flatten-application type)]
       ($_ Text/append  "(" (to-text type-fun) " " (|> type-args (List/map to-text) list;reverse (list;interpose " ") (List/fold Text/append "")) ")"))
 
     (#;UnivQ env body)
@@ -306,3 +306,32 @@
   [variant Void #;SumT]
   [tuple   Unit #;ProdT]
   )
+
+(def: #export (function inputs output)
+  (-> (List Type) Type Type)
+  (case inputs
+    #;Nil
+    output
+
+    (#;Cons input inputs')
+    (#;LambdaT input (function inputs' output))))
+
+(def: #export (application quant params)
+  (-> Type (List Type) Type)
+  (case params
+    #;Nil
+    quant
+
+    (#;Cons param params')
+    (application (#;AppT quant param) params')))
+
+(do-template [<name> <tag>]
+  [(def: #export (<name> size body)
+     (-> Nat Type Type)
+     (case size
+       +0 body
+       _  (<tag> (list) (<name> (n.dec size) body))))]
+
+  [univq #;UnivQ]
+  [exq   #;ExQ]
+  )
diff --git a/stdlib/source/lux/type/auto.lux b/stdlib/source/lux/type/auto.lux
index f33314ac1..c22434e9f 100644
--- a/stdlib/source/lux/type/auto.lux
+++ b/stdlib/source/lux/type/auto.lux
@@ -20,6 +20,37 @@
        (type ["tc" check #+ Check Monad<Check>])
        ))
 
+(def: (find-type-var id env)
+  (-> Nat (Bindings Nat (Maybe Type)) (Lux Type))
+  (case (list;find (|>. product;left (n.= id))
+                   (get@ #;mappings env))
+    (#;Some [_ (#;Some type)])
+    (case type
+      (#;VarT id')
+      (find-type-var id' env)
+
+      _
+      (:: Monad<Lux> wrap type))
+
+    (#;Some [_ #;None])
+    (compiler;fail (format "Unbound type-var " (%n id)))
+
+    #;None
+    (compiler;fail (format "Unknown type-var " (%n id)))
+    ))
+
+(def: (resolve-type var-name)
+  (-> Ident (Lux Type))
+  (do Monad<Lux>
+    [raw-type (compiler;find-type var-name)
+     compiler compiler;get-compiler]
+    (case raw-type
+      (#;VarT id)
+      (find-type-var id (get@ #;type-vars compiler))
+
+      _
+      (wrap raw-type))))
+
 (def: (find-member-type idx sig-type)
   (-> Nat Type (Check Type))
   (case sig-type
@@ -84,8 +115,12 @@
   (do Monad<Lux>
     [this-module-name compiler;current-module-name
      imp-mods (compiler;imported-modules this-module-name)
-     export-batches (mapM @ compiler;exports imp-mods)]
-    (wrap (prepare-defs this-module-name (List/join export-batches)))))
+     export-batches (mapM @ (lambda [imp-mod]
+                              (do @
+                                [exports (compiler;exports imp-mod)]
+                                (wrap (prepare-defs imp-mod exports))))
+                          imp-mods)]
+    (wrap (List/join export-batches))))
 
 (def: (apply-function-type func arg)
   (-> Type Type (Check Type))
@@ -123,7 +158,7 @@
   (lambda [compiler]
     (let [type-vars (get@ #;type-vars compiler)
           context (|> tc;fresh-context
-                      (set@ #tc;var-id (get@ #;counter type-vars))
+                      (set@ #tc;var-counter (get@ #;counter type-vars))
                       (set@ #tc;bindings (dict;from-list number;Hash<Nat> (get@ #;mappings type-vars))))]
       (#;Right [compiler context]))))
 
@@ -135,7 +170,7 @@
               (list;filter (lambda [[alt-name alt-type]]
                              (case (tc;run context
                                            (do Monad<Check>
-                                             [_ (tc;check sig-type 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)))
                                (#;Left error)
@@ -171,23 +206,23 @@
   (All [a] (-> [a a] (List a)))
   (list l r))
 
-(syntax: #export (::: {member s;symbol}
-                      {args (s;alt (s;some s;symbol)
-                                   (s;some s;any))})
+(syntax: #export (::: [member s;symbol]
+                      [args (s;alt (s;some s;symbol)
+                                   (s;some s;any))])
   (case args
     (#;Left args)
     (do @
       [[member-idx sig-type] (resolve-member member)
-       input-types (mapM @ compiler;find-type args)
+       input-types (mapM @ resolve-type args)
        output-type compiler;expected-type
        chosen-ones (find-alternatives sig-type member-idx input-types output-type)]
       (case chosen-ones
         #;Nil
-        (compiler;fail (format "No structure option could be found for member " (%ident member)))
+        (compiler;fail (format "No structure option could be found for member: " (%ident member)))
 
         (#;Cons chosen #;Nil)
         (wrap (list (` (:: (~ (ast;symbol chosen))
-                           (~ (ast;symbol member))
+                           (~ (ast;local-symbol (product;right member)))
                            (~@ (List/map ast;symbol args))))))
 
         _
@@ -205,7 +240,3 @@
        #let [retry (` (let [(~@ (|> (list;zip2 labels args-to-bind) (List/map join-pair) List/join))]
                         (;;::: (~ (ast;symbol member)) (~@ labels))))]]
       (wrap (list retry)))))
-
-(comment
-  (::: map i.inc (list 0 1 2 3 4))
-  )
diff --git a/stdlib/source/lux/type/check.lux b/stdlib/source/lux/type/check.lux
index 951586bb0..b9a1301bc 100644
--- a/stdlib/source/lux/type/check.lux
+++ b/stdlib/source/lux/type/check.lux
@@ -24,8 +24,8 @@
 (type: #export Fixpoints (List [[Type Type] Bool]))
 
 (type: #export Context
-  {#var-id Id
-   #ex-id Id
+  {#var-counter Id
+   #ex-counter Id
    #bindings (dict;Dict Id (Maybe Type))
    #fixpoints Fixpoints
    })
@@ -111,8 +111,8 @@
 (def: #export existential
   (Check [Id Type])
   (lambda [context]
-    (let [id (get@ #ex-id context)]
-      (#;Right [(update@ #ex-id n.inc context)
+    (let [id (get@ #ex-counter context)]
+      (#;Right [(update@ #ex-counter n.inc context)
                 [id (#;ExT id)]]))))
 
 (def: (bound? id)
@@ -241,9 +241,9 @@
 (def: #export create-var
   (Check [Id Type])
   (lambda [context]
-    (let [id (get@ #var-id context)]
+    (let [id (get@ #var-counter context)]
       (#;Right [(|> context
-                    (update@ #var-id n.inc)
+                    (update@ #var-counter n.inc)
                     (update@ #bindings (dict;put id #;None)))
                 [id (#;VarT id)]]))))
 
@@ -307,8 +307,8 @@
 
 (def: #export fresh-context
   Context
-  {#var-id +0
-   #ex-id +0
+  {#var-counter +0
+   #ex-counter +0
    #bindings (dict;new number;Hash<Nat>)
    #fixpoints (list)
    })