- Improved error messaging when building variants & tuples.

- Improved error messaging when type-checking.
- Improved error messaging when applying functions.

3 files changed, 307 insertions, 290 deletions

diff --git a/src/lux/analyser/lux.clj b/src/lux/analyser/lux.clj
index db1c4e28e..1ad187f77 100644
--- a/src/lux/analyser/lux.clj
+++ b/src/lux/analyser/lux.clj
@@ -80,38 +80,32 @@
                                      (&/V &&/$tuple =elems)
                                      ))))
         (|do [exo-type* (&type/actual-type exo-type)]
-          (|case exo-type*
-            (&/$TupleT ?members)
-            (|do [=elems (&/map2% (fn [elem-t elem]
-                                    (&&/analyse-1 analyse elem-t elem))
-                                  ?members ?elems)
-                  _cursor &/cursor]
-              (return (&/|list (&&/|meta exo-type _cursor
-                                         (&/V &&/$tuple =elems)
-                                         ))))
-
-            (&/$UnivQ _)
-            (|do [$var &type/existential
-                  exo-type** (&type/apply-type exo-type* $var)
-                  [[tuple-type tuple-cursor] tuple-analysis] (&&/cap-1 (analyse-tuple analyse (&/V &/$Right exo-type**) ?elems))]
-              (return (&/|list (&&/|meta exo-type tuple-cursor
-                                         tuple-analysis))))
-
-            _
-            (fail (str "[Analyser Error] Tuples require tuple-types: " (&type/show-type exo-type*) " " (&type/show-type exo-type) " " "[" (->> ?elems (&/|map &/show-ast) (&/|interpose " ") (&/fold str "")) "]"))
-            ))))))
-
-(defn with-attempt [m-value on-error]
-  (fn [state]
-    (|case (m-value state)
-      (&/$Left msg)
-      ((on-error msg) state)
-      
-      output
-      output)))
+          (&/with-attempt
+            (|case exo-type*
+              (&/$TupleT ?members)
+              (|do [=elems (&/map2% (fn [elem-t elem]
+                                      (&&/analyse-1 analyse elem-t elem))
+                                    ?members ?elems)
+                    _cursor &/cursor]
+                (return (&/|list (&&/|meta exo-type _cursor
+                                           (&/V &&/$tuple =elems)
+                                           ))))
+
+              (&/$UnivQ _)
+              (|do [$var &type/existential
+                    exo-type** (&type/apply-type exo-type* $var)
+                    [[tuple-type tuple-cursor] tuple-analysis] (&&/cap-1 (analyse-tuple analyse (&/V &/$Right exo-type**) ?elems))]
+                (return (&/|list (&&/|meta exo-type tuple-cursor
+                                           tuple-analysis))))
+
+              _
+              (fail (str "[Analyser Error] Tuples require tuple-types: " (&type/show-type exo-type*)))
+              )
+            (fn [err]
+              (fail (str err "\n" "[Analyser Error] Tuples require tuple-types: " (&type/show-type exo-type))))))))))
 
 (defn ^:private analyse-variant-body [analyse exo-type ?values]
-  (|do [output (with-attempt
+  (|do [output (&/with-attempt
                  (|case ?values
                    (&/$Nil)
                    (analyse-tuple analyse (&/V &/$Right exo-type) &/Nil$)
@@ -169,38 +163,48 @@
 
                       _
                       (&type/actual-type exo-type))]
-      (|case exo-type*
-        (&/$VariantT ?cases)
-        (|case (&/|at idx ?cases)
-          (&/$Some vtype)
-          (|do [=value (with-attempt
-                         (analyse-variant-body analyse vtype ?values)
-                         (fn [err]
-                           (|do [_exo-type (&type/deref+ exo-type)]
-                             (fail (str err "\n"
-                                        'analyse-variant " " idx " " (&type/show-type exo-type) " " (&type/show-type _exo-type)
-                                        " " (->> ?values (&/|map &/show-ast) (&/|interpose " ") (&/fold str "")))))))
-                _cursor &/cursor]
-            (return (&/|list (&&/|meta exo-type _cursor
-                                       (&/V &&/$variant (&/T idx =value))
-                                       ))))
-
-          (&/$None)
-          (fail (str "[Analyser Error] There is no case " idx " for variant type " (&type/show-type exo-type*))))
+      (&/with-attempt
+        (|case exo-type*
+          (&/$VariantT ?cases)
+          (|case (&/|at idx ?cases)
+            (&/$Some vtype)
+            (|do [=value (&/with-attempt
+                           (analyse-variant-body analyse vtype ?values)
+                           (fn [err]
+                             (|do [_exo-type (&type/deref+ exo-type)]
+                               (fail (str err "\n"
+                                          'analyse-variant " " idx " " (&type/show-type exo-type) " " (&type/show-type _exo-type)
+                                          " " (->> ?values (&/|map &/show-ast) (&/|interpose " ") (&/fold str "")))))))
+                  _cursor &/cursor]
+              (return (&/|list (&&/|meta exo-type _cursor
+                                         (&/V &&/$variant (&/T idx =value))
+                                         ))))
 
-        (&/$UnivQ _)
-        (|do [$var &type/existential
-              exo-type** (&type/apply-type exo-type* $var)]
-          (analyse-variant analyse (&/V &/$Right exo-type**) idx ?values))
+            (&/$None)
+            (fail (str "[Analyser Error] There is no case " idx " for variant type " (&type/show-type exo-type*))))
 
-        (&/$ExQ _)
-        (&type/with-var
-          (fn [$var]
-            (|do [exo-type** (&type/apply-type exo-type* $var)]
-              (analyse-variant analyse (&/V &/$Right exo-type**) idx ?values))))
-        
-        _
-        (fail (str "[Analyser Error] Can't create a variant if the expected type is " (&type/show-type exo-type*)))))))
+          (&/$UnivQ _)
+          (|do [$var &type/existential
+                exo-type** (&type/apply-type exo-type* $var)]
+            (analyse-variant analyse (&/V &/$Right exo-type**) idx ?values))
+
+          (&/$ExQ _)
+          (&type/with-var
+            (fn [$var]
+              (|do [exo-type** (&type/apply-type exo-type* $var)]
+                (analyse-variant analyse (&/V &/$Right exo-type**) idx ?values))))
+          
+          _
+          (fail (str "[Analyser Error] Can't create variant if the expected type is " (&type/show-type exo-type*))))
+        (fn [err]
+          (|case exo-type
+            (&/$VarT ?id)
+            (|do [=exo-type (&type/deref ?id)]
+              (fail (str err "\n" "[Analyser Error] Can't create variant if the expected type is " (&type/show-type =exo-type))))
+
+            _
+            (fail (str err "\n" "[Analyser Error] Can't create variant if the expected type is " (&type/show-type exo-type))))))
+      )))
 
 (defn analyse-record [analyse exo-type ?elems]
   (|do [[rec-members rec-type] (&&record/order-record ?elems)]
@@ -276,7 +280,7 @@
 
             _
             (fail* "[Analyser Error] Can't have anything other than a global def in the global environment."))
-          (fail* ""))
+          (fail* (str "[Analyser Error] Unknown global definition: " name)))
         
         (&/$Cons top-outer _)
         (|let [scopes (&/|tail (&/folds #(&/Cons$ (&/get$ &/$name %2) %1)
@@ -310,39 +314,40 @@
     
     (&/$Cons ?arg ?args*)
     (|do [?fun-type* (&type/actual-type fun-type)]
-      (|case ?fun-type*
-        (&/$UnivQ _)
-        (&type/with-var
-          (fn [$var]
-            (|do [type* (&type/apply-type ?fun-type* $var)
-                  [=output-t =args] (analyse-apply* analyse exo-type type* ?args)]
-              (|case $var
-                (&/$VarT ?id)
-                (|do [? (&type/bound? ?id)
-                      type** (if ?
-                               (&type/clean $var =output-t)
-                               (|do [_ (&type/set-var ?id (&/V &/$BoundT 1))]
-                                 (&type/clean $var =output-t)))]
-                  (return (&/T type** =args)))
-                ))))
-
-        (&/$ExQ _)
-        (|do [$var &type/existential
-              type* (&type/apply-type ?fun-type* $var)]
-          (analyse-apply* analyse exo-type type* ?args))
-
-        (&/$LambdaT ?input-t ?output-t)
-        (|do [[=output-t =args] (analyse-apply* analyse exo-type ?output-t ?args*)
-              =arg (with-attempt
-                     (&&/analyse-1 analyse ?input-t ?arg)
-                     (fn [err]
-                       (fail (str err "\n"
-                                  'analyse-apply* " " (&type/show-type exo-type) " " (&type/show-type ?fun-type*)
-                                  " " "(_ " (->> ?args (&/|map &/show-ast) (&/|interpose " ") (&/fold str "")) ")"))))]
-          (return (&/T =output-t (&/Cons$ =arg =args))))
+      (&/with-attempt
+        (|case ?fun-type*
+          (&/$UnivQ _)
+          (&type/with-var
+            (fn [$var]
+              (|do [type* (&type/apply-type ?fun-type* $var)
+                    [=output-t =args] (analyse-apply* analyse exo-type type* ?args)]
+                (|case $var
+                  (&/$VarT ?id)
+                  (|do [? (&type/bound? ?id)
+                        type** (if ?
+                                 (&type/clean $var =output-t)
+                                 (|do [_ (&type/set-var ?id (&/V &/$BoundT 1))]
+                                   (&type/clean $var =output-t)))]
+                    (return (&/T type** =args)))
+                  ))))
+
+          (&/$ExQ _)
+          (|do [$var &type/existential
+                type* (&type/apply-type ?fun-type* $var)]
+            (analyse-apply* analyse exo-type type* ?args))
+
+          (&/$LambdaT ?input-t ?output-t)
+          (|do [[=output-t =args] (analyse-apply* analyse exo-type ?output-t ?args*)
+                =arg (&/with-attempt
+                       (&&/analyse-1 analyse ?input-t ?arg)
+                       (fn [err]
+                         (fail (str err "\n" "[Analyser Error] Function expected: " (&type/show-type ?input-t)))))]
+            (return (&/T =output-t (&/Cons$ =arg =args))))
 
-        _
-        (fail (str "[Analyser Error] Can't apply a non-function: " (&type/show-type ?fun-type*)))))
+          _
+          (fail (str "[Analyser Error] Can't apply a non-function: " (&type/show-type ?fun-type*))))
+        (fn [err]
+          (fail (str err "\n" "[Analyser Error] Can't apply function " (&type/show-type fun-type) " to args: " (->> ?args (&/|map &/show-ast) (&/|interpose " ") (&/fold str "")))))))
     ))
 
 (defn analyse-apply [analyse exo-type form-cursor =fn ?args]
@@ -354,15 +359,15 @@
           (|case $def
             (&/$MacroD macro)
             (|do [macro-expansion #(-> macro (.apply ?args) (.apply %))
-                  :let [_ (when (or (= "invoke-static$" (aget real-name 1))
-                                    (= "invoke-virtual$" (aget real-name 1))
-                                    (= "new$" (aget real-name 1))
-                                    (= "let%" (aget real-name 1))
-                                    (= "jvm-import" (aget real-name 1)))
-                            (->> (&/|map &/show-ast macro-expansion)
-                                 (&/|interpose "\n")
-                                 (&/fold str "")
-                                 (prn (&/ident->text real-name))))]
+                  ;; :let [_ (when (or (= "invoke-static$" (aget real-name 1))
+                  ;;                   (= "invoke-virtual$" (aget real-name 1))
+                  ;;                   (= "new$" (aget real-name 1))
+                  ;;                   (= "let%" (aget real-name 1))
+                  ;;                   (= "jvm-import" (aget real-name 1)))
+                  ;;           (->> (&/|map &/show-ast macro-expansion)
+                  ;;                (&/|interpose "\n")
+                  ;;                (&/fold str "")
+                  ;;                (prn (&/ident->text real-name))))]
                   ]
               (&/flat-map% (partial analyse exo-type) macro-expansion))
 
diff --git a/src/lux/base.clj b/src/lux/base.clj
index e3c6dcd5b..1da3859fc 100644
--- a/src/lux/base.clj
+++ b/src/lux/base.clj
@@ -595,6 +595,7 @@
           (try (.invoke define-class this (to-array [class-name bytecode (int 0) (int (alength bytecode))]))
             (catch java.lang.reflect.InvocationTargetException e
               ;; (prn 'InvocationTargetException (.getCause e))
+              ;; (prn 'InvocationTargetException (.getTargetException e))
               ;; (prn 'memory-class-loader/findClass class-name (get @store class-name))
               (throw e)))
           (do ;; (prn 'memory-class-loader/store class-name (keys @store))
@@ -1004,3 +1005,12 @@
   (fn [x]
     (|do [y (g x)]
       (f y))))
+
+(defn with-attempt [m-value on-error]
+  (fn [state]
+    (|case (m-value state)
+      ($Left msg)
+      ((on-error msg) state)
+      
+      output
+      output)))
diff --git a/src/lux/type.clj b/src/lux/type.clj
index 80316f039..491e81b3b 100644
--- a/src/lux/type.clj
+++ b/src/lux/type.clj
@@ -474,197 +474,199 @@
 (defn ^:private check* [class-loader fixpoints invariant?? expected actual]
   (if (clojure.lang.Util/identical expected actual)
     (return (&/T fixpoints nil))
-    (|case [expected actual]
-      [(&/$VarT ?eid) (&/$VarT ?aid)]
-      (if (.equals ^Object ?eid ?aid)
-        (return (&/T fixpoints nil))
-        (|do [ebound (fn [state]
-                       (|case ((deref ?eid) state)
-                         (&/$Right state* ebound)
-                         (return* state* (&/V &/$Some ebound))
-
-                         (&/$Left _)
-                         (return* state &/None$)))
-              abound (fn [state]
-                       (|case ((deref ?aid) state)
-                         (&/$Right state* abound)
-                         (return* state* (&/V &/$Some abound))
-
-                         (&/$Left _)
-                         (return* state &/None$)))]
-          (|case [ebound abound]
-            [(&/$None _) (&/$None _)]
-            (|do [_ (set-var ?eid actual)]
-              (return (&/T fixpoints nil)))
-            
-            [(&/$Some etype) (&/$None _)]
-            (check* class-loader fixpoints invariant?? etype actual)
-
-            [(&/$None _) (&/$Some atype)]
-            (check* class-loader fixpoints invariant?? expected atype)
-
-            [(&/$Some etype) (&/$Some atype)]
-            (check* class-loader fixpoints invariant?? etype atype))))
-      
-      [(&/$VarT ?id) _]
-      (fn [state]
-        (|case ((set-var ?id actual) state)
-          (&/$Right state* _)
-          (return* state* (&/T fixpoints nil))
-
-          (&/$Left _)
-          ((|do [bound (deref ?id)]
-             (check* class-loader fixpoints invariant?? bound actual))
-           state)))
-      
-      [_ (&/$VarT ?id)]
-      (fn [state]
-        (|case ((set-var ?id expected) state)
-          (&/$Right state* _)
-          (return* state* (&/T fixpoints nil))
-
-          (&/$Left _)
-          ((|do [bound (deref ?id)]
-             (check* class-loader fixpoints invariant?? expected bound))
-           state)))
-
-      [(&/$AppT (&/$ExT eid) eA) (&/$AppT (&/$ExT aid) aA)]
-      (if (= eid aid)
-        (check* class-loader fixpoints invariant?? eA aA)
-        (fail (check-error expected actual)))
-
-      [(&/$AppT (&/$VarT ?id) A1) (&/$AppT F2 A2)]
-      (fn [state]
-        (|case ((|do [F1 (deref ?id)]
-                  (check* class-loader fixpoints invariant?? (App$ F1 A1) actual))
-                state)
-          (&/$Right state* output)
-          (return* state* output)
-
-          (&/$Left _)
-          ((|do [[fixpoints* _] (check* class-loader fixpoints invariant?? (Var$ ?id) F2)
-                 e* (apply-type F2 A1)
-                 a* (apply-type F2 A2)
-                 [fixpoints** _] (check* class-loader fixpoints* invariant?? e* a*)]
-             (return (&/T fixpoints** nil)))
-           state)))
-      
-      [(&/$AppT F1 A1) (&/$AppT (&/$VarT ?id) A2)]
-      (fn [state]
-        (|case ((|do [F2 (deref ?id)]
-                  (check* class-loader fixpoints invariant?? expected (App$ F2 A2)))
-                state)
-          (&/$Right state* output)
-          (return* state* output)
-
-          (&/$Left _)
-          ((|do [[fixpoints* _] (check* class-loader fixpoints invariant?? F1 (Var$ ?id))
-                 e* (apply-type F1 A1)
-                 a* (apply-type F1 A2)
-                 [fixpoints** _] (check* class-loader fixpoints* invariant?? e* a*)]
-             (return (&/T fixpoints** nil)))
-           state)))
-      
-      [(&/$AppT F A) _]
-      (let [fp-pair (&/T expected actual)
-            _ (when (> (&/|length fixpoints) 40)
-                (println 'FIXPOINTS (->> (&/|keys fixpoints)
-                                         (&/|map (fn [pair]
-                                                   (|let [[e a] pair]
-                                                     (str (show-type e) ":+:"
-                                                          (show-type a)))))
-                                         (&/|interpose "\n\n")
-                                         (&/fold str "")))
-                (assert false (prn-str 'check* '[(&/$AppT F A) _] (&/|length fixpoints) (show-type expected) (show-type actual))))]
-        (|case (fp-get fp-pair fixpoints)
-          (&/$Some ?)
-          (if ?
-            (return (&/T fixpoints nil))
-            (fail (check-error expected actual)))
-
-          (&/$None)
-          (|do [expected* (apply-type F A)]
-            (check* class-loader (fp-put fp-pair true fixpoints) invariant?? expected* actual))))
-
-      [_ (&/$AppT F A)]
-      (|do [actual* (apply-type F A)]
-        (check* class-loader fixpoints invariant?? expected actual*))
-
-      [(&/$UnivQ _) _]
-      (|do [$arg existential
-            expected* (apply-type expected $arg)]
-        (check* class-loader fixpoints invariant?? expected* actual))
-      
-      [_ (&/$UnivQ _)]
-      (with-var
-        (fn [$arg]
-          (|do [actual* (apply-type actual $arg)]
-            (check* class-loader fixpoints invariant?? expected actual*))))
-
-      [(&/$ExQ e!env e!def) _]
-      (with-var
-        (fn [$arg]
-          (|let [expected* (beta-reduce (->> e!env
-                                             (&/Cons$ $arg)
-                                             (&/Cons$ expected))
-                                        e!def)]
-            (check* class-loader fixpoints invariant?? expected* actual))))
-
-      [_ (&/$ExQ a!env a!def)]
-      (|do [$arg existential]
-        (|let [actual* (beta-reduce (->> a!env
-                                         (&/Cons$ $arg)
-                                         (&/Cons$ expected))
-                                    a!def)]
-          (check* class-loader fixpoints invariant?? expected actual*)))
-
-      [(&/$DataT e!data) (&/$DataT a!data)]
-      (&&host/check-host-types (partial check* class-loader fixpoints true)
-                               check-error
-                               fixpoints
-                               existential
-                               class-loader
-                               invariant??
-                               e!data
-                               a!data)
-
-      [(&/$LambdaT eI eO) (&/$LambdaT aI aO)]
-      (|do [[fixpoints* _] (check* class-loader fixpoints invariant?? aI eI)]
-        (check* class-loader fixpoints* invariant?? eO aO))
-
-      [(&/$TupleT e!members) (&/$TupleT a!members)]
-      (|do [fixpoints* (&/fold2% (fn [fp e a]
-                                   (|do [[fp* _] (check* class-loader fp invariant?? e a)]
-                                     (return fp*)))
-                                 fixpoints
-                                 e!members a!members)]
-        (return (&/T fixpoints* nil)))
-      
-      [_ (&/$VariantT (&/$Nil))]
-      (return (&/T fixpoints nil))
-
-      [(&/$VariantT e!cases) (&/$VariantT a!cases)]
-      (|do [fixpoints* (&/fold2% (fn [fp e a]
-                                   (|do [[fp* _] (check* class-loader fp invariant?? e a)]
-                                     (return fp*)))
+    (&/with-attempt
+      (|case [expected actual]
+        [(&/$VarT ?eid) (&/$VarT ?aid)]
+        (if (.equals ^Object ?eid ?aid)
+          (return (&/T fixpoints nil))
+          (|do [ebound (fn [state]
+                         (|case ((deref ?eid) state)
+                           (&/$Right state* ebound)
+                           (return* state* (&/V &/$Some ebound))
+
+                           (&/$Left _)
+                           (return* state &/None$)))
+                abound (fn [state]
+                         (|case ((deref ?aid) state)
+                           (&/$Right state* abound)
+                           (return* state* (&/V &/$Some abound))
+
+                           (&/$Left _)
+                           (return* state &/None$)))]
+            (|case [ebound abound]
+              [(&/$None _) (&/$None _)]
+              (|do [_ (set-var ?eid actual)]
+                (return (&/T fixpoints nil)))
+              
+              [(&/$Some etype) (&/$None _)]
+              (check* class-loader fixpoints invariant?? etype actual)
+
+              [(&/$None _) (&/$Some atype)]
+              (check* class-loader fixpoints invariant?? expected atype)
+
+              [(&/$Some etype) (&/$Some atype)]
+              (check* class-loader fixpoints invariant?? etype atype))))
+        
+        [(&/$VarT ?id) _]
+        (fn [state]
+          (|case ((set-var ?id actual) state)
+            (&/$Right state* _)
+            (return* state* (&/T fixpoints nil))
+
+            (&/$Left _)
+            ((|do [bound (deref ?id)]
+               (check* class-loader fixpoints invariant?? bound actual))
+             state)))
+        
+        [_ (&/$VarT ?id)]
+        (fn [state]
+          (|case ((set-var ?id expected) state)
+            (&/$Right state* _)
+            (return* state* (&/T fixpoints nil))
+
+            (&/$Left _)
+            ((|do [bound (deref ?id)]
+               (check* class-loader fixpoints invariant?? expected bound))
+             state)))
+
+        [(&/$AppT (&/$ExT eid) eA) (&/$AppT (&/$ExT aid) aA)]
+        (if (= eid aid)
+          (check* class-loader fixpoints invariant?? eA aA)
+          (fail (check-error expected actual)))
+
+        [(&/$AppT (&/$VarT ?id) A1) (&/$AppT F2 A2)]
+        (fn [state]
+          (|case ((|do [F1 (deref ?id)]
+                    (check* class-loader fixpoints invariant?? (App$ F1 A1) actual))
+                  state)
+            (&/$Right state* output)
+            (return* state* output)
+
+            (&/$Left _)
+            ((|do [[fixpoints* _] (check* class-loader fixpoints invariant?? (Var$ ?id) F2)
+                   e* (apply-type F2 A1)
+                   a* (apply-type F2 A2)
+                   [fixpoints** _] (check* class-loader fixpoints* invariant?? e* a*)]
+               (return (&/T fixpoints** nil)))
+             state)))
+        
+        [(&/$AppT F1 A1) (&/$AppT (&/$VarT ?id) A2)]
+        (fn [state]
+          (|case ((|do [F2 (deref ?id)]
+                    (check* class-loader fixpoints invariant?? expected (App$ F2 A2)))
+                  state)
+            (&/$Right state* output)
+            (return* state* output)
+
+            (&/$Left _)
+            ((|do [[fixpoints* _] (check* class-loader fixpoints invariant?? F1 (Var$ ?id))
+                   e* (apply-type F1 A1)
+                   a* (apply-type F1 A2)
+                   [fixpoints** _] (check* class-loader fixpoints* invariant?? e* a*)]
+               (return (&/T fixpoints** nil)))
+             state)))
+        
+        [(&/$AppT F A) _]
+        (let [fp-pair (&/T expected actual)
+              _ (when (> (&/|length fixpoints) 40)
+                  (println 'FIXPOINTS (->> (&/|keys fixpoints)
+                                           (&/|map (fn [pair]
+                                                     (|let [[e a] pair]
+                                                       (str (show-type e) ":+:"
+                                                            (show-type a)))))
+                                           (&/|interpose "\n\n")
+                                           (&/fold str "")))
+                  (assert false (prn-str 'check* '[(&/$AppT F A) _] (&/|length fixpoints) (show-type expected) (show-type actual))))]
+          (|case (fp-get fp-pair fixpoints)
+            (&/$Some ?)
+            (if ?
+              (return (&/T fixpoints nil))
+              (fail (check-error expected actual)))
+
+            (&/$None)
+            (|do [expected* (apply-type F A)]
+              (check* class-loader (fp-put fp-pair true fixpoints) invariant?? expected* actual))))
+
+        [_ (&/$AppT F A)]
+        (|do [actual* (apply-type F A)]
+          (check* class-loader fixpoints invariant?? expected actual*))
+
+        [(&/$UnivQ _) _]
+        (|do [$arg existential
+              expected* (apply-type expected $arg)]
+          (check* class-loader fixpoints invariant?? expected* actual))
+        
+        [_ (&/$UnivQ _)]
+        (with-var
+          (fn [$arg]
+            (|do [actual* (apply-type actual $arg)]
+              (check* class-loader fixpoints invariant?? expected actual*))))
+
+        [(&/$ExQ e!env e!def) _]
+        (with-var
+          (fn [$arg]
+            (|let [expected* (beta-reduce (->> e!env
+                                               (&/Cons$ $arg)
+                                               (&/Cons$ expected))
+                                          e!def)]
+              (check* class-loader fixpoints invariant?? expected* actual))))
+
+        [_ (&/$ExQ a!env a!def)]
+        (|do [$arg existential]
+          (|let [actual* (beta-reduce (->> a!env
+                                           (&/Cons$ $arg)
+                                           (&/Cons$ expected))
+                                      a!def)]
+            (check* class-loader fixpoints invariant?? expected actual*)))
+
+        [(&/$DataT e!data) (&/$DataT a!data)]
+        (&&host/check-host-types (partial check* class-loader fixpoints true)
+                                 check-error
                                  fixpoints
-                                 e!cases a!cases)]
-        (return (&/T fixpoints* nil)))
-
-      [(&/$ExT e!id) (&/$ExT a!id)]
-      (if (.equals ^Object e!id a!id)
+                                 existential
+                                 class-loader
+                                 invariant??
+                                 e!data
+                                 a!data)
+
+        [(&/$LambdaT eI eO) (&/$LambdaT aI aO)]
+        (|do [[fixpoints* _] (check* class-loader fixpoints invariant?? aI eI)]
+          (check* class-loader fixpoints* invariant?? eO aO))
+
+        [(&/$TupleT e!members) (&/$TupleT a!members)]
+        (|do [fixpoints* (&/fold2% (fn [fp e a]
+                                     (|do [[fp* _] (check* class-loader fp invariant?? e a)]
+                                       (return fp*)))
+                                   fixpoints
+                                   e!members a!members)]
+          (return (&/T fixpoints* nil)))
+        
+        [_ (&/$VariantT (&/$Nil))]
         (return (&/T fixpoints nil))
-        (fail (check-error expected actual)))
 
-      [(&/$NamedT ?ename ?etype) _]
-      (check* class-loader fixpoints invariant?? ?etype actual)
-
-      [_ (&/$NamedT ?aname ?atype)]
-      (check* class-loader fixpoints invariant?? expected ?atype)
-
-      [_ _]
-      (fail (check-error expected actual))
-      )))
+        [(&/$VariantT e!cases) (&/$VariantT a!cases)]
+        (|do [fixpoints* (&/fold2% (fn [fp e a]
+                                     (|do [[fp* _] (check* class-loader fp invariant?? e a)]
+                                       (return fp*)))
+                                   fixpoints
+                                   e!cases a!cases)]
+          (return (&/T fixpoints* nil)))
+
+        [(&/$ExT e!id) (&/$ExT a!id)]
+        (if (.equals ^Object e!id a!id)
+          (return (&/T fixpoints nil))
+          (fail (check-error expected actual)))
+
+        [(&/$NamedT ?ename ?etype) _]
+        (check* class-loader fixpoints invariant?? ?etype actual)
+
+        [_ (&/$NamedT ?aname ?atype)]
+        (check* class-loader fixpoints invariant?? expected ?atype)
+
+        [_ _]
+        (fail ""))
+      (fn [err]
+        (fail (check-error expected actual))))))
 
 (defn check [expected actual]
   (|do [class-loader &/loader