Ported tests for type-related modules.

7 files changed, 452 insertions, 450 deletions

diff --git a/stdlib/source/test/lux.lux b/stdlib/source/test/lux.lux
index f50cdf48a..191a664ce 100644
--- a/stdlib/source/test/lux.lux
+++ b/stdlib/source/test/lux.lux
@@ -118,17 +118,13 @@
      ["#." macro]
      ["#." math]
      ["#." time]
+     ["#." type]
      ["#." host
       ["#/." jvm]]]
     ## [control
     ##  [concurrency
     ##   ## [semaphore (#+)]
     ##   ]]
-    ## [type ## (#+)
-    ##  ## [check (#+)]
-    ##  ## [implicit (#+)] ## TODO: FIX Specially troublesome...
-    ##  ## [resource (#+)]
-    ##  [dynamic (#+)]]
     ## [compiler
     ##  [default
     ##   ["_default/." syntax]
@@ -376,6 +372,8 @@
           /math.test)
       (<| (_.context "/time")
           /time.test)
+      (<| (_.context "/type")
+          /type.test)
       (<| (_.context "/host Host-platform interoperation")
           ($_ _.and
               /host.test
@@ -384,5 +382,7 @@
       ))
 
 (program: args
-  (io (_.run! (<| (_.times 100)
-                  ..test))))
+  (<| io
+      _.run!
+      (_.times 100)
+      ..test))
diff --git a/stdlib/source/test/lux/macro/poly/equivalence.lux b/stdlib/source/test/lux/macro/poly/equivalence.lux
index 941eb881f..41ae1ecd0 100644
--- a/stdlib/source/test/lux/macro/poly/equivalence.lux
+++ b/stdlib/source/test/lux/macro/poly/equivalence.lux
@@ -1,9 +1,9 @@
 (.module:
   [lux #*
    data/text/format
-   [control/monad (#+ do)]
    ["r" math/random (#+ Random)]
    ["_" test (#+ Test)]
+   [control ["." monad (#+ do)]]
    [control
     [equivalence (#+ Equivalence)]]
    [data
diff --git a/stdlib/source/test/lux/type.lux b/stdlib/source/test/lux/type.lux
index 7f5d76730..1fcc7e3e9 100644
--- a/stdlib/source/test/lux/type.lux
+++ b/stdlib/source/test/lux/type.lux
@@ -1,39 +1,42 @@
 (.module:
-  [lux #*
+  [lux (#- type)
+   data/text/format
+   ["M" control/monad (#+ do)]
+   ["r" math/random (#+ Random)]
+   ["_" test (#+ Test)]
    [control
-    ["M" monad (#+ do Monad)]
     pipe]
    [data
     ["." maybe]
-    [text
-     format]
     [collection
-     ["." list]]]
-   [math
-    ["r" random]]
-   ["&" type]]
-  lux/test)
-
-## [Utils]
-(def: #export gen-short
+     ["." list]]]]
+  {1
+   ["." / ("#@." equivalence)]}
+  ["." / #_
+   ["#." check]
+   ["#." dynamic]
+   ["#." implicit]
+   ["#." resource]])
+
+(def: short
   (r.Random Text)
   (do r.monad
     [size (|> r.nat (:: @ map (n/% 10)))]
     (r.unicode size)))
 
-(def: #export gen-name
+(def: name
   (r.Random Name)
-  (r.and gen-short gen-short))
+  (r.and ..short ..short))
 
-(def: #export gen-type
+(def: #export type
   (r.Random Type)
-  (let [(^open "R;.") r.monad]
-    (r.rec (function (_ gen-type)
-             (let [pairG (r.and gen-type gen-type)
+  (let [(^open "R@.") r.monad]
+    (r.rec (function (_ recur)
+             (let [pairG (r.and recur recur)
                    idG r.nat
-                   quantifiedG (r.and (R;wrap (list)) gen-type)]
+                   quantifiedG (r.and (R@wrap (list)) recur)]
                ($_ r.or
-                   (r.and gen-short (R;wrap (list)))
+                   (r.and ..short (R@wrap (list)))
                    pairG
                    pairG
                    pairG
@@ -43,136 +46,122 @@
                    quantifiedG
                    quantifiedG
                    pairG
-                   (r.and gen-name gen-type)
+                   (r.and ..name recur)
                    ))))))
 
-## [Tests]
-(context: "Types"
-  (<| (times 100)
-      (do @
-        [sample gen-type]
-        (test "Every type is equal to itself."
-              (:: &.equivalence = sample sample)))))
-
-(context: "Type application"
-  (test "Can apply quantified types (universal and existential quantification)."
-        (and (maybe.default #0
-                            (do maybe.monad
-                              [partial (&.apply (list Bit) Ann)
-                               full (&.apply (list Int) partial)]
-                              (wrap (:: &.equivalence = full (#.Product Bit Int)))))
-             (|> (&.apply (list Bit) Text)
-                 (case> #.None #1 _ #0)))))
-
-(context: "Naming"
-  (let [base (#.Named ["" "a"] (#.Product Bit Int))
-        aliased (#.Named ["" "c"]
-                         (#.Named ["" "b"]
-                                  base))]
-    ($_ seq
-        (test "Can remove aliases from an already-named type."
-              (:: &.equivalence =
-                  base
-                  (&.un-alias aliased)))
-
-        (test "Can remove all names from a type."
-              (and (not (:: &.equivalence =
+(def: #export test
+  Test
+  (<| (_.context (%name (name-of /._)))
+      ($_ _.and
+          (do r.monad
+            [sample ..type]
+            (_.test "Every type is equal to itself."
+                    (:: /.equivalence = sample sample)))
+          (_.test "Can apply quantified types (universal and existential quantification)."
+                  (and (maybe.default #0
+                                      (do maybe.monad
+                                        [partial (/.apply (list Bit) Ann)
+                                         full (/.apply (list Int) partial)]
+                                        (wrap (:: /.equivalence = full (#.Product Bit Int)))))
+                       (|> (/.apply (list Bit) Text)
+                           (case> #.None #1 _ #0))))
+          (let [base (#.Named ["" "a"] (#.Product Bit Int))
+                aliased (#.Named ["" "c"]
+                                 (#.Named ["" "b"]
+                                          base))]
+            ($_ _.and
+                (_.test "Can remove aliases from an already-named type."
+                        (:: /.equivalence =
                             base
-                            (&.un-name aliased)))
-                   (:: &.equivalence =
-                       (&.un-name base)
-                       (&.un-name aliased)))))))
-
-(context: "Type construction [structs]"
-  (<| (times 100)
-      (do @
-        [size (|> r.nat (:: @ map (n/% 3)))
-         members (|> gen-type
-                     (r.filter (function (_ type)
-                                 (case type
-                                   (^or (#.Sum _) (#.Product _))
-                                   #0
-
-                                   _
-                                   #1)))
-                     (list.repeat size)
-                     (M.seq @))
-         #let [(^open "&;.") &.equivalence
-               (^open "L;.") (list.equivalence &.equivalence)]]
-        (with-expansions
-          [<struct-tests> (do-template [<desc> <ctor> <dtor> <unit>]
-                            [(test (format "Can build and tear-down " <desc> " types.")
+                            (/.un-alias aliased)))
+                (_.test "Can remove all names from a type."
+                        (and (not (:: /.equivalence =
+                                      base
+                                      (/.un-name aliased)))
+                             (:: /.equivalence =
+                                 (/.un-name base)
+                                 (/.un-name aliased))))))
+          (do r.monad
+            [size (|> r.nat (:: @ map (n/% 3)))
+             members (|> ..type
+                         (r.filter (function (_ type)
+                                     (case type
+                                       (^or (#.Sum _) (#.Product _))
+                                       #0
+
+                                       _
+                                       #1)))
+                         (list.repeat size)
+                         (M.seq @))
+             #let [(^open "/@.") /.equivalence
+                   (^open "list@.") (list.equivalence /.equivalence)]]
+            (`` ($_ _.and
+                    (~~ (do-template [<desc> <ctor> <dtor> <unit>]
+                          [(_.test (format "Can build and tear-down " <desc> " types.")
                                    (let [flat (|> members <ctor> <dtor>)]
-                                     (or (L;= members flat)
-                                         (and (L;= (list) members)
-                                              (L;= (list <unit>) flat)))))]
-
-                            ["variant" &.variant &.flatten-variant Nothing]
-                            ["tuple"   &.tuple   &.flatten-tuple   Any]
-                            )]
-          ($_ seq
-              <struct-tests>
-              )))))
-
-(context: "Type construction [parameterized]"
-  (<| (times 100)
-      (do @
-        [size (|> r.nat (:: @ map (n/% 3)))
-         members (M.seq @ (list.repeat size gen-type))
-         extra (|> gen-type
-                   (r.filter (function (_ type)
-                               (case type
-                                 (^or (#.Function _) (#.Apply _))
-                                 #0
-
-                                 _
-                                 #1))))
-         #let [(^open "&;.") &.equivalence
-               (^open "L;.") (list.equivalence &.equivalence)]]
-        ($_ seq
-            (test "Can build and tear-down function types."
-                  (let [[inputs output] (|> (&.function members extra) &.flatten-function)]
-                    (and (L;= members inputs)
-                         (&;= extra output))))
-
-            (test "Can build and tear-down application types."
-                  (let [[tfunc tparams] (|> extra (&.application members) &.flatten-application)]
-                    (n/= (list.size members) (list.size tparams))))
-            ))))
-
-(context: "Type construction [higher order]"
-  (<| (times 100)
-      (do @
-        [size (|> r.nat (:: @ map (n/% 3)))
-         extra (|> gen-type
-                   (r.filter (function (_ type)
-                               (case type
-                                 (^or (#.UnivQ _) (#.ExQ _))
-                                 #0
-
-                                 _
-                                 #1))))
-         #let [(^open "&;.") &.equivalence]]
-        (with-expansions
-          [<quant-tests> (do-template [<desc> <ctor> <dtor>]
-                           [(test (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"   &.univ-q &.flatten-univ-q]
-                           ["existentially-quantified" &.ex-q   &.flatten-ex-q]
-                           )]
-          ($_ seq
-              <quant-tests>
-              )))))
-
-(def: extraction
-  Test
-  (_.test "Can extract types."
-          (let [example (: (Maybe Nat)
-                           #.Nonae)]
-            (type;= (type (List Nat))
-                    (:by-example [a]
-                                 {(Maybe a) example}
-                                 (List a))))))
+                                     (or (list@= members flat)
+                                         (and (list@= (list) members)
+                                              (list@= (list <unit>) flat)))))]
+
+                          ["variant" /.variant /.flatten-variant Nothing]
+                          ["tuple"   /.tuple   /.flatten-tuple   Any]
+                          ))
+                    )))
+          (do r.monad
+            [size (|> r.nat (:: @ map (n/% 3)))
+             members (M.seq @ (list.repeat size ..type))
+             extra (|> ..type
+                       (r.filter (function (_ type)
+                                   (case type
+                                     (^or (#.Function _) (#.Apply _))
+                                     #0
+
+                                     _
+                                     #1))))
+             #let [(^open "/@.") /.equivalence
+                   (^open "list@.") (list.equivalence /.equivalence)]]
+            ($_ _.and
+                (_.test "Can build and tear-down function types."
+                        (let [[inputs output] (|> (/.function members extra) /.flatten-function)]
+                          (and (list@= members inputs)
+                               (/@= extra output))))
+
+                (_.test "Can build and tear-down application types."
+                        (let [[tfunc tparams] (|> extra (/.application members) /.flatten-application)]
+                          (n/= (list.size members) (list.size tparams))))
+                ))
+          (do r.monad
+            [size (|> r.nat (:: @ map (n/% 3)))
+             extra (|> ..type
+                       (r.filter (function (_ type)
+                                   (case type
+                                     (^or (#.UnivQ _) (#.ExQ _))
+                                     #0
+
+                                     _
+                                     #1))))
+             #let [(^open "/@.") /.equivalence]]
+            (`` ($_ _.and
+                    (~~ (do-template [<desc> <ctor> <dtor>]
+                          [(_.test (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"   /.univ-q /.flatten-univ-q]
+                          ["existentially-quantified" /.ex-q   /.flatten-ex-q]
+                          ))
+                    )))
+          (_.test (%name (name-of /.:by-example))
+                  (let [example (: (Maybe Nat)
+                                   #.None)]
+                    (/@= (.type (List Nat))
+                         (/.:by-example [a]
+                                        {(Maybe a) example}
+                                        (List a)))))
+
+          /check.test
+          /dynamic.test
+          /implicit.test
+          /resource.test
+          )))
diff --git a/stdlib/source/test/lux/type/check.lux b/stdlib/source/test/lux/type/check.lux
index 45f1ce821..d73b2783d 100644
--- a/stdlib/source/test/lux/type/check.lux
+++ b/stdlib/source/test/lux/type/check.lux
@@ -1,24 +1,54 @@
 (.module:
-  [lux #*
+  [lux (#- type)
+   data/text/format
+   [control ["." monad (#+ do)]]
+   ["r" math/random (#+ Random)]
+   ["_" test (#+ Test)]
    [control
-    ["." monad (#+ do Monad)]
     [pipe (#+ case>)]]
    [data
     ["." product]
     ["." maybe]
-    ["." number]
-    ["." text ("#;." equivalence)]
+    ["." text ("#@." equivalence)]
+    [number
+     ["." nat]]
     [collection
-     ["." list ("#;." functor)]
+     ["." list ("#@." functor)]
      ["." set]]]
-   [math
-    ["r" random]]
-   ["." type ("#;." equivalence)
-    ["@" check]]]
-  lux/test
-  ["." //])
+   ["." type ("#@." equivalence)]]
+  {1
+   ["." /]})
+
+## TODO: Remove the following 3 definitions ASAP. //.type already exists...
+(def: short
+  (r.Random Text)
+  (r.unicode 10))
+
+(def: name
+  (r.Random Name)
+  (r.and ..short ..short))
+
+(def: type
+  (r.Random Type)
+  (let [(^open "R@.") r.monad]
+    (r.rec (function (_ recur)
+             (let [pairG (r.and recur recur)
+                   idG r.nat
+                   quantifiedG (r.and (R@wrap (list)) recur)]
+               ($_ r.or
+                   (r.and ..short (R@wrap (list)))
+                   pairG
+                   pairG
+                   pairG
+                   idG
+                   idG
+                   idG
+                   quantifiedG
+                   quantifiedG
+                   pairG
+                   (r.and ..name recur)
+                   ))))))
 
-## [Utils]
 (def: (valid-type? type)
   (-> Type Bit)
   (case type
@@ -40,198 +70,177 @@
     #0))
 
 (def: (type-checks? input)
-  (-> (@.Check []) Bit)
-  (case (@.run @.fresh-context input)
+  (-> (/.Check []) Bit)
+  (case (/.run /.fresh-context input)
     (#.Right [])
     #1
 
     (#.Left error)
     #0))
 
-## [Tests]
-(context: "Any and Nothing."
-  (<| (times 100)
-      (do @
-        [sample (|> //.gen-type (r.filter valid-type?))]
-        ($_ seq
-            (test "Any is the super-type of everything."
-                  (@.checks? Any sample))
-
-            (test "Nothing is the sub-type of everything."
-                  (@.checks? sample Nothing))
-            ))))
-
-(context: "Simple type-checking."
-  ($_ seq
-      (test "Any and Nothing match themselves."
-            (and (@.checks? Nothing Nothing)
-                 (@.checks? Any Any)))
-
-      (test "Existential types only match with themselves."
-            (and (type-checks? (do @.monad
-                                 [[_ exT] @.existential]
-                                 (@.check exT exT)))
-                 (not (type-checks? (do @.monad
-                                      [[_ exTL] @.existential
-                                       [_ exTR] @.existential]
-                                      (@.check exTL exTR))))))
-
-      (test "Names do not affect type-checking."
-            (and (type-checks? (do @.monad
-                                 [[_ exT] @.existential]
-                                 (@.check (#.Named ["module" "name"] exT)
-                                          exT)))
-                 (type-checks? (do @.monad
-                                 [[_ exT] @.existential]
-                                 (@.check exT
-                                          (#.Named ["module" "name"] exT))))
-                 (type-checks? (do @.monad
-                                 [[_ exT] @.existential]
-                                 (@.check (#.Named ["module" "name"] exT)
-                                          (#.Named ["module" "name"] exT))))))
-
-      (test "Functions are covariant on inputs and contravariant on outputs."
-            (and (@.checks? (#.Function Nothing Any)
-                            (#.Function Any Nothing))
-                 (not (@.checks? (#.Function Any Nothing)
-                                 (#.Function Nothing Any)))))
-      ))
-
-(context: "Type application."
-  (<| (times 100)
-      (do @
-        [meta //.gen-type
-         data //.gen-type]
-        (test "Can type-check type application."
-              (and (@.checks? (|> Ann (#.Apply meta) (#.Apply data))
-                              (type.tuple (list meta data)))
-                   (@.checks? (type.tuple (list meta data))
-                              (|> Ann (#.Apply meta) (#.Apply data))))))))
-
-(context: "Primitive types."
-  (<| (times 100)
-      (do @
-        [nameL //.gen-short
-         nameR (|> //.gen-short (r.filter (|>> (text;= nameL) not)))
-         paramL //.gen-type
-         paramR (|> //.gen-type (r.filter (|>> (@.checks? paramL) not)))]
-        ($_ seq
-            (test "Primitive types match when they have the same name and the same parameters."
-                  (@.checks? (#.Primitive nameL (list paramL))
-                             (#.Primitive nameL (list paramL))))
-
-            (test "Names matter to primitive types."
-                  (not (@.checks? (#.Primitive nameL (list paramL))
-                                  (#.Primitive nameR (list paramL)))))
-
-            (test "Parameters matter to primitive types."
-                  (not (@.checks? (#.Primitive nameL (list paramL))
-                                  (#.Primitive nameL (list paramR)))))
-            ))))
-
-(context: "Type variables."
-  ($_ seq
-      (test "Type-vars check against themselves."
-            (type-checks? (do @.monad
-                            [[id var] @.var]
-                            (@.check var var))))
-
-      (test "Can bind unbound type-vars by type-checking against them."
-            (and (type-checks? (do @.monad
-                                 [[id var] @.var]
-                                 (@.check var .Any)))
-                 (type-checks? (do @.monad
-                                 [[id var] @.var]
-                                 (@.check .Any var)))))
-
-      (test "Cannot rebind already bound type-vars."
-            (not (type-checks? (do @.monad
-                                 [[id var] @.var
-                                  _ (@.check var .Bit)]
-                                 (@.check var .Nat)))))
-
-      (test "If the type bound to a var is a super-type to another, then the var is also a super-type."
-            (type-checks? (do @.monad
-                            [[id var] @.var
-                             _ (@.check var Any)]
-                            (@.check var .Bit))))
-
-      (test "If the type bound to a var is a sub-type of another, then the var is also a sub-type."
-            (type-checks? (do @.monad
-                            [[id var] @.var
-                             _ (@.check var Nothing)]
-                            (@.check .Bit var))))
-      ))
-
 (def: (build-ring num-connections)
-  (-> Nat (@.Check [[Nat Type] (List [Nat Type]) [Nat Type]]))
-  (do @.monad
-    [[head-id head-type] @.var
-     ids+types (monad.seq @ (list.repeat num-connections @.var))
+  (-> Nat (/.Check [[Nat Type] (List [Nat Type]) [Nat Type]]))
+  (do /.monad
+    [[head-id head-type] /.var
+     ids+types (monad.seq @ (list.repeat num-connections /.var))
      [tail-id tail-type] (monad.fold @ (function (_ [tail-id tail-type] [_head-id _head-type])
                                          (do @
-                                           [_ (@.check head-type tail-type)]
+                                           [_ (/.check head-type tail-type)]
                                            (wrap [tail-id tail-type])))
                                      [head-id head-type]
                                      ids+types)]
     (wrap [[head-id head-type] ids+types [tail-id tail-type]])))
 
-(context: "Rings of type variables."
-  (<| (times 100)
-      (do @
-        [num-connections (|> r.nat (:: @ map (n/% 100)))
-         boundT (|> //.gen-type (r.filter (|>> (case> (#.Var _) #0 _ #1))))
-         pick-pcg (r.and r.nat r.nat)]
-        ($_ seq
-            (test "Can create rings of variables."
-                  (type-checks? (do @.monad
-                                  [[[head-id head-type] ids+types [tail-id tail-type]] (build-ring num-connections)
-                                   #let [ids (list;map product.left ids+types)]
-                                   headR (@.ring head-id)
-                                   tailR (@.ring tail-id)]
-                                  (@.assert ""
-                                            (let [same-rings? (:: set.equivalence = headR tailR)
-                                                  expected-size? (n/= (inc num-connections) (set.size headR))
-                                                  same-vars? (|> (set.to-list headR)
-                                                                 (list.sort n/<)
-                                                                 (:: (list.equivalence number.equivalence) = (list.sort n/< (#.Cons head-id ids))))]
-                                              (and same-rings?
-                                                   expected-size?
-                                                   same-vars?))))))
-            (test "When a var in a ring is bound, all the ring is bound."
-                  (type-checks? (do @.monad
-                                  [[[head-id headT] ids+types tailT] (build-ring num-connections)
-                                   #let [ids (list;map product.left ids+types)]
-                                   _ (@.check headT boundT)
-                                   head-bound (@.read head-id)
-                                   tail-bound (monad.map @ @.read ids)
-                                   headR (@.ring head-id)
-                                   tailR+ (monad.map @ @.ring ids)]
-                                  (let [rings-were-erased? (and (set.empty? headR)
-                                                                (list.every? set.empty? tailR+))
-                                        same-types? (list.every? (type;= boundT) (list& (maybe.default headT head-bound)
-                                                                                        (list;map (function (_ [tail-id ?tailT])
-                                                                                                    (maybe.default (#.Var tail-id) ?tailT))
-                                                                                                  (list.zip2 ids tail-bound))))]
-                                    (@.assert ""
-                                              (and rings-were-erased?
-                                                   same-types?))))))
-            (test "Can merge multiple rings of variables."
-                  (type-checks? (do @.monad
-                                  [[[head-idL headTL] ids+typesL [tail-idL tailTL]] (build-ring num-connections)
-                                   [[head-idR headTR] ids+typesR [tail-idR tailTR]] (build-ring num-connections)
-                                   headRL-pre (@.ring head-idL)
-                                   headRR-pre (@.ring head-idR)
-                                   _ (@.check headTL headTR)
-                                   headRL-post (@.ring head-idL)
-                                   headRR-post (@.ring head-idR)]
-                                  (@.assert ""
-                                            (let [same-rings? (:: set.equivalence = headRL-post headRR-post)
-                                                  expected-size? (n/= (n/* 2 (inc num-connections))
-                                                                      (set.size headRL-post))
-                                                  union? (:: set.equivalence = headRL-post (set.union headRL-pre headRR-pre))]
-                                              (and same-rings?
-                                                   expected-size?
-                                                   union?))))))
-            ))
-      ))
+(def: #export test
+  Test
+  (<| (_.context (%name (name-of /._)))
+      ($_ _.and
+          (do r.monad
+            [sample (|> ..type (r.filter valid-type?))]
+            ($_ _.and
+                (_.test "Any is the super-type of everything."
+                        (/.checks? Any sample))
+                (_.test "Nothing is the sub-type of everything."
+                        (/.checks? sample Nothing))
+                ))
+          ($_ _.and
+              (_.test "Any and Nothing match themselves."
+                      (and (/.checks? Nothing Nothing)
+                           (/.checks? Any Any)))
+              (_.test "Existential types only match with themselves."
+                      (and (type-checks? (do /.monad
+                                           [[_ exT] /.existential]
+                                           (/.check exT exT)))
+                           (not (type-checks? (do /.monad
+                                                [[_ exTL] /.existential
+                                                 [_ exTR] /.existential]
+                                                (/.check exTL exTR))))))
+              (_.test "Names do not affect type-checking."
+                      (and (type-checks? (do /.monad
+                                           [[_ exT] /.existential]
+                                           (/.check (#.Named ["module" "name"] exT)
+                                                    exT)))
+                           (type-checks? (do /.monad
+                                           [[_ exT] /.existential]
+                                           (/.check exT
+                                                    (#.Named ["module" "name"] exT))))
+                           (type-checks? (do /.monad
+                                           [[_ exT] /.existential]
+                                           (/.check (#.Named ["module" "name"] exT)
+                                                    (#.Named ["module" "name"] exT))))))
+              (_.test "Functions are covariant on inputs and contravariant on outputs."
+                      (and (/.checks? (#.Function Nothing Any)
+                                      (#.Function Any Nothing))
+                           (not (/.checks? (#.Function Any Nothing)
+                                           (#.Function Nothing Any)))))
+              )
+          (do r.monad
+            [meta ..type
+             data ..type]
+            (_.test "Can type-check type application."
+                    (and (/.checks? (|> Ann (#.Apply meta) (#.Apply data))
+                                    (type.tuple (list meta data)))
+                         (/.checks? (type.tuple (list meta data))
+                                    (|> Ann (#.Apply meta) (#.Apply data))))))
+          (do r.monad
+            [#let [gen-short (r.ascii 10)]
+             nameL gen-short
+             nameR (|> gen-short (r.filter (|>> (text@= nameL) not)))
+             paramL ..type
+             paramR (|> ..type (r.filter (|>> (/.checks? paramL) not)))]
+            ($_ _.and
+                (_.test "Primitive types match when they have the same name and the same parameters."
+                        (/.checks? (#.Primitive nameL (list paramL))
+                                   (#.Primitive nameL (list paramL))))
+                (_.test "Names matter to primitive types."
+                        (not (/.checks? (#.Primitive nameL (list paramL))
+                                        (#.Primitive nameR (list paramL)))))
+                (_.test "Parameters matter to primitive types."
+                        (not (/.checks? (#.Primitive nameL (list paramL))
+                                        (#.Primitive nameL (list paramR)))))
+                ))
+          ($_ _.and
+              (_.test "Type-vars check against themselves."
+                      (type-checks? (do /.monad
+                                      [[id var] /.var]
+                                      (/.check var var))))
+              (_.test "Can bind unbound type-vars by type-checking against them."
+                      (and (type-checks? (do /.monad
+                                           [[id var] /.var]
+                                           (/.check var .Any)))
+                           (type-checks? (do /.monad
+                                           [[id var] /.var]
+                                           (/.check .Any var)))))
+              (_.test "Cannot rebind already bound type-vars."
+                      (not (type-checks? (do /.monad
+                                           [[id var] /.var
+                                            _ (/.check var .Bit)]
+                                           (/.check var .Nat)))))
+              (_.test "If the type bound to a var is a super-type to another, then the var is also a super-type."
+                      (type-checks? (do /.monad
+                                      [[id var] /.var
+                                       _ (/.check var Any)]
+                                      (/.check var .Bit))))
+              (_.test "If the type bound to a var is a sub-type of another, then the var is also a sub-type."
+                      (type-checks? (do /.monad
+                                      [[id var] /.var
+                                       _ (/.check var Nothing)]
+                                      (/.check .Bit var))))
+              )
+          (do r.monad
+            [num-connections (|> r.nat (:: @ map (n/% 100)))
+             boundT (|> ..type (r.filter (|>> (case> (#.Var _) #0 _ #1))))
+             pick-pcg (r.and r.nat r.nat)]
+            ($_ _.and
+                (_.test "Can create rings of variables."
+                        (type-checks? (do /.monad
+                                        [[[head-id head-type] ids+types [tail-id tail-type]] (build-ring num-connections)
+                                         #let [ids (list@map product.left ids+types)]
+                                         headR (/.ring head-id)
+                                         tailR (/.ring tail-id)]
+                                        (/.assert ""
+                                                  (let [same-rings? (:: set.equivalence = headR tailR)
+                                                        expected-size? (n/= (inc num-connections) (set.size headR))
+                                                        same-vars? (|> (set.to-list headR)
+                                                                       (list.sort n/<)
+                                                                       (:: (list.equivalence nat.equivalence) = (list.sort n/< (#.Cons head-id ids))))]
+                                                    (and same-rings?
+                                                         expected-size?
+                                                         same-vars?))))))
+                (_.test "When a var in a ring is bound, all the ring is bound."
+                        (type-checks? (do /.monad
+                                        [[[head-id headT] ids+types tailT] (build-ring num-connections)
+                                         #let [ids (list@map product.left ids+types)]
+                                         _ (/.check headT boundT)
+                                         head-bound (/.read head-id)
+                                         tail-bound (monad.map @ /.read ids)
+                                         headR (/.ring head-id)
+                                         tailR+ (monad.map @ /.ring ids)]
+                                        (let [rings-were-erased? (and (set.empty? headR)
+                                                                      (list.every? set.empty? tailR+))
+                                              same-types? (list.every? (type@= boundT) (list& (maybe.default headT head-bound)
+                                                                                              (list@map (function (_ [tail-id ?tailT])
+                                                                                                          (maybe.default (#.Var tail-id) ?tailT))
+                                                                                                        (list.zip2 ids tail-bound))))]
+                                          (/.assert ""
+                                                    (and rings-were-erased?
+                                                         same-types?))))))
+                (_.test "Can merge multiple rings of variables."
+                        (type-checks? (do /.monad
+                                        [[[head-idL headTL] ids+typesL [tail-idL tailTL]] (build-ring num-connections)
+                                         [[head-idR headTR] ids+typesR [tail-idR tailTR]] (build-ring num-connections)
+                                         headRL-pre (/.ring head-idL)
+                                         headRR-pre (/.ring head-idR)
+                                         _ (/.check headTL headTR)
+                                         headRL-post (/.ring head-idL)
+                                         headRR-post (/.ring head-idR)]
+                                        (/.assert ""
+                                                  (let [same-rings? (:: set.equivalence = headRL-post headRR-post)
+                                                        expected-size? (n/= (n/* 2 (inc num-connections))
+                                                                            (set.size headRL-post))
+                                                        union? (:: set.equivalence = headRL-post (set.union headRL-pre headRR-pre))]
+                                                    (and same-rings?
+                                                         expected-size?
+                                                         union?))))))
+                ))
+          )))
diff --git a/stdlib/source/test/lux/type/dynamic.lux b/stdlib/source/test/lux/type/dynamic.lux
index 70e26f743..e2564627a 100644
--- a/stdlib/source/test/lux/type/dynamic.lux
+++ b/stdlib/source/test/lux/type/dynamic.lux
@@ -1,31 +1,32 @@
 (.module:
   [lux #*
-   [control
-    [monad (#+ do)]]
+   data/text/format
+   ["r" math/random (#+ Random)]
+   ["_" test (#+ Test)]
+   [control ["." monad (#+ do)]]
    [data
-    ["." error]]
-   [math
-    ["r" random]]
-   [type
-    ["/" dynamic (#+ Dynamic :dynamic :check)]]]
-  lux/test)
+    ["." error]]]
+  {1
+   ["." / (#+ Dynamic :dynamic :check)]})
 
-(context: "Dynamic typing."
-  (do @
-    [expected r.nat
-     #let [value (:dynamic expected)]]
-    ($_ seq
-        (test "Can check dynamic values."
-              (case (:check Nat value)
-                (#error.Success actual)
-                (n/= expected actual)
-                
-                (#error.Failure error)
-                false))
-        (test "Cannot confuse types."
-              (case (:check Text value)
-                (#error.Success actual)
-                false
-                
-                (#error.Failure error)
-                true)))))
+(def: #export test
+  Test
+  (<| (_.context (%name (name-of /._)))
+      (do r.monad
+        [expected r.nat
+         #let [value (:dynamic expected)]]
+        ($_ _.and
+            (_.test "Can check dynamic values."
+                    (case (:check Nat value)
+                      (#error.Success actual)
+                      (n/= expected actual)
+                      
+                      (#error.Failure error)
+                      false))
+            (_.test "Cannot confuse types."
+                    (case (:check Text value)
+                      (#error.Success actual)
+                      false
+                      
+                      (#error.Failure error)
+                      true))))))
diff --git a/stdlib/source/test/lux/type/implicit.lux b/stdlib/source/test/lux/type/implicit.lux
index dffd9496c..5383c252f 100644
--- a/stdlib/source/test/lux/type/implicit.lux
+++ b/stdlib/source/test/lux/type/implicit.lux
@@ -1,40 +1,41 @@
 (.module:
   [lux #*
-   [io]
+   data/text/format
+   ["r" math/random (#+ Random)]
+   ["_" test (#+ Test)]
+   [control ["." monad (#+ do)]]
    [control
-    [equivalence]
-    [functor]
-    [monad (#+ Monad do)]]
+    [equivalence (#+)]
+    [functor (#+)]]
    [data
-    ["." bit ("#;." equivalence)]
-    [number]
-    [collection [list]]]
-   [math
-    ["r" random]]
-   [type implicit]]
-  lux/test)
+    ["." bit ("#@." equivalence)]
+    [number
+     ["." nat]]
+    [collection
+     ["." list]]]]
+  {1
+   ["." /]})
 
-(context: "Automatic structure selection"
-  (<| (times 100)
-      (do @
+(def: #export test
+  Test
+  (<| (_.context (%name (name-of /._)))
+      (do r.monad
         [x r.nat
          y r.nat]
-        ($_ seq
-            (test "Can automatically select first-order structures."
-                  (let [(^open "list;.") (list.equivalence number.equivalence)]
-                    (and (bit;= (:: number.equivalence = x y)
-                                (::: = x y))
-                         (list;= (list.n/range 1 10)
-                                 (::: map inc (list.n/range 0 9)))
-                         )))
-            
-            (test "Can automatically select second-order structures."
-                  (::: =
-                    (list.n/range 1 10)
-                    (list.n/range 1 10)))
-
-            (test "Can automatically select third-order structures."
-                  (let [lln (::: map (list.n/range 1)
-                              (list.n/range 1 10))]
-                    (::: = lln lln)))
+        ($_ _.and
+            (_.test "Can automatically select first-order structures."
+                    (let [(^open "list@.") (list.equivalence nat.equivalence)]
+                      (and (bit@= (:: nat.equivalence = x y)
+                                  (/.::: = x y))
+                           (list@= (list.n/range 1 10)
+                                   (/.::: map inc (list.n/range 0 9)))
+                           )))
+            (_.test "Can automatically select second-order structures."
+                    (/.::: =
+                      (list.n/range 1 10)
+                      (list.n/range 1 10)))
+            (_.test "Can automatically select third-order structures."
+                    (let [lln (/.::: map (list.n/range 1)
+                                (list.n/range 1 10))]
+                      (/.::: = lln lln)))
             ))))
diff --git a/stdlib/source/test/lux/type/resource.lux b/stdlib/source/test/lux/type/resource.lux
index b04321cc2..15d7cd137 100644
--- a/stdlib/source/test/lux/type/resource.lux
+++ b/stdlib/source/test/lux/type/resource.lux
@@ -1,48 +1,50 @@
 (.module:
   [lux #*
+   data/text/format
+   ["r" math/random (#+ Random)]
+   ["_" test (#+ Test)]
    [control
     [monad
      [indexed (#+ do)]]]
-   [type
-    ["." resource (#+ Res)]]
    ["." io]]
-  lux/test)
+  {1
+   ["." / (#+ Res)]})
 
-(context: "Sub-structural typing."
-  ($_ seq
-      (test "Can produce and consume keys in an ordered manner."
-            (<| (n/= (n/+ 123 456))
-                io.run
-                resource.run-sync
-                (do resource.sync
-                  [res|left (resource.ordered-sync 123)
-                   res|right (resource.ordered-sync 456)
-                   right (resource.read-sync res|right)
-                   left (resource.read-sync res|left)]
-                  (wrap (n/+ left right)))))
-      
-      (test "Can exchange commutative keys."
-            (<| (n/= (n/+ 123 456))
-                io.run
-                resource.run-sync
-                (do resource.sync
-                  [res|left (resource.commutative-sync 123)
-                   res|right (resource.commutative-sync 456)
-                   _ (resource.exchange-sync [1 0])
-                   left (resource.read-sync res|left)
-                   right (resource.read-sync res|right)]
-                  (wrap (n/+ left right)))))
-
-      (test "Can group and un-group keys."
-            (<| (n/= (n/+ 123 456))
-                io.run
-                resource.run-sync
-                (do resource.sync
-                  [res|left (resource.commutative-sync 123)
-                   res|right (resource.commutative-sync 456)
-                   _ (resource.group-sync 2)
-                   _ (resource.un-group-sync 2)
-                   right (resource.read-sync res|right)
-                   left (resource.read-sync res|left)]
-                  (wrap (n/+ left right)))))
-      ))
+(def: #export test
+  Test
+  (<| (_.context (%name (name-of /._)))
+      ($_ _.and
+          (_.test "Can produce and consume keys in an ordered manner."
+                  (<| (n/= (n/+ 123 456))
+                      io.run
+                      /.run-sync
+                      (do /.sync
+                        [res|left (/.ordered-sync 123)
+                         res|right (/.ordered-sync 456)
+                         right (/.read-sync res|right)
+                         left (/.read-sync res|left)]
+                        (wrap (n/+ left right)))))
+          (_.test "Can exchange commutative keys."
+                  (<| (n/= (n/+ 123 456))
+                      io.run
+                      /.run-sync
+                      (do /.sync
+                        [res|left (/.commutative-sync 123)
+                         res|right (/.commutative-sync 456)
+                         _ (/.exchange-sync [1 0])
+                         left (/.read-sync res|left)
+                         right (/.read-sync res|right)]
+                        (wrap (n/+ left right)))))
+          (_.test "Can group and un-group keys."
+                  (<| (n/= (n/+ 123 456))
+                      io.run
+                      /.run-sync
+                      (do /.sync
+                        [res|left (/.commutative-sync 123)
+                         res|right (/.commutative-sync 456)
+                         _ (/.group-sync 2)
+                         _ (/.un-group-sync 2)
+                         right (/.read-sync res|right)
+                         left (/.read-sync res|left)]
+                        (wrap (n/+ left right)))))
+          )))