- Yet more refactoring.

1 files changed, 31 insertions, 28 deletions

diff --git a/stdlib/test/test/lux/meta/type/check.lux b/stdlib/test/test/lux/meta/type/check.lux
index b1239fa43..127e02cbd 100644
--- a/stdlib/test/test/lux/meta/type/check.lux
+++ b/stdlib/test/test/lux/meta/type/check.lux
@@ -76,7 +76,7 @@
     false))
 
 ## [Tests]
-(context: "Top and Bottom"
+(context: "Top and Bottom."
   (<| (times +100)
       (do @
         [sample (|> gen-type (r;filter valid-type?))]
@@ -96,35 +96,35 @@
 
       (test "Existential types only match with themselves."
             (and (type-checks? (do @;Monad<Check>
-                                 [[id ex] @;existential]
-                                 (@;check ex ex)))
+                                 [[_ exT] @;existential]
+                                 (@;check exT exT)))
                  (not (type-checks? (do @;Monad<Check>
-                                      [[lid lex] @;existential
-                                       [rid rex] @;existential]
-                                      (@;check lex rex))))))
+                                      [[_ exTL] @;existential
+                                       [_ exTR] @;existential]
+                                      (@;check exTL exTR))))))
 
-      (test "Names don't affect type-checking."
+      (test "Names do not affect type-checking."
             (and (type-checks? (do @;Monad<Check>
-                                 [[id ex] @;existential]
-                                 (@;check (#;Named ["module" "name"] ex)
-                                          ex)))
+                                 [[_ exT] @;existential]
+                                 (@;check (#;Named ["module" "name"] exT)
+                                          exT)))
                  (type-checks? (do @;Monad<Check>
-                                 [[id ex] @;existential]
-                                 (@;check ex
-                                          (#;Named ["module" "name"] ex))))
+                                 [[_ exT] @;existential]
+                                 (@;check exT
+                                          (#;Named ["module" "name"] exT))))
                  (type-checks? (do @;Monad<Check>
-                                 [[id ex] @;existential]
-                                 (@;check (#;Named ["module" "name"] ex)
-                                          (#;Named ["module" "name"] ex))))))
+                                 [[_ exT] @;existential]
+                                 (@;check (#;Named ["module" "name"] exT)
+                                          (#;Named ["module" "name"] exT))))))
 
-      (test "Can type-check functions."
+      (test "Functions are covariant on inputs and contravariant on outputs."
             (and (@;checks? (#;Function Bottom Top)
                             (#;Function Top Bottom))
                  (not (@;checks? (#;Function Top Bottom)
                                  (#;Function Bottom Top)))))
       ))
 
-(context: "Type application"
+(context: "Type application."
   (<| (times +100)
       (do @
         [meta gen-type
@@ -135,7 +135,7 @@
                    (@;checks? (type;tuple (list meta data))
                               (|> Ann (#;Apply meta) (#;Apply data))))))))
 
-(context: "Primitive types"
+(context: "Primitive types."
   (<| (times +100)
       (do @
         [nameL gen-name
@@ -156,7 +156,7 @@
                                   (#;Primitive nameL (list paramR)))))
             ))))
 
-(context: "Type-vars"
+(context: "Type variables."
   ($_ seq
       (test "Type-vars check against themselves."
             (type-checks? (do @;Monad<Check>
@@ -203,11 +203,11 @@
                                      ids+types)]
     (wrap [[head-id head-type] ids+types [tail-id tail-type]])))
 
-(context: "Rings."
+(context: "Rings of type variables."
   (<| (times +100)
       (do @
         [num-connections (|> r;nat (:: @ map (n.% +100)))
-         bound (|> gen-type (r;filter (|>. (case> (#;Var _) false _ true))))
+         boundT (|> gen-type (r;filter (|>. (case> (#;Var _) false _ true))))
          pick-pcg (r;seq r;nat r;nat)]
         ($_ seq
             (test "Can create rings of variables."
@@ -227,26 +227,29 @@
                                                    same-vars?))))))
             (test "When a var in a ring is bound, all the ring is bound."
                   (type-checks? (do @;Monad<Check>
-                                  [[[head-id head-type] ids+types tail-type] (build-ring num-connections)
+                                  [[[head-id headT] ids+types tailT] (build-ring num-connections)
                                    #let [ids (list/map product;left ids+types)]
-                                   _ (@;check head-type bound)
+                                   _ (@;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/= bound) (list& head-bound tail-bound))]
+                                        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<Check>
-                                  [[[head-idL head-typeL] ids+typesL [tail-idL tail-typeL]] (build-ring num-connections)
-                                   [[head-idR head-typeR] ids+typesR [tail-idR tail-typeR]] (build-ring num-connections)
+                                  [[[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 head-typeL head-typeR)
+                                   _ (@;check headTL headTR)
                                    headRL-post (@;ring head-idL)
                                    headRR-post (@;ring head-idR)]
                                   (@;assert ""