- Updated tests for lux/type.

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

10 files changed, 427 insertions, 81 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)
    })
diff --git a/stdlib/test/test/lux/type.lux b/stdlib/test/test/lux/type.lux
index 8fa871e70..0e203f376 100644
--- a/stdlib/test/test/lux/type.lux
+++ b/stdlib/test/test/lux/type.lux
@@ -1,41 +1,137 @@
+##  Copyright (c) Eduardo Julian. All rights reserved.
+##  This Source Code Form is subject to the terms of the Mozilla Public License, v. 2.0.
+##  If a copy of the MPL was not distributed with this file,
+##  You can obtain one at http://mozilla.org/MPL/2.0/.
+
 (;module:
   lux
   (lux (codata [io])
        (control monad)
        (data [text "Text/" Monoid<Text>]
-             [number])
-       type
-       (codata function))
+             text/format
+             [number]
+             maybe
+             (struct [list]))
+       (math ["R" random])
+       pipe
+       ["&" type])
   lux/test)
 
-(test: "lux/type exports"
-  (let% [<eq-tests> (do-template [<type>]
-                      [(match true (:: Eq<Type> = <type> <type>))]
-
-                      [(#;HostT "java.util.List" (list Int))]
-                      [#;UnitT]
-                      [#;VoidT]
-                      [(#;VarT +123)]
-                      [(#;ExT +123)]
-                      [(#;BoundT +123)]
-                      [(#;LambdaT Bool Int)]
-                      [(#;AppT List Int)]
-                      [(#;NamedT ["" "Int-List"] (#;AppT List Int))]
-                      [(#;SumT Bool Int)]
-                      [(#;ProdT Bool Int)]
-                      [(#;UnivQ (list) (#;ProdT Bool (#;BoundT +1)))]
-                      [(#;ExQ (list) (#;ProdT Bool (#;BoundT +1)))]
-                      )]
-    (test-all <eq-tests>
-              (match (^=> (#;Some _type) (:: Eq<Type> = _type (#;ProdT Bool Int)))
-                     (apply-type (type (Meta Bool)) Int))
-              (match #;None (apply-type Text Bool))
-              (match true
-                     (:: Eq<Type> =
-                         (#;NamedT ["" "a"]
-                                   (#;ProdT Bool Int))
-                         (un-alias (#;NamedT ["" "c"]
-                                             (#;NamedT ["" "b"]
-                                                       (#;NamedT ["" "a"]
-                                                                 (#;ProdT Bool Int)))))))
-              )))
+## [Utils]
+(def: gen-name
+  (R;Random Text)
+  (do R;Monad<Random>
+    [size (|> R;nat (:: @ map (n.% +10)))]
+    (R;text size)))
+
+(def: gen-ident
+  (R;Random Ident)
+  (R;seq gen-name gen-name))
+
+(def: gen-type
+  (R;Random Type)
+  (let [(^open "R/") R;Monad<Random>]
+    (R;rec (lambda [gen-type]
+             ($_ R;alt
+                 (R;seq gen-name (R/wrap (list)))
+                 (R/wrap [])
+                 (R/wrap [])
+                 (R;seq gen-type gen-type)
+                 (R;seq gen-type gen-type)
+                 (R;seq gen-type gen-type)
+                 R;nat
+                 R;nat
+                 R;nat
+                 (R;seq (R/wrap (list)) gen-type)
+                 (R;seq (R/wrap (list)) gen-type)
+                 (R;seq gen-type gen-type)
+                 (R;seq gen-ident gen-type)
+                 )))))
+
+## [Tests]
+(test: "Types"
+  [sample gen-type]
+  (assert "Every type is equal to itself."
+          (:: &;Eq<Type> = sample sample)))
+
+(test: "Type application"
+  (assert "Can apply quantified types (universal and existential quantification)."
+          (and (default false
+                 (do Monad<Maybe>
+                   [partial (&;apply-type Meta Bool)
+                    full (&;apply-type partial Int)]
+                   (wrap (:: &;Eq<Type> = full (#;ProdT Bool Int)))))
+               (|> (&;apply-type Text Bool)
+                   (case> #;None true _ false)))))
+
+(test: "Naming"
+  (let [base (#;NamedT ["" "a"] (#;ProdT Bool Int))
+        aliased (#;NamedT ["" "c"]
+                          (#;NamedT ["" "b"]
+                                    base))]
+    ($_ seq
+        (assert "Can remove aliases from an already-named type."
+                (:: &;Eq<Type> =
+                    base
+                    (&;un-alias aliased)))
+
+        (assert "Can remove all names from a type."
+                (and (not (:: &;Eq<Type> =
+                              base
+                              (&;un-name aliased)))
+                     (:: &;Eq<Type> =
+                         (&;un-name base)
+                         (&;un-name aliased)))))))
+
+(test: "Type construction [structs]"
+  [size (|> R;nat (:: @ map (n.% +3)))
+   members (seqM @ (list;repeat size gen-type))
+   #let [(^open "&/") &;Eq<Type>
+         (^open "L/") (list;Eq<List> &;Eq<Type>)]]
+  (let% [<struct-tests> (do-template [<desc> <ctor> <dtor> <unit>]
+                          [(assert (format "Can build and tear-down " <desc> " types.")
+                                   (let [flat (|> members <ctor> <dtor>)]
+                                     (or (n.= (list;size members) (list;size flat))
+                                         (and (n.= +0 (list;size members))
+                                              (n.= +1 (list;size flat))
+                                              (|> flat list;head (default (undefined)) (&/= <unit>))))))]
+
+                          ["variant" &;variant &;flatten-variant #;VoidT]
+                          ["tuple"   &;tuple   &;flatten-tuple   #;UnitT]
+                          )]
+    ($_ seq
+        <struct-tests>
+        )))
+
+(test: "Type construction [parameterized]"
+  [size (|> R;nat (:: @ map (n.% +3)))
+   members (seqM @ (list;repeat size gen-type))
+   extra gen-type
+   #let [(^open "&/") &;Eq<Type>
+         (^open "L/") (list;Eq<List> &;Eq<Type>)]]
+  ($_ seq
+      (assert "Can build and tear-down function types."
+              (let [[inputs output] (|> (&;function members extra) &;flatten-function)]
+                (n.= (list;size members) (list;size inputs))))
+
+      (assert "Can build and tear-down application types."
+              (let [[tfunc tparams] (|> members (&;application extra) &;flatten-application)]
+                (n.= (list;size members) (list;size tparams))))
+      ))
+
+(test: "Type construction [higher order]"
+  [size (|> R;nat (:: @ map (n.% +3)))
+   extra gen-type
+   #let [(^open "&/") &;Eq<Type>]]
+  (let% [<quant-tests> (do-template [<desc> <ctor> <dtor>]
+                         [(assert (format "Can build and tear-down " <desc> " types.")
+                                  (let [[flat-size flat-body] (|> extra (<ctor> size) <dtor>)]
+                                    (and (n.= size flat-size)
+                                         (&/= extra flat-body))))]
+
+                         ["universally-quantified"   &;univq &;flatten-univq]
+                         ["existentially-quantified" &;exq   &;flatten-exq]
+                         )]
+    ($_ seq
+        <quant-tests>
+        )))
diff --git a/stdlib/test/test/lux/type/auto.lux b/stdlib/test/test/lux/type/auto.lux
new file mode 100644
index 000000000..ef69961cd
--- /dev/null
+++ b/stdlib/test/test/lux/type/auto.lux
@@ -0,0 +1,28 @@
+##  Copyright (c) Eduardo Julian. All rights reserved.
+##  This Source Code Form is subject to the terms of the Mozilla Public License, v. 2.0.
+##  If a copy of the MPL was not distributed with this file,
+##  You can obtain one at http://mozilla.org/MPL/2.0/.
+
+(;module:
+  lux
+  (lux (codata [io])
+       (control monad
+                [eq])
+       (data [text "Text/" Monoid<Text>]
+             text/format
+             [number]
+             [bool "B/" Eq<Bool>]
+             maybe
+             (struct [list]))
+       (math ["R" random])
+       pipe
+       [type]
+       type/auto)
+  lux/test)
+
+(test: "Automatic structure selection"
+  [x R;nat
+   y R;nat]
+  (assert "Can automatically select first-order structures."
+          (B/= (:: number;Eq<Nat> = x y)
+               (::: eq;= x y))))
diff --git a/stdlib/test/test/lux/type/check.lux b/stdlib/test/test/lux/type/check.lux
new file mode 100644
index 000000000..273dbad4c
--- /dev/null
+++ b/stdlib/test/test/lux/type/check.lux
@@ -0,0 +1,162 @@
+##  Copyright (c) Eduardo Julian. All rights reserved.
+##  This Source Code Form is subject to the terms of the Mozilla Public License, v. 2.0.
+##  If a copy of the MPL was not distributed with this file,
+##  You can obtain one at http://mozilla.org/MPL/2.0/.
+
+(;module:
+  lux
+  (lux (codata [io])
+       (control monad)
+       (data [text "Text/" Monoid<Text>]
+             text/format
+             [number]
+             maybe
+             (struct [list]))
+       (math ["R" random])
+       pipe
+       [type]
+       ["&" type/check])
+  lux/test)
+
+## [Utils]
+(def: gen-name
+  (R;Random Text)
+  (do R;Monad<Random>
+    [size (|> R;nat (:: @ map (n.% +10)))]
+    (R;text size)))
+
+(def: gen-ident
+  (R;Random Ident)
+  (R;seq gen-name gen-name))
+
+(def: gen-type
+  (R;Random Type)
+  (let [(^open "R/") R;Monad<Random>]
+    (R;rec (lambda [gen-type]
+             ($_ R;alt
+                 (R;seq gen-name (R/wrap (list)))
+                 (R/wrap [])
+                 (R/wrap [])
+                 (R;seq gen-type gen-type)
+                 (R;seq gen-type gen-type)
+                 (R;seq gen-type gen-type)
+                 R;nat
+                 R;nat
+                 R;nat
+                 (R;seq (R/wrap (list)) gen-type)
+                 (R;seq (R/wrap (list)) gen-type)
+                 (R;seq gen-type gen-type)
+                 (R;seq gen-ident gen-type)
+                 )))))
+
+(def: (type-checks? input)
+  (-> (&;Check []) Bool)
+  (case (&;run &;fresh-context input)
+    (#;Right [])
+    true
+
+    (#;Left error)
+    false))
+
+## [Tests]
+(test: "Top and Bottom"
+  [sample gen-type]
+  ($_ seq
+      (assert "Top is the super-type 0f everything."
+              (&;checks? Top sample))
+
+      (assert "Bottom is the sub-type 0f everything."
+              (&;checks? sample Bottom))
+      ))
+
+(test: "Simple type-checking."
+  ($_ seq
+      (assert "Unit and Void match themselves."
+              (and (&;checks? Void Void)
+                   (&;checks? Unit Unit)))
+
+      (assert "Existential types only match with themselves."
+              (and (type-checks? (do &;Monad<Check>
+                                   [[id ex] &;existential]
+                                   (&;check ex ex)))
+                   (not (type-checks? (do &;Monad<Check>
+                                        [[lid lex] &;existential
+                                         [rid rex] &;existential]
+                                        (&;check lex rex))))))
+
+      (assert "Names don't affect type-checking."
+              (and (type-checks? (do &;Monad<Check>
+                                   [[id ex] &;existential]
+                                   (&;check (#;NamedT ["module" "name"] ex)
+                                            ex)))
+                   (type-checks? (do &;Monad<Check>
+                                   [[id ex] &;existential]
+                                   (&;check ex
+                                            (#;NamedT ["module" "name"] ex))))
+                   (type-checks? (do &;Monad<Check>
+                                   [[id ex] &;existential]
+                                   (&;check (#;NamedT ["module" "name"] ex)
+                                            (#;NamedT ["module" "name"] ex))))))
+
+      (assert "Can type-check functions."
+              (and (&;checks? (#;LambdaT Bottom Top)
+                              (#;LambdaT Top Bottom))
+                   (not (&;checks? (#;LambdaT Top Bottom)
+                                   (#;LambdaT Bottom Top)))))
+      ))
+
+(test: "Type application"
+  [meta gen-type
+   data gen-type]
+  (assert "Can type-check type application."
+          (and (&;checks? (#;AppT (#;AppT Meta meta) data)
+                          (type;tuple (list meta data)))
+               (&;checks? (type;tuple (list meta data))
+                          (#;AppT (#;AppT Meta meta) data)))))
+
+(test: "Host types"
+  [nameL gen-name
+   nameR gen-name
+   paramL gen-type
+   paramR gen-type]
+  ($_ seq
+      (assert "Host types match when they have the same name and the same parameters."
+              (&;checks? (#;HostT nameL (list paramL))
+                         (#;HostT nameL (list paramL))))
+
+      (assert "Names matter to host types."
+              (&;checks? (#;HostT nameL (list paramL))
+                         (#;HostT nameR (list paramL))))
+
+      (assert "Parameters matter to host types."
+              (&;checks? (#;HostT nameL (list paramL))
+                         (#;HostT nameL (list paramR))))
+      ))
+
+(test: "Type-vars"
+  ($_ seq
+      (assert "Type-vars check against themselves."
+              (type-checks? (&;with-var (lambda [[id var]] (&;check var var)))))
+
+      (assert "Can bind unbound type-vars by type-checking against them."
+              (and (type-checks? (&;with-var (lambda [[id var]] (&;check var #;UnitT))))
+                   (type-checks? (&;with-var (lambda [[id var]] (&;check #;UnitT var))))))
+
+      (assert "Can't rebind already bound type-vars."
+              (not (type-checks? (&;with-var (lambda [[id var]]
+                                               (do &;Monad<Check>
+                                                 [_ (&;check var #;UnitT)]
+                                                 (&;check var #;VoidT)))))))
+
+      (assert "If the type bound to a var is a super-type to another, then the var is also a super-type."
+              (type-checks? (&;with-var (lambda [[id var]]
+                                          (do &;Monad<Check>
+                                            [_ (&;check var Top)]
+                                            (&;check var #;UnitT))))))
+
+      (assert "If the type bound to a var is a sub-type of another, then the var is also a sub-type."
+              (type-checks? (&;with-var (lambda [[id var]]
+                                          (do &;Monad<Check>
+                                            [_ (&;check var Bottom)]
+                                            (&;check #;UnitT var))))))
+      ))
diff --git a/stdlib/test/tests.lux b/stdlib/test/tests.lux
index e225e1f28..ef94dca90 100644
--- a/stdlib/test/tests.lux
+++ b/stdlib/test/tests.lux
@@ -59,17 +59,17 @@
              (macro ["_;" ast]
                     ["_;" syntax]
                     ["_;" template])
-             ## [type]
-             ## (type [check] [auto])
-             ## (control ...)
+             ["_;" type]
+             (type ["_;" check]
+                   ["_;" auto])
+             ## (control [effect])
              )
         )
   ## (lux (codata [cont])
-  ## (macro [poly]
-  ##        (poly ["poly_;" eq]
-  ##              ["poly_;" text-encoder]
-  ##              ["poly_;" functor]))
-  ##      (control [effect]))
+  ##      (macro [poly]
+  ##             (poly ["poly_;" eq]
+  ##                   ["poly_;" text-encoder]
+  ##                   ["poly_;" functor])))
   )
 
 ## [Program]