- |do bindings are now based on pattern matching (that way, tuple destructuring can be done at do).

- Patterns are no longer put inside a MatchAC structure, but are instead just moved around as lists.
- Code outside of &type can no longer create/delete type-vars directly, but must now rely on with-var & with-vars to manage the life-cycle of type-vars.
- Simplified pattern-matching analysis at lux/analyser/case.
- The LEFT_APP optimization in check* has been replicated on the other side as RIGHT_APP, to attempt to improve performance of pattern-matching.

10 files changed, 366 insertions, 374 deletions

diff --git a/src/lux/analyser.clj b/src/lux/analyser.clj
index 14d5599e4..7f65c6476 100644
--- a/src/lux/analyser.clj
+++ b/src/lux/analyser.clj
@@ -436,7 +436,7 @@
     [["lux;Meta" [meta ["lux;Form" ["lux;Cons" [?fn ?args]]]]]]
     (fn [state]
       ;; (prn '(&/show-ast ?fn) (&/show-ast ?fn))
-      (matchv ::M/objects [((&&/with-var #(&&/analyse-1 (partial analyse-ast eval!) % ?fn)) state)]
+      (matchv ::M/objects [((&type/with-var #(&&/analyse-1 (partial analyse-ast eval!) % ?fn)) state)]
         [["lux;Right" [state* =fn]]]
         ((&&lux/analyse-apply (partial analyse-ast eval!) exo-type =fn ?args) state*)
 
diff --git a/src/lux/analyser/base.clj b/src/lux/analyser/base.clj
index 35c12c3e0..9acd37028 100644
--- a/src/lux/analyser/base.clj
+++ b/src/lux/analyser/base.clj
@@ -1,7 +1,7 @@
 (ns lux.analyser.base
   (:require [clojure.core.match :as M :refer [match matchv]]
             clojure.core.match.array
-            (lux [base :as & :refer [|do return fail]]
+            (lux [base :as & :refer [|let |do return fail]]
                  [type :as &type])))
 
 ;; [Resources]
@@ -36,22 +36,9 @@
           [_]
           (fail "[Analyser Error] Can't expand to other than 2 elements.")))))
 
-(defn with-var [k]
-  (|do [=var &type/create-var
-        =ret (k =var)]
-    (matchv ::M/objects [=ret]
-      [["Expression" [?expr ?type]]]
-      (|do [id (&type/var-id =var)
-            =type (&type/clean id ?type)
-            :let [_ (prn 'with-var/CLEANING id)]
-            _ (&type/delete-var id)]
-        (return (&/V "Expression" (&/T ?expr =type))))
-
-      [_]
-      (assert false (pr-str '&&/with-var (aget =ret 0))))))
-
-(defmacro with-vars [vars body]
-  (reduce (fn [b v]
-            `(with-var (fn [~v] ~b)))
-          body
-          (reverse vars)))
+(defn resolved-ident [ident]
+  (|let [[?module ?name] ident]
+    (|do [module* (if (= "" ?module)
+                    &/get-module-name
+                    (return ?module))]
+      (return (&/ident->text (&/T module* ?name))))))
diff --git a/src/lux/analyser/case.clj b/src/lux/analyser/case.clj
index 74d5ea5a3..7a0fbe510 100644
--- a/src/lux/analyser/case.clj
+++ b/src/lux/analyser/case.clj
@@ -17,149 +17,111 @@
     [_]
     (&type/actual-type type)))
 
-(defn ^:private variant-case [case type]
-  (matchv ::M/objects [type]
-    [["lux;VariantT" ?cases]]
-    (if-let [case-type (&/|get case ?cases)]
-      (return case-type)
-      (fail (str "[Pattern-maching error] Variant lacks case: " case)))
-
-    [_]
-    (fail "[Pattern-maching error] Type is not a variant.")))
-
-(defn ^:private analyse-variant [analyse-pattern idx value-type tag value]
-  (|do [[idx* test] (analyse-pattern idx value-type value)]
-    (return (&/T idx* (&/V "VariantTestAC" (&/T tag test))))))
-
-(defn ^:private analyse-pattern [idx value-type pattern]
+(defn ^:private analyse-pattern [value-type pattern kont]
   ;; (prn 'analyse-pattern/pattern (aget pattern 0) (aget pattern 1) (alength (aget pattern 1)))
   (matchv ::M/objects [pattern]
     [["lux;Meta" [_ pattern*]]]
     ;; (assert false)
-    (do ;; (prn 'analyse-pattern/pattern* (aget pattern* 0))
-        ;; (when (= "lux;Form" (aget pattern* 0))
-        ;;   (prn 'analyse-pattern/_2 (aget pattern* 1 0)) ;; "lux;Cons"
-        ;;   (prn 'analyse-pattern/_2 (aget pattern* 1 1 0 0)) ;; "lux;Meta"
-        ;;   (prn 'analyse-pattern/_2 (alength (aget pattern* 1 1 0 1)))
-        ;;   (prn 'analyse-pattern/_2 (aget pattern* 1 1 0 1 1 0)) ;; "lux;Tag"
-        ;;   (prn 'analyse-pattern/_2 [(aget pattern* 1 1 0 1 1 1 0) (aget pattern* 1 1 0 1 1 1 1)]) ;; ["" "Cons"]
-        ;;   (prn 'analyse-pattern/_2 (aget pattern* 1 1 1 0)) ;; "lux;Cons"
-        ;;   (prn 'analyse-pattern/_2 (aget pattern* 1 1 1 1 0)) ;; #<Object[] [Ljava.lang.Object;@63c7c38b>
-        ;;   (prn 'analyse-pattern/_2 (aget pattern* 1 1 1 1 1 0)) ;; "lux;Nil"
-        ;;   )
-        ;; ["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Tag" [?module ?name]]]]
-        ;;                          ["lux;Cons" [?value
-        ;;                                       ["lux;Nil" _]]]]]]
-        (matchv ::M/objects [pattern*]
-          [["lux;Symbol" [?module ?name]]]
-          (return (&/T (inc idx) (&/V "StoreTestAC" (&/T idx (str ?module ";" ?name) value-type))))
-
-          [["lux;Bool" ?value]]
-          (|do [_ (&type/check value-type &type/Bool)]
-            (return (&/T idx (&/V "BoolTestAC" ?value))))
-
-          [["lux;Int" ?value]]
-          (|do [_ (&type/check value-type &type/Int)]
-            (return (&/T idx (&/V "IntTestAC" ?value))))
-
-          [["lux;Real" ?value]]
-          (|do [_ (&type/check value-type &type/Real)]
-            (return (&/T idx (&/V "RealTestAC" ?value))))
-
-          [["lux;Char" ?value]]
-          (|do [_ (&type/check value-type &type/Char)]
-            (return (&/T idx (&/V "CharTestAC" ?value))))
-
-          [["lux;Text" ?value]]
-          (|do [_ (&type/check value-type &type/Text)]
-            (return (&/T idx (&/V "TextTestAC" ?value))))
-
-          [["lux;Tuple" ?members]]
-          (|do [=vars (&/map% (constantly &type/create-var) ?members)
-                _ (&type/check value-type (&/V "lux;TupleT" =vars))
-                [idx* tests] (&/fold% (fn [idx+subs mv]
-                                        (|let [[_idx subs] idx+subs
-                                               [?member ?var] mv]
-                                          (|do [[idx* test] (analyse-pattern _idx ?var ?member)]
-                                            (return (&/T idx* (&/|cons test subs))))))
-                                      (&/T idx (&/|list))
-                                      (&/zip2 ?members =vars))]
-            (return (&/T idx* (&/V "TupleTestAC" (&/|reverse tests)))))
-          
-          [["lux;Record" ?fields]]
-          (|do [=vars (&/map% (constantly &type/create-var) ?fields)
-                _ (&type/check value-type (&/V "lux;RecordT" (&/zip2 (&/|keys ?fields) =vars)))
-                tests (&/fold% (fn [idx+subs mv]
-                                 (|let [[_idx subs] idx+subs
-                                        [[slot value] ?var] mv]
-                                   (|do [[idx* test] (analyse-pattern _idx ?var value)]
-                                     (return (&/T idx* (&/|cons (&/T slot test) subs))))))
-                               (&/T idx (&/|list)) (&/zip2 ?fields =vars))]
-            (return (&/V "RecordTestAC" tests)))
-
-          [["lux;Tag" [?module ?name]]]
-          (|do [module* (if (= "" ?module)
-                          &/get-module-name
-                          (return ?module))
-                :let [=tag (str module* ";" ?name)]
-                value-type* (resolve-type value-type)
-                case-type (variant-case =tag value-type*)]
-            (analyse-variant analyse-pattern idx case-type =tag (&/V "lux;Meta" (&/T (&/T "" -1 -1)
-                                                                                     (&/V "lux;Tuple" (&/|list))))))
-
-          [["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Tag" [?module ?name]]]]
-                                    ["lux;Cons" [?value
-                                                 ["lux;Nil" _]]]]]]]
-          (|do [module* (if (= "" ?module)
-                          &/get-module-name
-                          (return ?module))
-                :let [=tag (str module* ";" ?name)]
-                value-type* (resolve-type value-type)
-                case-type (variant-case =tag value-type*)]
-            (analyse-variant analyse-pattern idx case-type =tag ?value))
-          ))
-    ))
-
-(defn ^:private with-test [test body]
-  (matchv ::M/objects [test]
-    [["StoreTestAC" [?idx ?name ?type]]]
-    (&env/with-local ?name ?type
-      body)
-
-    [["TupleTestAC" ?tests]]
-    (&/fold #(with-test %2 %1) body (&/|reverse ?tests))
-
-    [["RecordTestAC" ?tests]]
-    (&/fold #(with-test %2 %1) body (&/|reverse (&/|vals ?tests)))
-
-    [["VariantTestAC" [?tag ?value]]]
-    (with-test ?value body)
-    
-    [_]
-    body
-    ))
-
-(defn ^:private analyse-branch [analyse exo-type value-type pattern body match]
-  (|do [idx &env/next-local-idx
-        [idx* =test] (analyse-pattern idx value-type pattern)
-        =body (with-test =test
-                (&&/analyse-1 analyse exo-type body))]
-    (matchv ::M/objects [match]
-      [["MatchAC" ?patterns]]
-      (return (&/V "MatchAC" (&/|cons (&/T =test =body) ?patterns))))))
+    (matchv ::M/objects [pattern*]
+      [["lux;Symbol" ?ident]]
+      (|do [=kont (&env/with-local (&/ident->text ?ident) value-type
+                    kont)
+            idx &env/next-local-idx]
+        (return (&/T (&/V "StoreTestAC" idx) =kont)))
+
+      [["lux;Bool" ?value]]
+      (|do [_ (&type/check value-type &type/Bool)
+            =kont kont]
+        (return (&/T (&/V "BoolTestAC" ?value) =kont)))
+
+      [["lux;Int" ?value]]
+      (|do [=kont kont
+            _ (&type/check value-type &type/Int)]
+        (return (&/T (&/V "IntTestAC" ?value) =kont)))
+
+      [["lux;Real" ?value]]
+      (|do [=kont kont
+            _ (&type/check value-type &type/Real)]
+        (return (&/T (&/V "RealTestAC" ?value) =kont)))
+
+      [["lux;Char" ?value]]
+      (|do [=kont kont
+            _ (&type/check value-type &type/Char)]
+        (return (&/T (&/V "CharTestAC" ?value) =kont)))
+
+      [["lux;Text" ?value]]
+      (|do [=kont kont
+            _ (&type/check value-type &type/Text)]
+        (return (&/T (&/V "TextTestAC" ?value) =kont)))
+
+      [["lux;Tuple" ?members]]
+      (&type/with-vars (&/|length ?members)
+        (fn [=vars]
+          (|do [_ (&type/check value-type (&/V "lux;TupleT" =vars))
+                [=tests =kont] (&/fold (fn [kont* vm]
+                                         (|let [[v m] vm]
+                                           (|do [[=test [=tests =kont]] (analyse-pattern v m kont*)]
+                                             (matchv ::M/objects [=kont]
+                                               [["Expression" [?val ?type]]]
+                                               (|do [=type (&type/clean v ?type)]
+                                                 (return (&/T (&/|cons =test =tests)
+                                                              (&/V "Expression" (&/T ?val =type)))))))))
+                                       (|do [=kont kont]
+                                         (return (&/T (&/|list) =kont)))
+                                       (&/|reverse (&/zip2 =vars ?members)))]
+            (return (&/T (&/V "TupleTestAC" =tests) =kont)))))
+
+      [["lux;Record" ?fields]]
+      (&type/with-vars (&/|length ?fields)
+        (fn [=vars]
+          (|do [_ (&type/check value-type (&/V "lux;RecordT" (&/zip2 (&/|keys ?fields) =vars)))
+                [=tests =kont] (&/fold (fn [kont* vm]
+                                         (|let [[v [k m]] vm]
+                                           (|do [[=test [=tests =kont]] (analyse-pattern v m kont*)]
+                                             (matchv ::M/objects [=kont]
+                                               [["Expression" [?val ?type]]]
+                                               (|do [=type (&type/clean v ?type)]
+                                                 (return (&/T (&/|put k =test =tests)
+                                                              (&/V "Expression" (&/T ?val =type)))))))))
+                                       (|do [=kont kont]
+                                         (return (&/T (&/|table) =kont)))
+                                       (&/|reverse (&/zip2 =vars ?fields)))]
+            (return (&/T (&/V "RecordTestAC" =tests) =kont)))))
+
+      [["lux;Tag" ?ident]]
+      (|do [=tag (&&/resolved-ident ?ident)
+            value-type* (resolve-type value-type)
+            case-type (&type/variant-case =tag value-type*)
+            [=test =kont] (analyse-pattern case-type (&/V "lux;Meta" (&/T (&/T "" -1 -1)
+                                                                          (&/V "lux;Tuple" (&/|list))))
+                                           kont)]
+        (return (&/T (&/V "VariantTestAC" (&/T =tag =test)) =kont)))
+
+      [["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Tag" ?ident]]]
+                                ["lux;Cons" [?value
+                                             ["lux;Nil" _]]]]]]]
+      (|do [=tag (&&/resolved-ident ?ident)
+            value-type* (resolve-type value-type)
+            case-type (&type/variant-case =tag value-type*)
+            [=test =kont] (analyse-pattern case-type ?value
+                                           kont)]
+        (return (&/T (&/V "VariantTestAC" (&/T =tag =test)) =kont)))
+      )))
+
+(defn ^:private analyse-branch [analyse exo-type value-type pattern body patterns]
+  (|do [pattern+body (analyse-pattern value-type pattern
+                                      (&&/analyse-1 analyse exo-type body))]
+    (return (&/|cons pattern+body patterns))))
 
 (let [compare-kv #(compare (aget %1 0) (aget %2 0))]
   (defn ^:private merge-total [struct test+body]
-    ;; (prn 'merge-total (aget struct 0) (class test+body))
-    ;; (prn 'merge-total (aget struct 0) (aget test+body 0))
-    ;; (prn 'merge-total (aget struct 0) (aget test+body 0 0))
     (matchv ::M/objects [test+body]
       [[test ?body]]
       (matchv ::M/objects [struct test]
-        [["DefaultTotal" total?] ["StoreTestAC" [?idx ?name type]]]
+        [["DefaultTotal" total?] ["StoreTestAC" ?idx]]
         (return (&/V "DefaultTotal" true))
 
-        [[?tag [total? ?values]] ["StoreTestAC" [?idx ?name type]]]
+        [[?tag [total? ?values]] ["StoreTestAC" ?idx]]
         (return (&/V ?tag (&/T true ?values)))
         
         [["DefaultTotal" total?] ["BoolTestAC" ?value]]
@@ -239,92 +201,86 @@
           (return (&/V "VariantTotal" (&/T total? (&/|put ?tag struct ?branches)))))
         ))))
 
-(defn ^:private totality-struct [owner-total? match]
-  (let [msg "Pattern matching is non-total"]
-    (matchv ::M/objects [match]
-      [["MatchAC" ?tests]]
-      (&/fold% merge-total (&/V "DefaultTotal" false) ?tests))))
-
 (defn ^:private check-totality [value-type struct]
   (prn 'check-totality (aget value-type 0) (aget struct 0) (&type/show-type value-type))
   (matchv ::M/objects [struct]
     [["BoolTotal" [?total _]]]
-    (|do [_ (&type/check value-type &type/Bool)]
-      (return ?total))
+    (return ?total)
 
     [["IntTotal" [?total _]]]
-    (|do [_ (&type/check value-type &type/Int)]
-      (return ?total))
+    (return ?total)
 
     [["RealTotal" [?total _]]]
-    (|do [_ (&type/check value-type &type/Real)]
-      (return ?total))
+    (return ?total)
 
     [["CharTotal" [?total _]]]
-    (|do [_ (&type/check value-type &type/Char)]
-      (return ?total))
+    (return ?total)
 
     [["TextTotal" [?total _]]]
-    (|do [_ (&type/check value-type &type/Text)]
-      (return ?total))
+    (return ?total)
 
     [["TupleTotal" [?total ?structs]]]
-    (|do [elems-vars (&/map% (constantly &type/create-var) ?structs)
-          _ (&type/check value-type (&/V "lux;TupleT" elems-vars))
-          totals (&/map% (fn [sv]
-                           (|let [[sub-struct tvar] sv]
-                             (check-totality tvar sub-struct)))
-                         (&/zip2 ?structs elems-vars))]
-      (return (or ?total
-                  (every? true? totals))))
+    (if ?total
+      (return true)
+      (|do [value-type* (resolve-type value-type)]
+        (matchv ::M/objects [value-type*]
+          [["lux;TupleT" ?members]]
+          (|do [totals (&/map% (fn [sv]
+                                 (|let [[sub-struct ?member] sv]
+                                   (check-totality ?member sub-struct)))
+                               (&/zip2 ?structs ?members))]
+            (return (&/fold #(and %1 %2) true totals)))
+
+          [_]
+          (fail ""))))
 
     [["RecordTotal" [?total ?structs]]]
-    (|do [elems-vars (&/map% (constantly &type/create-var) ?structs)
-          :let [structs+vars (&/zip2 ?structs elems-vars)
-                record-type (&/V "lux;RecordT" (&/|map (fn [sv]
-                                                         (|let [[[k v] tvar] sv]
-                                                           (&/T k tvar)))
-                                                       structs+vars))]
-          _ (&type/check value-type record-type)
-          totals (&/map% (fn [sv]
-                           (|let [[[k v] tvar] sv]
-                             (check-totality tvar v)))
-                         structs+vars)]
-      (return (or ?total
-                  (every? true? totals))))
+    (if ?total
+      (return true)
+      (|do [value-type* (resolve-type value-type)]
+        (matchv ::M/objects [value-type*]
+          [["lux;RecordT" ?fields]]
+          (|do [totals (&/map% (fn [field]
+                                 (|let [[?tk ?tv] field]
+                                   (if-let [sub-struct (&/|get ?tk ?structs)]
+                                     (check-totality ?tv sub-struct)
+                                     (return false))))
+                               ?fields)]
+            (return (&/fold #(and %1 %2) true totals)))
+
+          [_]
+          (fail ""))))
 
     [["VariantTotal" [?total ?structs]]]
-    (&/try-all% (&/|list (|do [real-type (resolve-type value-type)
-                               :let [_ (prn 'real-type/_1 (&type/show-type real-type))]
-                               veredicts (matchv ::M/objects [real-type]
-                                           [["lux;VariantT" ?cases]]
-                                           (&/map% (fn [case]
-                                                     (|let [[ctag ctype] case]
-                                                       (if-let [sub-struct (&/|get ctag ?structs)]
-                                                         (check-totality ctype sub-struct)
-                                                         (return ?total))))
-                                                   ?cases)
-
-                                           [_]
-                                           (fail "[Pattern-maching error] Value is not a variant."))]
-                           (return (&/fold #(and %1 %2) ?total veredicts)))
-                         (fail "[Pattern-maching error] Can't pattern-match on an unknown variant type.")))
+    (if ?total
+      (return true)
+      (|do [value-type* (resolve-type value-type)]
+        (matchv ::M/objects [value-type*]
+          [["lux;VariantT" ?cases]]
+          (|do [totals (&/map% (fn [case]
+                                 (|let [[?tk ?tv] case]
+                                   (if-let [sub-struct (&/|get ?tk ?structs)]
+                                     (check-totality ?tv sub-struct)
+                                     (return false))))
+                               ?cases)]
+            (return (&/fold #(and %1 %2) true totals)))
+
+          [_]
+          (fail ""))))
     
-    [["DefaultTotal" true]]
-    (return true)
+    [["DefaultTotal" ?total]]
+    (return ?total)
     ))
 
 ;; [Exports]
 (defn analyse-branches [analyse exo-type value-type branches]
-  (|do [=match (&/fold% (fn [match branch]
-                          (|let [[pattern body] branch]
-                            (analyse-branch analyse exo-type value-type pattern body match)))
-                        (&/V "MatchAC" (&/|list))
-                        branches)
-        struct (totality-struct false =match)
+  (|do [patterns (&/fold% (fn [patterns branch]
+                            (|let [[pattern body] branch]
+                              (analyse-branch analyse exo-type value-type pattern body patterns)))
+                          (&/|list)
+                          branches)
+        struct (&/fold% merge-total (&/V "DefaultTotal" false) patterns)
         ? (check-totality value-type struct)]
-    (matchv ::M/objects [=match]
-      [["MatchAC" ?tests]]
-      (if ?
-        (return (&/V "MatchAC" (&/|reverse ?tests)))
-        (fail "[Pattern-maching error] Pattern-matching is non-total.")))))
+    (if ?
+      (return (&/|reverse patterns))
+      (fail "[Pattern-maching error] Pattern-matching is non-total."))))
diff --git a/src/lux/analyser/env.clj b/src/lux/analyser/env.clj
index 454d8ad6c..a083801ed 100644
--- a/src/lux/analyser/env.clj
+++ b/src/lux/analyser/env.clj
@@ -10,7 +10,7 @@
     (return* state (->> state (&/get$ "lux;local-envs") &/|head (&/get$ "lux;locals") (&/get$ "lux;counter")))))
 
 (defn with-local [name type body]
-  (prn 'with-local name)
+  ;; (prn 'with-local name)
   (fn [state]
     (let [old-mappings (->> state (&/get$ "lux;local-envs") &/|head (&/get$ "lux;locals") (&/get$ "lux;mappings"))
           =return (body (&/update$ "lux;local-envs"
diff --git a/src/lux/analyser/host.clj b/src/lux/analyser/host.clj
index 33ceb2b22..404573de4 100644
--- a/src/lux/analyser/host.clj
+++ b/src/lux/analyser/host.clj
@@ -182,8 +182,8 @@
                                                                                                                                                                    ["lux;Nil" _]]]]]]]]]]
                                                                                                  ["lux;Nil" _]]]]]]]]]]]
                               (do ;; (prn 'analyse-jvm-interface ?member-name ?inputs ?output)
-                                  (|do [?inputs (&/map% extract-ident ?inputs)]
-                                    (return [?member-name [?inputs ?output]])))
+                                  (|do [inputs* (&/map% extract-ident ?inputs)]
+                                    (return [?member-name [inputs* ?output]])))
                               
                               [_]
                               (fail "[Analyser Error] Invalid method signature!")))
diff --git a/src/lux/analyser/lux.clj b/src/lux/analyser/lux.clj
index 32f65320a..8e3afb476 100644
--- a/src/lux/analyser/lux.clj
+++ b/src/lux/analyser/lux.clj
@@ -13,26 +13,34 @@
                           [env :as &&env]
                           [def :as &&def])))
 
-(defn ^:private analyse-1+ [analyse]
-  (fn [?token]
-    (&&/with-var #(&&/analyse-1 analyse % ?token))))
+(defn ^:private analyse-1+ [analyse ?token]
+  (&type/with-var
+    (fn [$var]
+      (prn 'analyse-1+ (aget $var 1) (&/show-ast ?token))
+      (|do [=expr (&&/analyse-1 analyse $var ?token)]
+        (matchv ::M/objects [=expr]
+          [["Expression" [?item ?type]]]
+          (|do [=type (&type/clean $var ?type)]
+            (return (&/V "Expression" (&/T ?item =type))))
+          )))))
 
 ;; [Exports]
 (defn analyse-tuple [analyse exo-type ?elems]
   ;; (prn 'analyse-tuple (str "[" (->> ?elems (&/|map &/show-ast) (&/|interpose " ") (&/fold str "")) "]")
   ;;      (&type/show-type exo-type))
-  (|do [members-vars (&/map% (constantly &type/create-var) ?elems)
-        _ (&type/check exo-type (&/V "lux;TupleT" members-vars))
-        =elems (&/map% (fn [ve]
-                         (|let [[=var elem] ve]
-                           (|do [output (&&/analyse-1 analyse =var elem)]
-                             (matchv ::M/objects [output]
-                               [["Expression" [?val ?type]]]
-                               (|do [=val-type (&type/clean =var ?type)]
-                                 (return (&/V "Expression" (&/T ?val exo-type))))))))
-                       (&/zip2 members-vars ?elems))]
-    (return (&/|list (&/V "Expression" (&/T (&/V "tuple" =elems)
-                                            exo-type))))))
+  (&type/with-vars (&/|length ?elems)
+    (fn [=vars]
+      (|do [_ (&type/check exo-type (&/V "lux;TupleT" =vars))
+            =elems (&/map% (fn [ve]
+                             (|let [[=var elem] ve]
+                               (|do [output (&&/analyse-1 analyse =var elem)]
+                                 (matchv ::M/objects [output]
+                                   [["Expression" [?val ?type]]]
+                                   (|do [=type (&type/clean =var ?type)]
+                                     (return (&/V "Expression" (&/T ?val =type))))))))
+                           (&/zip2 =vars ?elems))]
+        (return (&/|list (&/V "Expression" (&/T (&/V "tuple" =elems)
+                                                exo-type))))))))
 
 (defn analyse-variant [analyse exo-type ident ?value]
   (|let [[?module ?name] ident]
@@ -46,8 +54,8 @@
                         [["lux;VarT" ?id]]
                         (|do [? (&type/bound? ?id)]
                           (if ?
-                            (|do [exo-type (&type/deref ?id)]
-                              (&type/actual-type exo-type))
+                            (|do [exo-type* (&type/deref ?id)]
+                              (&type/actual-type exo-type*))
                             (|do [_ (&type/set-var ?id &type/Type)]
                               (&type/actual-type &type/Type))))
 
@@ -112,7 +120,7 @@
                            (return (&/|list global)))
                          state)
             (do (prn (str "((" (->> stack (&/|map show-frame) &/->seq (interpose " ") (reduce str "")) "))"))
-             (fail* (str "[Analyser Error] Unrecognized identifier: " local-ident))))
+              (fail* (str "[Analyser Error] Unrecognized identifier: " local-ident))))
 
           [["lux;Cons" [top-outer _]]]
           (|let [scopes (&/|tail (&/folds #(&/|cons (&/get$ "lux;name" %2) %1)
@@ -127,12 +135,15 @@
                                                   (->> top-outer (&/get$ "lux;closure") (&/get$ "lux;mappings") (&/|get local-ident)))
                                               (&/|list))
                                          (&/zip2 (&/|reverse inner) scopes))]
-            (return* (&/set$ "lux;local-envs" (&/|++ inner* outer) state) (&/|list =local)))
+            (&/run-state (|do [=local-type (&&/expr-type =local)
+                               _ (&type/check exo-type =local-type)]
+                           (return (&/|list =local)))
+                         (&/set$ "lux;local-envs" (&/|++ inner* outer) state)))
           )))
     ))
 
 (defn ^:private analyse-apply* [analyse exo-type =fn ?args]
-  (|do [=args (&/map% (fn [arg] (&&/with-var #(&&/analyse-1 analyse % arg)))
+  (|do [=args (&/map% (fn [arg] (analyse-1+ analyse arg))
                       ?args)
         =fn-type (&&/expr-type =fn)
         [=apply =output-type] (&/fold% (fn [[=fn =fn-type] =input]
@@ -176,12 +187,13 @@
     ))
 
 (defn analyse-case [analyse exo-type ?value ?branches]
+  (prn 'analyse-case 'exo-type (&type/show-type exo-type) (&/show-ast ?value))
   (|do [:let [num-branches (&/|length ?branches)]
         _ (&/assert! (> num-branches 0) "[Analyser Error] Can't have empty branches in \"case'\" expression.")
         _ (&/assert! (even? num-branches) "[Analyser Error] Unbalanced branches in \"case'\" expression.")
-        =value ((analyse-1+ analyse) ?value)
-        :let [_ (prn 'analyse-case/GOT_VALUE)]
+        =value (analyse-1+ analyse ?value)
         =value-type (&&/expr-type =value)
+        :let [_ (prn 'analyse-case/GOT_VALUE (&type/show-type =value-type))]
         =match (&&case/analyse-branches analyse exo-type =value-type (&/|as-pairs ?branches))
         :let [_ (prn 'analyse-case/GOT_MATCH)]]
     (return (&/|list (&/V "Expression" (&/T (&/V "case" (&/T =value =match))
@@ -189,55 +201,67 @@
 
 (defn analyse-lambda* [analyse exo-type ?self ?arg ?body]
   ;; (prn 'analyse-lambda ?self ?arg ?body)
-  (|do [lambda-expr (&&/with-vars [=arg =return]
-                 (|do [:let [_ (prn 'analyse-lambda/_-1 (&type/show-type =arg) (&type/show-type =return))]
-                       :let [=lambda-type* (&/V "lux;LambdaT" (&/T =arg =return))]
-                       :let [_ (prn 'analyse-lambda/_0)]
-                       _ (&type/check exo-type =lambda-type*)
-                       :let [_ (prn 'analyse-lambda/_0.5 (&type/show-type exo-type))]
-                       :let [_ (prn 'analyse-lambda/_1 (&type/show-type =lambda-type*))]
-                       _ (|do [aid (&type/var-id =arg)
-                               atype (&type/deref aid)
-                               rid (&type/var-id =return)
-                               rtype (&type/deref rid)
-                               :let [_ (prn 'analyse-lambda/_1.5 (&type/show-type atype) (&type/show-type rtype))]]
-                           (return nil))
-                       [=scope =captured =body] (&&lambda/with-lambda ?self =lambda-type*
-                                                  ?arg =arg
-                                                  (&&/analyse-1 analyse =return ?body))
-                       :let [_ (prn 'analyse-lambda/_2)]
-                       =lambda-type (matchv ::M/objects [=arg]
-                                      [["lux;VarT" ?id]]
-                                      (|do [? (&type/bound? ?id)]
-                                        (if ?
-                                          (return =lambda-type*)
-                                          (let [var-name (str (gensym ""))]
-                                            (|do [_ (&type/set-var ?id (&/V "lux;BoundT" var-name))]
-                                              (return (&/V "lux;AllT" (&/T (&/|list) "" var-name =lambda-type*)))))))
+  (|do [lambda-expr (&type/with-vars 2
+                 (fn [=vars2]
+                   (matchv ::M/objects [=vars2]
+                     [["lux;Cons" [=arg ["lux;Cons" [=return ["lux;Nil" _]]]]]]
+                     (|do [:let [_ (prn 'analyse-lambda/_-1 (&type/show-type =arg) (&type/show-type =return))]
+                           :let [=lambda-type* (&/V "lux;LambdaT" (&/T =arg =return))]
+                           :let [_ (prn 'analyse-lambda/_0)]
+                           _ (&type/check exo-type =lambda-type*)
+                           :let [_ (prn 'analyse-lambda/_0.5 (&type/show-type exo-type))]
+                           :let [_ (prn 'analyse-lambda/_1 (&type/show-type =lambda-type*))]
+                           ;; _ (|do [aid (&type/var-id =arg)
+                           ;;         atype (&type/deref aid)
+                           ;;         rid (&type/var-id =return)
+                           ;;         rtype (&type/deref rid)
+                           ;;         :let [_ (prn 'analyse-lambda/_1.5 (&type/show-type atype) (&type/show-type rtype))]]
+                           ;;     (return nil))
+                           [=scope =captured =body] (&&lambda/with-lambda ?self =lambda-type*
+                                                      ?arg =arg
+                                                      (&&/analyse-1 analyse =return ?body))
+                           =lambda-type** (&type/clean =return =lambda-type*)
+                           :let [_ (prn 'analyse-lambda/_2)]
+                           =lambda-type (matchv ::M/objects [=arg]
+                                          [["lux;VarT" ?id]]
+                                          (|do [? (&type/bound? ?id)]
+                                            (if ?
+                                              (&type/clean =arg =lambda-type**)
+                                              (let [var-name (str (gensym ""))]
+                                                (|do [_ (&type/set-var ?id (&/V "lux;BoundT" var-name))
+                                                      =lambda-type*** (&type/clean =arg =lambda-type**)]
+                                                  (return (&/V "lux;AllT" (&/T (&/|list) "" var-name =lambda-type***)))))))
 
-                                      [_]
-                                      (fail ""))
-                       :let [_ (prn 'analyse-lambda/_3 (&type/show-type =lambda-type))]]
-                   (return (&/V "Expression" (&/T (&/V "lambda" (&/T =scope =captured =body)) =lambda-type)))))
+                                          [_]
+                                          (fail ""))
+                           :let [_ (prn 'analyse-lambda/_3 (&type/show-type =lambda-type))]]
+                       (return (&/V "Expression" (&/T (&/V "lambda" (&/T =scope =captured =body)) =lambda-type))))
+                     )))
         :let [_ (prn 'analyse-lambda/_4)]]
     (return lambda-expr)))
 
+(defn analyse-lambda** [analyse exo-type ?self ?arg ?body]
+  (prn 'analyse-lambda**/&& (aget exo-type 0))
+  (matchv ::M/objects [exo-type]
+    [["lux;AllT" _]]
+    (&type/with-var
+      (fn [$var]
+        (|do [exo-type* (&type/apply-type exo-type $var)
+              output (analyse-lambda** analyse exo-type* ?self ?arg ?body)]
+          (matchv ::M/objects [output]
+            [["Expression" [?item ?type]]]
+            (|do [=type (&type/clean $var ?type)]
+              (return (&/V "Expression" (&/T ?item =type))))))))
+    
+    [_]
+    (analyse-lambda* analyse exo-type ?self ?arg ?body)))
+
 (defn analyse-lambda [analyse exo-type ?self ?arg ?body]
-  (prn 'analyse-lambda/&& (aget exo-type 0))
-  (|do [output (matchv ::M/objects [exo-type]
-                 [["lux;AllT" _]]
-                 (&&/with-var
-                   (fn [$arg]
-                     (|do [exo-type* (&type/apply-type exo-type $arg)
-                           outputs (analyse-lambda analyse exo-type* ?self ?arg ?body)]
-                       (return (&/|head outputs)))))
-                 
-                 [_]
-                 (analyse-lambda* analyse exo-type ?self ?arg ?body))]
+  (|do [output (analyse-lambda** analyse exo-type ?self ?arg ?body)]
     (return (&/|list output))))
 
 (defn analyse-def [analyse exo-type ?name ?value]
-  ;; (prn 'analyse-def/CODE ?name (&/show-ast ?value))
+  (prn 'analyse-def/CODE ?name (&/show-ast ?value))
   (|do [_ (&type/check exo-type &type/Nothing)
         module-name &/get-module-name
         ? (&&def/defined? module-name ?name)]
@@ -245,8 +269,7 @@
       (fail (str "[Analyser Error] Can't redefine " ?name))
       (|do [:let [_ (prn 'analyse-def/_0)]
             =value (&/with-scope ?name
-                     (&&/with-var
-                       #(&&/analyse-1 analyse % ?value)))
+                     (analyse-1+ analyse ?value))
             :let [_ (prn 'analyse-def/_1)]
             =value-type (&&/expr-type =value)
             :let [_ (prn 'analyse-def/_2)]
@@ -270,7 +293,7 @@
 (defn analyse-check [analyse eval! exo-type ?type ?value]
   (println "analyse-check#0")
   (|do [=type (&&/analyse-1 analyse &type/Type ?type)
-        ;; =type ((analyse-1+ analyse) ?type)
+        ;; =type (analyse-1+ analyse ?type)
         :let [_ (println "analyse-check#1")]
         ==type (eval! =type)
         _ (&type/check exo-type ==type)
diff --git a/src/lux/base.clj b/src/lux/base.clj
index f9d3c9c23..6771c9290 100644
--- a/src/lux/base.clj
+++ b/src/lux/base.clj
@@ -150,7 +150,6 @@
   ;; (prn 'bind m-value step)
   (fn [state]
     (let [inputs (m-value state)]
-      ;; (prn 'bind/inputs (aget inputs 0))
       (matchv ::M/objects [inputs]
         [["lux;Right" [?state ?datum]]]
         (let [next-fn (step ?datum)]
@@ -159,7 +158,11 @@
           (next-fn ?state))
         
         [["lux;Left" _]]
-        inputs))))
+        inputs
+
+        ;; [_]
+        ;; (assert false (pr-str 'bind/inputs (aget inputs 0)))
+        ))))
 
 (defmacro |do [steps return]
   (assert (not= 0 (count steps)) "The steps can't be empty!")
@@ -168,13 +171,13 @@
             (case label
               :let `(|let ~computation ~inner)
               ;; else
-              ;; `(bind ~computation
-              ;;        (fn [val#]
-              ;;          (matchv ::M/objects [val#]
-              ;;            [~label]
-              ;;            ~inner)))
               `(bind ~computation
-                     (fn [~label] ~inner))
+                     (fn [val#]
+                       (matchv ::M/objects [val#]
+                         [~label]
+                         ~inner)))
+              ;; `(bind ~computation
+              ;;        (fn [~label] ~inner))
               ))
           return
           (reverse (partition 2 steps))))
@@ -375,12 +378,6 @@
             (fold str ""))
        "}}"))
 
-(defn if% [text-m then-m else-m]
-  (|do [? text-m]
-    (if ?
-      then-m
-      else-m)))
-
 (defn apply% [monad call-state]
   (fn [state]
     ;; (prn 'apply-m monad call-state)
@@ -726,3 +723,7 @@
     [["lux;Meta" [_ ["lux;Form" ?elems]]]]
     (str "(" (->> ?elems (|map show-ast) (|interpose " ") (fold str "")) ")")
     ))
+
+(defn ident->text [ident]
+  (|let [[?module ?name] ident]
+    (str ?module ";" ?name)))
diff --git a/src/lux/compiler/case.clj b/src/lux/compiler/case.clj
index 7fd22dc59..0a24c5953 100644
--- a/src/lux/compiler/case.clj
+++ b/src/lux/compiler/case.clj
@@ -22,7 +22,7 @@
   (defn ^:private compile-match [writer ?match $target $else]
     (prn 'compile-match (aget ?match 0) $target $else)
     (matchv ::M/objects [?match]
-      [["StoreTestAC" [?idx ?name ?value]]]
+      [["StoreTestAC" ?idx]]
       (doto writer
         (.visitVarInsn Opcodes/ASTORE ?idx)
         (.visitJumpInsn Opcodes/GOTO $target))
@@ -115,17 +115,15 @@
                        $value-else (new Label)]))))
       )))
 
-(defn ^:private separate-bodies [matches]
-  (prn 'separate-bodies (aget matches 0))
-  (matchv ::M/objects [matches]
-    [["MatchAC" ?tests]]
-    (|let [[_ mappings patterns*] (&/fold (fn [$id+mappings+=matches pattern+body]
-                                            (|let [[$id mappings =matches] $id+mappings+=matches
-                                                   [pattern body] pattern+body]
-                                              (&/T (inc $id) (&/|put $id body mappings) (&/|put $id pattern =matches))))
-                                          (&/T 0 (&/|table) (&/|table))
-                                          ?tests)]
-      (&/T mappings (&/|reverse patterns*)))))
+(defn ^:private separate-bodies [patterns]
+  ;; (prn 'separate-bodies (aget matches 0))
+  (|let [[_ mappings patterns*] (&/fold (fn [$id+mappings+=matches pattern+body]
+                                          (|let [[$id mappings =matches] $id+mappings+=matches
+                                                 [pattern body] pattern+body]
+                                            (&/T (inc $id) (&/|put $id body mappings) (&/|put $id pattern =matches))))
+                                        (&/T 0 (&/|table) (&/|table))
+                                        patterns)]
+    (&/T mappings (&/|reverse patterns*))))
 
 (let [ex-class (&host/->class "java.lang.IllegalStateException")]
   (defn ^:private compile-pattern-matching [writer compile mappings patterns $end]
diff --git a/src/lux/compiler/lux.clj b/src/lux/compiler/lux.clj
index a12c30531..2417a0459 100644
--- a/src/lux/compiler/lux.clj
+++ b/src/lux/compiler/lux.clj
@@ -146,12 +146,12 @@
                             (doto (.visitEnd))))]
          ;; :let [_ (prn 'compile-def/pre-body)]
          _ (&/with-writer (.visitMethod =class Opcodes/ACC_PUBLIC "<clinit>" "()V" nil nil)
-             (|do [*writer* &/get-writer
-                    :let [_ (.visitCode *writer*)]
+             (|do [**writer** &/get-writer
+                    :let [_ (.visitCode **writer**)]
                     ;; :let [_ (prn 'compile-def/pre-body2)]
                     _ (compile ?body)
                     ;; :let [_ (prn 'compile-def/post-body2)]
-                    :let [_ (doto *writer*
+                    :let [_ (doto **writer**
                               (.visitFieldInsn Opcodes/PUTSTATIC current-class "_datum" datum-sig)
                               (.visitInsn Opcodes/RETURN)
                               (.visitMaxs 0 0)
diff --git a/src/lux/type.clj b/src/lux/type.clj
index 4eeea30aa..b17079bcc 100644
--- a/src/lux/type.clj
+++ b/src/lux/type.clj
@@ -84,16 +84,17 @@
       (fail* (str "[Type Error] Unknown type-var: " id)))))
 
 ;; [Exports]
-(def create-var
+;; Type vars
+(def ^:private create-var
   (fn [state]
     (let [id (->> state (&/get$ "lux;types") (&/get$ "lux;counter"))]
       (return* (&/update$ "lux;types" #(->> %
                                             (&/update$ "lux;counter" inc)
                                             (&/update$ "lux;mappings" (fn [ms] (&/|put id (&/V "lux;None" nil) ms))))
                           state)
-               (&/V "lux;VarT" id)))))
+               id))))
 
-(defn delete-var [id]
+(defn ^:private delete-var [id]
   (fn [state]
     (prn 'delete-var id)
     (if-let [tvar (->> state (&/get$ "lux;types") (&/get$ "lux;mappings") (&/|get id))]
@@ -103,69 +104,73 @@
                nil)
       (fail* (str "[Type Error] Unknown type-var: " id)))))
 
-(defn var-id [type]
-  (matchv ::M/objects [type]
-    [["lux;VarT" ?id]]
-    (return ?id)
-    
-    [_]
-    (fail (str "[Type Error] Not type-var: " (show-type type)))))
-
-(defn clean [?tid type]
+(defn with-var [k]
+  (|do [id create-var
+        output (k (&/V "lux;VarT" id))
+        _ (delete-var id)]
+    (return output)))
+
+(defn with-vars [amount k]
+  (|do [=vars (&/map% (constantly create-var) (&/|range amount))
+        output (k (&/|map #(&/V "lux;VarT" %) =vars))
+        _ (&/map% delete-var (&/|reverse =vars))]
+    (return output)))
+
+(defn ^:private clean* [?tid type]
   (matchv ::M/objects [type]
     [["lux;VarT" ?id]]
     (if (= ?tid ?id)
       (|do [=type (deref ?id)]
-        (clean ?tid =type))
+        (clean* ?tid =type))
       (return type))
     
     [["lux;LambdaT" [?arg ?return]]]
-    (|do [=arg (clean ?tid ?arg)
-          =return (clean ?tid ?return)]
+    (|do [=arg (clean* ?tid ?arg)
+          =return (clean* ?tid ?return)]
       (return (&/V "lux;LambdaT" (&/T =arg =return))))
 
     [["lux;AppT" [?lambda ?param]]]
-    (|do [=lambda (clean ?tid ?lambda)
-          =param (clean ?tid ?param)]
+    (|do [=lambda (clean* ?tid ?lambda)
+          =param (clean* ?tid ?param)]
       (return (&/V "lux;AppT" (&/T =lambda =param))))
 
     [["lux;TupleT" ?members]]
-    (|do [=members (&/map% (partial clean ?tid) ?members)]
+    (|do [=members (&/map% (partial clean* ?tid) ?members)]
       (return (&/V "lux;TupleT" =members)))
     
     [["lux;VariantT" ?members]]
     (|do [=members (&/map% (fn [[k v]]
-                             (|do [=v (clean ?tid v)]
+                             (|do [=v (clean* ?tid v)]
                                (return (&/T k =v))))
                            ?members)]
       (return (&/V "lux;VariantT" =members)))
 
     [["lux;RecordT" ?members]]
     (|do [=members (&/map% (fn [[k v]]
-                             (|do [=v (clean ?tid v)]
+                             (|do [=v (clean* ?tid v)]
                                (return (&/T k =v))))
                            ?members)]
       (return (&/V "lux;RecordT" =members)))
 
     [["lux;AllT" [?env ?name ?arg ?body]]]
     (|do [=env (&/map% (fn [[k v]]
-                         (|do [=v (clean ?tid v)]
+                         (|do [=v (clean* ?tid v)]
                            (return (&/T k =v))))
                        ?env)
-          body* (clean ?tid ?body)]
+          body* (clean* ?tid ?body)]
       (return (&/V "lux;AllT" (&/T =env ?name ?arg body*))))
 
     [_]
     (return type)
     ))
 
-(defn with-var [k]
-  (|do [=var create-var
-        id (var-id =var)
-        type (k =var)]
-    (|do [type* (clean id type)
-          _ (delete-var id)]
-      (return type*))))
+(defn clean [tvar type]
+  (matchv ::M/objects [tvar]
+    [["lux;VarT" ?id]]
+    (clean* ?id type)
+    
+    [_]
+    (fail (str "[Type Error] Not type-var: " (show-type tvar)))))
 
 (defn show-type [type]
   ;; (prn 'show-type (aget type 0))
@@ -435,6 +440,26 @@
     [_ ["lux;AppT" [F A]]]
     (|do [actual* (apply-type F A)]
       (check* fixpoints expected actual*))
+    ;; (let [fp-pair (&/T expected actual)
+    ;;       _ (prn 'RIGHT_APP (&/|length fixpoints))
+    ;;       _ (when (> (&/|length fixpoints) 10)
+    ;;           (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))]
+    ;;   (matchv ::M/objects [(fp-get fp-pair fixpoints)]
+    ;;     [["lux;Some" ?]]
+    ;;     (if ?
+    ;;       (return (&/T fixpoints nil))
+    ;;       (fail (check-error expected actual)))
+
+    ;;     [["lux;None" _]]
+    ;;     (|do [actual* (apply-type F A)]
+    ;;       (check* (fp-put fp-pair true fixpoints) expected actual*))))
 
     [["lux;AllT" _] _]
     (with-var
@@ -470,23 +495,23 @@
     [["lux;TupleT" e!members] ["lux;TupleT" a!members]]
     (do ;; (do (prn 'e!members (&/|length e!members))
         ;;   (prn 'a!members (&/|length a!members)))
-      (if (= (&/|length e!members) (&/|length a!members))
-        (|do [fixpoints* (&/fold% (fn [fixp ea]
-                                    (|let [[e a] ea]
-                                      (do ;; (prn "lux;TupleT" 'ITER (show-type e) (show-type a))
-                                          (|do [[fixp* _] (check* fixp e a)]
-                                            (return fixp*)))))
-                                  fixpoints
-                                  (&/zip2 e!members a!members))
-              ;; :let [_ (prn "lux;TupleT" 'DONE)]
-              ]
-          (return (&/T fixpoints* nil)))
-        (do ;; (prn "lux;TupleT" (&/|length e!members) (&/|length a!members))
-            ;; (prn "lux;TupleT"
-            ;;      (&/fold str "" (&/|interpose " " (&/|map show-type e!members)))
-            ;;      (&/fold str "" (&/|interpose " " (&/|map show-type a!members))))
-            ;; (prn "lux;TupleT#fail" (fail "[Type Error] Tuples don't match in size."))
-            (fail "[Type Error] Tuples don't match in size."))))
+        (if (= (&/|length e!members) (&/|length a!members))
+          (|do [fixpoints* (&/fold% (fn [fixp ea]
+                                      (|let [[e a] ea]
+                                        (do ;; (prn "lux;TupleT" 'ITER (show-type e) (show-type a))
+                                            (|do [[fixp* _] (check* fixp e a)]
+                                              (return fixp*)))))
+                                    fixpoints
+                                    (&/zip2 e!members a!members))
+                ;; :let [_ (prn "lux;TupleT" 'DONE)]
+                ]
+            (return (&/T fixpoints* nil)))
+          (do ;; (prn "lux;TupleT" (&/|length e!members) (&/|length a!members))
+              ;; (prn "lux;TupleT"
+              ;;      (&/fold str "" (&/|interpose " " (&/|map show-type e!members)))
+              ;;      (&/fold str "" (&/|interpose " " (&/|map show-type a!members))))
+              ;; (prn "lux;TupleT#fail" (fail "[Type Error] Tuples don't match in size."))
+              (fail "[Type Error] Tuples don't match in size."))))
     
     [["lux;VariantT" e!cases] ["lux;VariantT" a!cases]]
     (if (= (&/|length e!cases) (&/|length a!cases))
@@ -519,16 +544,7 @@
       (fail "[Type Error] Records don't match in size."))
 
     [_ _]
-    (do (prn (show-type expected) (show-type actual))
-      (assert false))
-
-    ;; [["lux;BoundT" name] _]
-    ;; (do (prn "lux;BoundT" name)
-    ;;   (assert false))
-    ;; ...
-    
-    ;; [_ ["lux;BoundT" name]]
-    ;; ...
+    (fail (println-str "[Type Error] Can't type-check: " (show-type expected) (show-type actual)))
     ))
 
 (defn check [expected actual]
@@ -543,9 +559,10 @@
 
     [["lux;AllT" [local-env local-name local-arg local-def]]]
     (with-var
-      (fn [$arg]
-        (|do [func* (apply-type func $arg)]
-          (apply-lambda func* param))))
+      (fn [$var]
+        (|do [func* (apply-type func $var)
+              =return (apply-lambda func* param)]
+          (clean $var =return))))
 
     [_]
     (fail (str "[Type System] Can't apply type " (show-type func) " to type " (show-type param)))
@@ -560,3 +577,13 @@
     [_]
     (return type)
     ))
+
+(defn variant-case [case type]
+  (matchv ::M/objects [type]
+    [["lux;VariantT" ?cases]]
+    (if-let [case-type (&/|get case ?cases)]
+      (return case-type)
+      (fail (str "[Type Error] Variant lacks case: " case)))
+
+    [_]
+    (fail (str "[Type Error] Type is not a variant: " (show-type type)))))