- Yet more refactoring.

2 files changed, 118 insertions, 166 deletions

diff --git a/stdlib/source/lux/meta/type/check.lux b/stdlib/source/lux/meta/type/check.lux
index d6589760e..74c5a2a90 100644
--- a/stdlib/source/lux/meta/type/check.lux
+++ b/stdlib/source/lux/meta/type/check.lux
@@ -6,7 +6,7 @@
                 ["ex" exception #+ exception:])
        (data [text "text/" Monoid<Text> Eq<Text>]
              [number "nat/" Codec<Text,Nat>]
-             maybe
+             [maybe]
              [product]
              (coll [list]
                    [set #+ Set])
@@ -24,7 +24,9 @@
 
 (type: #export Var Nat)
 
-(type: #export Assumptions (List [[Type Type] Bool]))
+(type: #export Assumption
+  {#subsumption [Type Type]
+   #verdict Bool})
 
 (type: #export (Check a)
   (-> Type-Context (e;Error [Type-Context a])))
@@ -152,42 +154,35 @@
       (#e;Success [(update@ #;ex-counter n.inc context)
                    [id (#;Ex id)]]))))
 
-(def: #export (bound? id)
-  (-> Var (Check Bool))
-  (function [context]
-    (case (|> context (get@ #;var-bindings) (var::get id))
-      (#;Some (#;Some bound))
-      (#e;Success [context true])
-
-      (#;Some #;None)
-      (#e;Success [context false])
-      
-      #;None
-      (ex;throw Unknown-Type-Var (nat/encode id)))))
-
-(def: #export (concrete? id)
-  (-> Var (Check Bool))
-  (function [context]
-    (case (|> context (get@ #;var-bindings) (var::get id))
-      (#;Some (#;Some bound))
-      (#e;Success [context (case bound (#;Var _) false _ true)])
-
-      (#;Some #;None)
-      (#e;Success [context false])
-      
-      #;None
-      (ex;throw Unknown-Type-Var (nat/encode id)))))
+(do-template [<name> <outputT> <fail> <succeed>]
+  [(def: #export (<name> id)
+     (-> Var (Check <outputT>))
+     (function [context]
+       (case (|> context (get@ #;var-bindings) (var::get id))
+         (^or (#;Some (#;Some (#;Var _)))
+              (#;Some #;None))
+         (#e;Success [context <fail>])
+         
+         (#;Some (#;Some bound))
+         (#e;Success [context <succeed>])
+
+         #;None
+         (ex;throw Unknown-Type-Var (nat/encode id)))))]
+
+  [bound? Bool false true]
+  [read (Maybe Type) #;None (#;Some bound)]
+  )
 
-(def: #export (read id)
+(def: (peek id)
   (-> Var (Check Type))
   (function [context]
     (case (|> context (get@ #;var-bindings) (var::get id))
-      (#;Some (#;Some type))
-      (#e;Success [context type])
+      (#;Some (#;Some bound))
+      (#e;Success [context bound])
 
       (#;Some #;None)
       (ex;throw Unbound-Type-Var (nat/encode id))
-      
+
       #;None
       (ex;throw Unknown-Type-Var (nat/encode id)))))
 
@@ -220,51 +215,6 @@
       #;None
       (ex;throw Unknown-Type-Var (nat/encode id)))))
 
-(def: #export (clean t-id type)
-  (-> Var Type (Check Type))
-  (case type
-    (#;Var id)
-    (do Monad<Check>
-      [? (concrete? id)]
-      (if ?
-        (if (n.= t-id id)
-          (read id)
-          (do Monad<Check>
-            [=type (read id)
-             ==type (clean t-id =type)
-             _ (update ==type id)]
-            (wrap type)))
-        (wrap type)))
-
-    (#;Primitive name params)
-    (do Monad<Check>
-      [=params (monad;map @ (clean t-id) params)]
-      (wrap (#;Primitive name =params)))
-    
-    (^template [<tag>]
-      (<tag> left right)
-      (do Monad<Check>
-        [=left (clean t-id left)
-         =right (clean t-id right)]
-        (wrap (<tag> =left =right))))
-    ([#;Function]
-     [#;Apply]
-     [#;Product]
-     [#;Sum])
-
-    (^template [<tag>]
-      (<tag> env body)
-      (do Monad<Check>
-        [=env (monad;map @ (clean t-id) env)
-         =body (clean t-id body)] ## TODO: DO NOT CLEAN THE BODY
-        (wrap (<tag> =env =body))))
-    ([#;UnivQ]
-     [#;ExQ])
-    
-    _
-    (:: Monad<Check> wrap type)
-    ))
-
 (def: #export var
   (Check [Var Type])
   (function [context]
@@ -291,12 +241,13 @@
   (case funcT
     (#;Var func-id)
     (do Monad<Check>
-      [? (concrete? func-id)]
-      (if ?
-        (do @
-          [funcT' (read func-id)]
-          (apply-type! funcT' argT))
-        (throw Invalid-Type-Application (type;to-text (#;Apply argT funcT)))))
+      [?funcT' (read func-id)]
+      (case ?funcT'
+        #;None
+        (throw Invalid-Type-Application (type;to-text (#;Apply argT funcT)))
+
+        (#;Some funcT')
+        (apply-type! funcT' argT)))
 
     _
     (function [context]
@@ -373,15 +324,15 @@
       (right context))))
 
 (def: (assumed? [e a] assumptions)
-  (-> [Type Type] Assumptions (Maybe Bool))
-  (:: Monad<Maybe> map product;right
+  (-> [Type Type] (List Assumption) (Maybe Bool))
+  (:: maybe;Monad<Maybe> map product;right
       (list;find (function [[[fe fa] status]]
                    (and (type/= e fe)
                         (type/= a fa)))
                  assumptions)))
 
 (def: (assume! ea status assumptions)
-  (-> [Type Type] Bool Assumptions Assumptions)
+  (-> [Type Type] Bool (List Assumption) (List Assumption))
   (#;Cons [ea status] assumptions))
 
 (def: (on id type then else)
@@ -398,8 +349,8 @@
          _ (monad;map @ (update type) (set;to-list ring))]
         then)
       (do Monad<Check>
-        [bound (read id)]
-        (else bound))))
+        [?bound (read id)]
+        (else (maybe;default (#;Var id) ?bound)))))
 
 (def: (link-2 left right)
   (-> Var Var (Check Unit))
@@ -414,15 +365,15 @@
     (update (#;Var to) interpose)))
 
 (def: (check-vars check' assumptions idE idA)
-  (-> (-> Type Type Assumptions (Check Assumptions))
-      Assumptions
+  (-> (-> Type Type (List Assumption) (Check (List Assumption)))
+      (List Assumption)
       Var Var
-      (Check Assumptions))
+      (Check (List Assumption)))
   (if (n.= idE idA)
     (check/wrap assumptions)
     (do Monad<Check>
-      [ebound (attempt (read idE))
-       abound (attempt (read idA))]
+      [ebound (attempt (peek idE))
+       abound (attempt (peek idA))]
       (case [ebound abound]
         ## Link the 2 variables circularily
         [#;None #;None]
@@ -504,9 +455,9 @@
       output)))
 
 (def: (check-apply check' assumptions [eAT eFT] [aAT aFT])
-  (-> (-> Type Type Assumptions (Check Assumptions)) Assumptions
+  (-> (-> Type Type (List Assumption) (Check (List Assumption))) (List Assumption)
       [Type Type] [Type Type]
-      (Check Assumptions))
+      (Check (List Assumption)))
   (case [eFT aFT]
     (^or [(#;Ex _) _] [_ (#;Ex _)])
     (do Monad<Check>
@@ -514,31 +465,39 @@
       (check' eAT aAT assumptions))
 
     [(#;Var id) _]
-    (either (do Monad<Check>
-              [rFT (read id)]
-              (check' (#;Apply eAT rFT) (#;Apply aAT aFT) assumptions))
-            (do Monad<Check>
-              [assumptions (check' (#;Var id) aFT assumptions)
-               e' (apply-type! aFT eAT)
-               a' (apply-type! aFT aAT)]
-              (check' e' a' assumptions)))
+    (do Monad<Check>
+      [?rFT (read id)]
+      (case ?rFT
+        (#;Some rFT)
+        (check' (#;Apply eAT rFT) (#;Apply aAT aFT) assumptions)
+
+        _
+        (do Monad<Check>
+          [assumptions (check' eFT aFT assumptions)
+           e' (apply-type! aFT eAT)
+           a' (apply-type! aFT aAT)]
+          (check' e' a' assumptions))))
 
     [_ (#;Var id)]
-    (either (do Monad<Check>
-              [rFT (read id)]
-              (check' (#;Apply eAT eFT) (#;Apply aAT rFT) assumptions))
-            (do Monad<Check>
-              [assumptions (check' eFT (#;Var id) assumptions)
-               e' (apply-type! eFT eAT)
-               a' (apply-type! eFT aAT)]
-              (check' e' a' assumptions)))
+    (do Monad<Check>
+      [?rFT (read id)]
+      (case ?rFT
+        (#;Some rFT)
+        (check' (#;Apply eAT eFT) (#;Apply aAT rFT) assumptions)
+
+        _
+        (do Monad<Check>
+          [assumptions (check' eFT aFT assumptions)
+           e' (apply-type! eFT eAT)
+           a' (apply-type! eFT aAT)]
+          (check' e' a' assumptions))))
 
     _
     (fail "")))
 
 (def: #export (check' expected actual assumptions)
   {#;doc "Type-check to ensure that the 'expected' type subsumes the 'actual' type."}
-  (-> Type Type Assumptions (Check Assumptions))
+  (-> Type Type (List Assumption) (Check (List Assumption)))
   (if (is expected actual)
     (check/wrap assumptions)
     (with-error-stack
@@ -588,33 +547,23 @@
           [actual' (apply-type! F A)]
           (check' expected actual' assumptions))
 
-        [(#;UnivQ _) _]
-        (do Monad<Check>
-          [[ex-id ex] existential
-           expected' (apply-type! expected ex)]
-          (check' expected' actual assumptions))
-
-        [_ (#;UnivQ _)]
-        (do Monad<Check>
-          [[var-id var] ;;var
-           actual' (apply-type! actual var)
-           assumptions (check' expected actual' assumptions)
-           _ (clean var-id expected)]
-          (check/wrap assumptions))
-
-        [(#;ExQ e!env e!def) _]
-        (do Monad<Check>
-          [[var-id var] ;;var
-           expected' (apply-type! expected var)
-           assumptions (check' expected' actual assumptions)
-           _ (clean var-id actual)]
-          (check/wrap assumptions))
-
-        [_ (#;ExQ a!env a!def)]
-        (do Monad<Check>
-          [[ex-id ex] existential
-           actual' (apply-type! actual ex)]
-          (check' expected actual' assumptions))
+        (^template [<tag> <instancer>]
+          [(<tag> _) _]
+          (do Monad<Check>
+            [[_ paramT] <instancer>
+             expected' (apply-type! expected paramT)]
+            (check' expected' actual assumptions)))
+        ([#;UnivQ ;;existential]
+         [#;ExQ ;;var])
+
+        (^template [<tag> <instancer>]
+          [_ (<tag> _)]
+          (do Monad<Check>
+            [[_ paramT] <instancer>
+             actual' (apply-type! actual paramT)]
+            (check' expected actual' assumptions)))
+        ([#;UnivQ ;;var]
+         [#;ExQ ;;existential])
 
         [(#;Primitive e-name e-params) (#;Primitive a-name a-params)]
         (if (and (text/= e-name a-name)
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 ""