- Type-vars can now be deleted and be scoped (through with-var).

- Fixed a few bugs with types and pattern-matching.
- Fixed a bug wherein primitive-analysis did now unify the primitive type with the exotype.
- Modified lambda-analysis so functions subject to universal quantification can manage better the universally-quantified variables.

8 files changed, 474 insertions, 332 deletions

diff --git a/src/lux.clj b/src/lux.clj
index 7bee8df16..e035e92c8 100644
--- a/src/lux.clj
+++ b/src/lux.clj
@@ -11,8 +11,12 @@
   ;; TODO: All optimizations
   ;; TODO: Anonymous classes
   ;; TODO: 
-  
+
   ;; Finish total-locals
+
+  ;; TODO: Change &type/check to it returns a tuple with the new expected & actual types
+  ;; TODO: Stop passing-along the exo-types and instead pass-along endo-types where possible
+  ;; TODO: Optimize analyser to avoid redundant checks when dealing with type-checking (making sure check* is being handed a type)
   
   (time (&compiler/compile-all (&/|list "lux")))
   (System/gc)
diff --git a/src/lux/analyser.clj b/src/lux/analyser.clj
index 39eaf9e16..14d5599e4 100644
--- a/src/lux/analyser.clj
+++ b/src/lux/analyser.clj
@@ -38,19 +38,24 @@
   (matchv ::M/objects [token]
     ;; Standard special forms
     [["lux;Meta" [meta ["lux;Bool" ?value]]]]
-    (return (&/|list (&/V "Expression" (&/T (&/V "bool" ?value) &type/Bool))))
+    (|do [_ (&type/check exo-type &type/Bool)]
+      (return (&/|list (&/V "Expression" (&/T (&/V "bool" ?value) exo-type)))))
 
     [["lux;Meta" [meta ["lux;Int" ?value]]]]
-    (return (&/|list (&/V "Expression" (&/T (&/V "int" ?value)  &type/Int))))
+    (|do [_ (&type/check exo-type &type/Int)]
+      (return (&/|list (&/V "Expression" (&/T (&/V "int" ?value) exo-type)))))
 
     [["lux;Meta" [meta ["lux;Real" ?value]]]]
-    (return (&/|list (&/V "Expression" (&/T (&/V "real" ?value) &type/Real))))
+    (|do [_ (&type/check exo-type &type/Real)]
+      (return (&/|list (&/V "Expression" (&/T (&/V "real" ?value) exo-type)))))
 
     [["lux;Meta" [meta ["lux;Char" ?value]]]]
-    (return (&/|list (&/V "Expression" (&/T (&/V "char" ?value) &type/Char))))
+    (|do [_ (&type/check exo-type &type/Char)]
+      (return (&/|list (&/V "Expression" (&/T (&/V "char" ?value) exo-type)))))
 
     [["lux;Meta" [meta ["lux;Text" ?value]]]]
-    (return (&/|list (&/V "Expression" (&/T (&/V "text" ?value) &type/Text))))
+    (|do [_ (&type/check exo-type &type/Text)]
+      (return (&/|list (&/V "Expression" (&/T (&/V "text" ?value) exo-type)))))
 
     [["lux;Meta" [meta ["lux;Tuple" ?elems]]]]
     (&&lux/analyse-tuple analyse exo-type ?elems)
diff --git a/src/lux/analyser/base.clj b/src/lux/analyser/base.clj
index 0d2d8304a..35c12c3e0 100644
--- a/src/lux/analyser/base.clj
+++ b/src/lux/analyser/base.clj
@@ -37,9 +37,21 @@
           (fail "[Analyser Error] Can't expand to other than 2 elements.")))))
 
 (defn with-var [k]
-  (|do [=var &type/fresh-var
+  (|do [=var &type/create-var
         =ret (k =var)]
     (matchv ::M/objects [=ret]
       [["Expression" [?expr ?type]]]
-      (|do [=type (&type/clean =var ?type)]
-        (return (&/V "Expression" (&/T ?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)))
diff --git a/src/lux/analyser/case.clj b/src/lux/analyser/case.clj
index 6b2fe7a03..74d5ea5a3 100644
--- a/src/lux/analyser/case.clj
+++ b/src/lux/analyser/case.clj
@@ -8,93 +8,116 @@
                           [env :as &env])))
 
 ;; [Utils]
+(defn ^:private resolve-type [type]
+  (matchv ::M/objects [type]
+    [["lux;VarT" ?idx]]
+    (|do [type* (&type/deref ?idx)]
+      (resolve-type type*))
+
+    [_]
+    (&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]
-  (prn 'analyse-pattern/pattern (aget pattern 0) (aget pattern 1) (alength (aget pattern 1)))
+  ;; (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% (fn [_] &type/fresh-var)
-                            (&/|range (&/|length ?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% (fn [_] &type/fresh-var)
-                            (&/|range (&/|length ?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))]
-          (analyse-variant analyse-pattern idx value-type (str module* ";" ?name) (&/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))]
-          (analyse-variant analyse-pattern idx value-type (str module* ";" ?name) ?value))
-        ))
+        ;; (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]
@@ -127,9 +150,9 @@
 
 (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))
+    ;; (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]
@@ -222,49 +245,41 @@
       [["MatchAC" ?tests]]
       (&/fold% merge-total (&/V "DefaultTotal" false) ?tests))))
 
-(defn ^:private resolve-type [type]
-  (matchv ::M/objects [type]
-    [["lux;VarT" ?idx]]
-    (&type/deref ?idx)
-
-    [_]
-    (return type)))
-
 (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 [value-type struct]
-    [_ ["BoolTotal" [?total _]]]
+  (matchv ::M/objects [struct]
+    [["BoolTotal" [?total _]]]
     (|do [_ (&type/check value-type &type/Bool)]
       (return ?total))
 
-    [_ ["IntTotal" [?total _]]]
+    [["IntTotal" [?total _]]]
     (|do [_ (&type/check value-type &type/Int)]
       (return ?total))
 
-    [_ ["RealTotal" [?total _]]]
+    [["RealTotal" [?total _]]]
     (|do [_ (&type/check value-type &type/Real)]
       (return ?total))
 
-    [_ ["CharTotal" [?total _]]]
+    [["CharTotal" [?total _]]]
     (|do [_ (&type/check value-type &type/Char)]
       (return ?total))
 
-    [_ ["TextTotal" [?total _]]]
+    [["TextTotal" [?total _]]]
     (|do [_ (&type/check value-type &type/Text)]
       (return ?total))
 
-    [_ ["TupleTotal" [?total ?structs]]]
-    (|do [elems-vars (&/map% (constantly &type/fresh-var) (&/|range (&/|length ?structs)))
+    [["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 [[struct tvar] sv]
-                             (check-totality tvar struct)))
+                           (|let [[sub-struct tvar] sv]
+                             (check-totality tvar sub-struct)))
                          (&/zip2 ?structs elems-vars))]
       (return (or ?total
                   (every? true? totals))))
 
-    [_ ["RecordTotal" [?total ?structs]]]
-    (|do [elems-vars (&/map% (constantly &type/fresh-var) (&/|range (&/|length ?structs)))
+    [["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]
@@ -278,13 +293,24 @@
       (return (or ?total
                   (every? true? totals))))
 
-    [_ ["VariantTotal" [?total ?structs]]]
+    [["VariantTotal" [?total ?structs]]]
     (&/try-all% (&/|list (|do [real-type (resolve-type value-type)
-                               :let [_ (prn 'real-type (&type/show-type real-type))]]
-                           (assert false))
+                               :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.")))
     
-    [_ ["DefaultTotal" true]]
+    [["DefaultTotal" true]]
     (return true)
     ))
 
diff --git a/src/lux/analyser/lambda.clj b/src/lux/analyser/lambda.clj
index 619c39766..ae049f50f 100644
--- a/src/lux/analyser/lambda.clj
+++ b/src/lux/analyser/lambda.clj
@@ -8,7 +8,7 @@
 ;; [Resource]
 (defn with-lambda [self self-type arg arg-type body]
   ;; (prn 'with-lambda (&/|length self) (&/|length arg))
-  (prn 'with-lambda [(aget self 0) (aget self 1)] [(aget arg 0) (aget arg 1)] (alength self) (alength arg))
+  ;; (prn 'with-lambda [(aget self 0) (aget self 1)] [(aget arg 0) (aget arg 1)] (alength self) (alength arg))
   (|let [[?module1 ?name1] self
          [?module2 ?name2] arg]
     (&/with-closure
diff --git a/src/lux/analyser/lux.clj b/src/lux/analyser/lux.clj
index a9a42ffe3..32f65320a 100644
--- a/src/lux/analyser/lux.clj
+++ b/src/lux/analyser/lux.clj
@@ -19,9 +19,9 @@
 
 ;; [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/fresh-var) ?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]
@@ -36,8 +36,8 @@
 
 (defn analyse-variant [analyse exo-type ident ?value]
   (|let [[?module ?name] ident]
-    (do (prn 'analyse-variant (str ?module ";" ?name) (&/show-ast ?value))
-      (|do [:let [_ (prn 'analyse-variant/exo-type (&type/show-type exo-type))]
+    (do ;; (prn 'analyse-variant (str ?module ";" ?name) (&/show-ast ?value))
+      (|do [;; :let [_ (prn 'analyse-variant/exo-type (&type/show-type exo-type))]
             module (if (= "" ?module)
                      &/get-module-name
                      (return ?module))
@@ -53,13 +53,15 @@
 
                         [_]
                         (&type/actual-type exo-type))
-            :let [_ (prn 'exo-type* (&type/show-type exo-type*))]]
+            ;; :let [_ (prn 'analyse-variant/exo-type* (&type/show-type exo-type*))]
+            ]
         (matchv ::M/objects [exo-type*]
           [["lux;VariantT" ?cases]]
           (if-let [vtype (&/|get ?tag ?cases)]
-            (|do [:let [_ (prn 'VARIANT_BODY ?tag (&/show-ast ?value) (&type/show-type vtype))]
+            (|do [;; :let [_ (prn 'VARIANT_BODY ?tag (&/show-ast ?value) (&type/show-type vtype))]
                   =value (&&/analyse-1 analyse vtype ?value)
-                  :let [_ (prn 'GOT_VALUE =value)]]
+                  ;; :let [_ (prn 'GOT_VALUE =value)]
+                  ]
               (return (&/|list (&/V "Expression" (&/T (&/V "variant" (&/T ?tag =value))
                                                       exo-type)))))
             (fail (str "[Analyser Error] There is no case " ?tag " for variant type " (&type/show-type exo-type*))))
@@ -178,47 +180,79 @@
         _ (&/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-type (&&/expr-type =value)
-        =match (&&case/analyse-branches analyse exo-type =value-type (&/|as-pairs ?branches))]
+        =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))
                                             exo-type))))))
 
-(defn analyse-lambda [analyse exo-type ?self ?arg ?body]
+(defn analyse-lambda* [analyse exo-type ?self ?arg ?body]
   ;; (prn 'analyse-lambda ?self ?arg ?body)
-  (|do [=lambda-type* &type/fresh-lambda
-        _ (&type/check exo-type =lambda-type*)]
-    (matchv ::M/objects [=lambda-type*]
-      [["lux;LambdaT" [=arg =return]]]
-      (|do [[=scope =captured =body] (&&lambda/with-lambda ?self =lambda-type*
-                                       ?arg =arg
-                                       (&&/analyse-1 analyse =return ?body))
-            =lambda-type** (&type/clean =return =lambda-type*)
-            =lambda-type (matchv ::M/objects [=arg]
-                           [["lux;VarT" ?id]]
-                           (&/try-all% (&/|list (|do [bound (&type/deref ?id)]
-                                                  (&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)))))))
+  (|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*)))))))
+
+                                      [_]
+                                      (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)))
 
-                           [_]
-                           (fail ""))]
-        (return (&/|list (&/V "Expression" (&/T (&/V "lambda" (&/T =scope =captured =body)) =lambda-type))))))))
+(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))]
+    (return (&/|list output))))
 
 (defn analyse-def [analyse exo-type ?name ?value]
-  (prn 'analyse-def ?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)]
     (if ?
       (fail (str "[Analyser Error] Can't redefine " ?name))
-      (|do [=value (&/with-scope ?name
+      (|do [:let [_ (prn 'analyse-def/_0)]
+            =value (&/with-scope ?name
                      (&&/with-var
                        #(&&/analyse-1 analyse % ?value)))
+            :let [_ (prn 'analyse-def/_1)]
             =value-type (&&/expr-type =value)
-            :let [_ (prn 'analyse-def ?name (&type/show-type =value-type))]
-            _ (&&def/define module-name ?name =value-type)]
+            :let [_ (prn 'analyse-def/_2)]
+            ;; :let [_ (prn 'analyse-def/TYPE ?name (&type/show-type =value-type))]
+            _ (&&def/define module-name ?name =value-type)
+            :let [_ (prn 'analyse-def/_3)]]
         (return (&/|list (&/V "Statement" (&/V "def" (&/T ?name =value)))))))))
 
 (defn analyse-declare-macro [exo-type ident]
@@ -241,12 +275,12 @@
         ==type (eval! =type)
         _ (&type/check exo-type ==type)
         :let [_ (println "analyse-check#4" (&type/show-type ==type))]
-        =value (&&/analyse-1 analyse exo-type ?value)
+        =value (&&/analyse-1 analyse ==type ?value)
         :let [_ (println "analyse-check#5")]]
     (matchv ::M/objects [=value]
       [["Expression" [?expr ?expr-type]]]
       (|do [:let [_ (println "analyse-check#6" (&type/show-type ?expr-type))]
-            _ (&type/check ==type ?expr-type)
+            ;; _ (&type/check ==type ?expr-type)
             :let [_ (println "analyse-check#7")]]
         (return (&/|list (&/V "Expression" (&/T ?expr ==type))))))))
 
diff --git a/src/lux/base.clj b/src/lux/base.clj
index 91519eb0c..f9d3c9c23 100644
--- a/src/lux/base.clj
+++ b/src/lux/base.clj
@@ -87,6 +87,16 @@
       (V "lux;Cons" (T (T slot value) table*))
       (V "lux;Cons" (T (T k v) (|put slot value table*))))))
 
+(defn |remove [slot table]
+  (matchv ::M/objects [table]
+    [["lux;Nil" _]]
+    table
+    
+    [["lux;Cons" [[k v] table*]]]
+    (if (= k slot)
+      table*
+      (V "lux;Cons" (T (T k v) (|remove slot table*))))))
+
 (defn |merge [table1 table2]
   ;; (prn '|merge (aget table1 0) (aget table2 0))
   (matchv ::M/objects [table2]
@@ -125,7 +135,7 @@
 ;; [Resources/Monads]
 (defn fail [message]
   (fn [_]
-    (prn 'FAIL message)
+    ;; (prn 'FAIL message)
     (V "lux;Left" message)))
 
 (defn return [value]
diff --git a/src/lux/type.clj b/src/lux/type.clj
index 0cd839cf2..4eeea30aa 100644
--- a/src/lux/type.clj
+++ b/src/lux/type.clj
@@ -7,6 +7,42 @@
 (declare show-type)
 
 ;; [Util]
+(def Any (&/V "lux;AnyT" nil))
+(def Nothing (&/V "lux;NothingT" nil))
+(def Bool (&/V "lux;DataT" "java.lang.Boolean"))
+(def Int (&/V "lux;DataT" "java.lang.Long"))
+(def Real (&/V "lux;DataT" "java.lang.Double"))
+(def Char (&/V "lux;DataT" "java.lang.Character"))
+(def Text (&/V "lux;DataT" "java.lang.String"))
+(def Unit (&/V "lux;TupleT" (&/|list)))
+
+(def List
+  (&/V "lux;AllT" (&/T (&/|table) "List" "a"
+                       (&/V "lux;VariantT" (&/|list (&/T "lux;Nil" (&/V "lux;TupleT" (&/|list)))
+                                                    (&/T "lux;Cons" (&/V "lux;TupleT" (&/|list (&/V "lux;BoundT" "a")
+                                                                                               (&/V "lux;AppT" (&/T (&/V "lux;BoundT" "List")
+                                                                                                                    (&/V "lux;BoundT" "a")))))))))))
+
+(def Type
+  (let [Type (&/V "lux;AppT" (&/T (&/V "lux;BoundT" "Type") (&/V "lux;BoundT" "_")))
+        TypeEnv (&/V "lux;AppT" (&/T List (&/V "lux;TupleT" (&/|list Text Type))))
+        Unit (&/V "lux;TupleT" (&/|list))
+        TypePair (&/V "lux;TupleT" (&/|list Type Type))]
+    (&/V "lux;AppT" (&/T (&/V "lux;AllT" (&/T (&/|list) "Type" "_"
+                                              (&/V "lux;VariantT" (&/|list (&/T "lux;AnyT" Unit)
+                                                                           (&/T "lux;NothingT" Unit)
+                                                                           (&/T "lux;DataT" Text)
+                                                                           (&/T "lux;TupleT" (&/V "lux;AppT" (&/T List Type)))
+                                                                           (&/T "lux;VariantT" TypeEnv)
+                                                                           (&/T "lux;RecordT" TypeEnv)
+                                                                           (&/T "lux;LambdaT" TypePair)
+                                                                           (&/T "lux;BoundT" Text)
+                                                                           (&/T "lux;VarT" Int)
+                                                                           (&/T "lux;AllT" (&/V "lux;TupleT" (&/|list TypeEnv Text Text Type)))
+                                                                           (&/T "lux;AppT" TypePair)
+                                                                           ))))
+                         (&/V "lux;NothingT" nil)))))
+
 (defn bound? [id]
   (fn [state]
     (if-let [type* (->> state (&/get$ "lux;types") (&/get$ "lux;mappings") (&/|get id))]
@@ -16,21 +52,21 @@
         
         [["lux;None" _]]
         (return* state false))
-      (fail* (str "Unknown type-var: " id)))))
+      (fail* (str "[Type Error] Unknown type-var: " id)))))
 
 (defn deref [id]
   (fn [state]
     (let [mappings (->> state (&/get$ "lux;types") (&/get$ "lux;mappings"))]
       (do (prn 'deref/mappings (&/->seq (&/|keys mappings)))
         (if-let [type* (->> mappings (&/|get id))]
-          (do (prn 'deref/type* (aget type* 0))
+          (do ;; (prn 'deref/type* (aget type* 0))
             (matchv ::M/objects [type*]
               [["lux;Some" type]]
               (return* state type)
               
               [["lux;None" _]]
-              (fail* (str "Unbound type-var: " id))))
-          (fail* (str "Unknown type-var: " id)))))))
+              (fail* (str "[Type Error] Unbound type-var: " id))))
+          (fail* (str "[Type Error] Unknown type-var: " id)))))))
 
 (defn set-var [id type]
   (fn [state]
@@ -38,17 +74,17 @@
       (do ;; (prn 'set-var (aget tvar 0))
           (matchv ::M/objects [tvar]
             [["lux;Some" bound]]
-            (fail* (str "Can't rebind type var: " id " | Current type: " (show-type bound)))
+            (fail* (str "[Type Error] Can't rebind type var: " id " | Current type: " (show-type bound)))
             
             [["lux;None" _]]
             (return* (&/update$ "lux;types" (fn [ts] (&/update$ "lux;mappings" #(&/|put id (&/V "lux;Some" type) %)
                                                                ts))
                                 state)
                      nil)))
-      (fail* (str "Unknown type-var: " id)))))
+      (fail* (str "[Type Error] Unknown type-var: " id)))))
 
 ;; [Exports]
-(def fresh-var
+(def create-var
   (fn [state]
     (let [id (->> state (&/get$ "lux;types") (&/get$ "lux;counter"))]
       (return* (&/update$ "lux;types" #(->> %
@@ -57,59 +93,79 @@
                           state)
                (&/V "lux;VarT" id)))))
 
-(def fresh-lambda
-  (|do [=arg fresh-var
-        =return fresh-var]
-    (return (&/V "lux;LambdaT" (&/T =arg =return)))))
-
-(defn clean [tvar type]
-  (matchv ::M/objects [tvar]
-    [["lux;VarT" ?tid]]
-    (matchv ::M/objects [type]
-      [["lux;VarT" ?id]]
-      (if (= ?tid ?id)
-        (|do [=type (deref ?id)]
-          (clean tvar =type))
-        (return type))
-      
-      [["lux;LambdaT" [?arg ?return]]]
-      (|do [=arg (clean tvar ?arg)
-            =return (clean tvar ?return)]
-        (return (&/V "lux;LambdaT" (&/T =arg =return))))
-
-      [["lux;AppT" [?lambda ?param]]]
-      (|do [=lambda (clean tvar ?lambda)
-            =param (clean tvar ?param)]
-        (return (&/V "lux;AppT" (&/T =lambda =param))))
-
-      [["lux;TupleT" ?members]]
-      (|do [=members (&/map% (partial clean tvar) ?members)]
-        (return (&/V "lux;TupleT" =members)))
-      
-      [["lux;VariantT" ?members]]
-      (|do [=members (&/map% (fn [[k v]]
-                               (|do [=v (clean tvar v)]
-                                 (return (&/T k =v))))
-                             ?members)]
-        (return (&/V "lux;VariantT" =members)))
-
-      [["lux;RecordT" ?members]]
-      (|do [=members (&/map% (fn [[k v]]
-                               (|do [=v (clean tvar 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 tvar v)]
-                             (return (&/T k =v))))
-                         ?env)]
-        (return (&/V "lux;AllT" (&/T =env ?name ?arg ?body))))
-
-      [_]
-      (return type)
-      )))
+(defn delete-var [id]
+  (fn [state]
+    (prn 'delete-var id)
+    (if-let [tvar (->> state (&/get$ "lux;types") (&/get$ "lux;mappings") (&/|get id))]
+      (return* (&/update$ "lux;types" (fn [ts] (&/update$ "lux;mappings" #(&/|remove id %)
+                                                         ts))
+                          state)
+               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]
+  (matchv ::M/objects [type]
+    [["lux;VarT" ?id]]
+    (if (= ?tid ?id)
+      (|do [=type (deref ?id)]
+        (clean ?tid =type))
+      (return type))
+    
+    [["lux;LambdaT" [?arg ?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)]
+      (return (&/V "lux;AppT" (&/T =lambda =param))))
+
+    [["lux;TupleT" ?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)]
+                               (return (&/T k =v))))
+                           ?members)]
+      (return (&/V "lux;VariantT" =members)))
+
+    [["lux;RecordT" ?members]]
+    (|do [=members (&/map% (fn [[k 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)]
+                           (return (&/T k =v))))
+                       ?env)
+          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 show-type [type]
   ;; (prn 'show-type (aget type 0))
@@ -167,80 +223,88 @@
     ))
 
 (defn type= [x y]
-  (matchv ::M/objects [x y]
-    [["lux;AnyT" _] ["lux;AnyT" _]]
-    true
-
-    [["lux;NothingT" _] ["lux;NothingT" _]]
-    true
-
-    [["lux;DataT" xname] ["lux;DataT" yname]]
-    (= xname yname)
-
-    [["lux;TupleT" xelems] ["lux;TupleT" yelems]]
-    (&/fold (fn [old xy] (and old (type= (aget xy 0) (aget xy 1))))
-            true
-            (&/zip2 xelems yelems))
-
-    [["lux;VariantT" xcases] ["lux;VariantT" ycases]]
-    (&/fold (fn [old cases]
-              (matchv ::M/objects [cases]
-                [[[xtag xtype] [ytag ytype]]]
-                (and (= xtag ytag)
-                     (type= xtype ytype))))
-            true (&/zip2 xcases ycases))
-    
-
-    [["lux;RecordT" xfields] ["lux;RecordT" yfields]]
-    (&/fold (fn [old cases]
-              (matchv ::M/objects [cases]
-                [[[xtag xtype] [ytag ytype]]]
-                (and (= xtag ytag)
-                     (type= xtype ytype))))
-            true (&/zip2 xfields yfields))
-
-    [["lux;LambdaT" [xinput xoutput]] ["lux;LambdaT" [yinput youtput]]]
-    (and (type= xinput yinput)
-         (type= xoutput youtput))
-
-    [["lux;VarT" xid] ["lux;VarT" yid]]
-    (= xid yid)
-
-    [["lux;BoundT" xname] ["lux;BoundT" yname]]
-    (= xname yname)
-
-    [["lux;AppT" [xlambda xparam]] ["lux;AppT" [ylambda yparam]]]
-    (and (type= xlambda ylambda)
-         (type= xparam yparam))
-    
-    [["lux;AllT" [xenv xname xarg xbody]] ["lux;AllT" [yenv yname yarg ybody]]]
-    (and (&/fold (fn [old cases]
-                   (matchv ::M/objects [cases]
-                     [[[xtag xtype] [ytag ytype]]]
-                     (and (= xtag ytag)
-                          (type= xtype ytype))))
-                 true (&/zip2 xenv yenv))
-         (= xname yname)
-         (= xarg yarg)
-         (type= xbody ybody))
-
-    [_ _]
-    (do ;; (prn 'type= (show-type x) (show-type y))
-        false)
-    ))
-
-(defn ^:private fp-get [k xs]
-  (matchv ::M/objects [k]
-    [[e a]]
-    (matchv ::M/objects [xs]
+  (let [output (matchv ::M/objects [x y]
+                 [["lux;AnyT" _] ["lux;AnyT" _]]
+                 true
+
+                 [["lux;NothingT" _] ["lux;NothingT" _]]
+                 true
+
+                 [["lux;DataT" xname] ["lux;DataT" yname]]
+                 (= xname yname)
+
+                 [["lux;TupleT" xelems] ["lux;TupleT" yelems]]
+                 (&/fold (fn [old xy]
+                           (|let [[x* y*] xy]
+                             (and old
+                                  (type= x* y*))))
+                         true
+                         (&/zip2 xelems yelems))
+
+                 [["lux;VariantT" xcases] ["lux;VariantT" ycases]]
+                 (and (= (&/|length xcases) (&/|length ycases))
+                      (&/fold (fn [old case]
+                                (and old
+                                     (type= (&/|get case xcases) (&/|get case ycases))))
+                              true
+                              (&/|keys xcases)))
+
+                 [["lux;RecordT" xfields] ["lux;RecordT" yfields]]
+                 (and (= (&/|length xfields) (&/|length yfields))
+                      (&/fold (fn [old field]
+                                (and old
+                                     (type= (&/|get field xfields) (&/|get field yfields))))
+                              true
+                              (&/|keys xfields)))
+
+                 [["lux;LambdaT" [xinput xoutput]] ["lux;LambdaT" [yinput youtput]]]
+                 (and (type= xinput yinput)
+                      (type= xoutput youtput))
+
+                 [["lux;VarT" xid] ["lux;VarT" yid]]
+                 (= xid yid)
+
+                 [["lux;BoundT" xname] ["lux;BoundT" yname]]
+                 (= xname yname)
+
+                 [["lux;AppT" [xlambda xparam]] ["lux;AppT" [ylambda yparam]]]
+                 (and (type= xlambda ylambda)
+                      (type= xparam yparam))
+                 
+                 [["lux;AllT" [xenv xname xarg xbody]] ["lux;AllT" [yenv yname yarg ybody]]]
+                 (do ;; (prn 'TESTING_ALLT
+                     ;;      'NAME [xname yname] (= xname yname)
+                     ;;      'ARG (= xarg yarg)
+                     ;;      'LENGTH [(&/|length xenv) (&/|length yenv)] (= (&/|length xenv) (&/|length yenv)))
+                   (and (= xname yname)
+                        (= xarg yarg)
+                        (type= xbody ybody)
+                        ;; (= (&/|length xenv) (&/|length yenv))
+                        ;; (&/fold (fn [old bname]
+                        ;;           (and old
+                        ;;                (type= (&/|get bname xenv) (&/|get bname yenv))))
+                        ;;         true
+                        ;;         (&/|keys xenv))
+                        ))
+
+                 [_ _]
+                 (do (prn 'type= (show-type x) (show-type y))
+                   false)
+                 )]
+    ;; (prn 'type= output (show-type x) (show-type y))
+    output))
+
+(defn ^:private fp-get [k fixpoints]
+  (|let [[e a] k]
+    (matchv ::M/objects [fixpoints]
       [["lux;Nil" _]]
       (&/V "lux;None" nil)
 
-      [["lux;Cons" [[[e* a*] v*] xs*]]]
+      [["lux;Cons" [[[e* a*] v*] fixpoints*]]]
       (if (and (type= e e*)
                (type= a a*))
         (&/V "lux;Some" v*)
-        (fp-get k xs*))
+        (fp-get k fixpoints*))
       )))
 
 (defn ^:private fp-put [k v fixpoints]
@@ -315,7 +379,7 @@
 (def init-fixpoints (&/|list))
 
 (defn ^:private check* [fixpoints expected actual]
-  (prn 'check* (aget expected 0) (aget actual 0))
+  ;; (prn 'check* (aget expected 0) (aget actual 0))
   ;; (prn 'check* (show-type expected) (show-type actual))
   (matchv ::M/objects [expected actual]
     [["lux;AnyT" _] _]
@@ -347,8 +411,17 @@
                            (check* fixpoints expected bound))))
 
     [["lux;AppT" [F A]] _]
-    (|do [expected* (apply-type F A)
-          :let [fp-pair (&/T expected actual)]]
+    (let [fp-pair (&/T expected actual)
+          _ (prn 'LEFT_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 ?
@@ -356,21 +429,34 @@
           (fail (check-error expected actual)))
 
         [["lux;None" _]]
-        (check* (fp-put fp-pair true fixpoints) expected* actual)))
+        (|do [expected* (apply-type F A)]
+          (check* (fp-put fp-pair true fixpoints) expected* actual))))
 
     [_ ["lux;AppT" [F A]]]
     (|do [actual* (apply-type F A)]
       (check* fixpoints expected actual*))
 
     [["lux;AllT" _] _]
-    (|do [$var fresh-var
-          expected* (apply-type expected $var)]
-      (check* fixpoints expected* actual))
+    (with-var
+      (fn [$arg]
+        (|do [expected* (apply-type expected $arg)]
+          (check* fixpoints expected* actual))))
 
     [_ ["lux;AllT" _]]
-    (|do [$var fresh-var
-          actual* (apply-type actual $var)]
-      (check* fixpoints expected actual*))
+    (with-var
+      (fn [$arg]
+        (|do [actual* (apply-type actual $arg)]
+          (check* fixpoints expected actual*))))
+
+    ;; [["lux;AllT" _] _]
+    ;; (|do [$arg create-var
+    ;;       expected* (apply-type expected $arg)]
+    ;;   (check* fixpoints expected* actual))
+
+    ;; [_ ["lux;AllT" _]]
+    ;; (|do [$arg create-var
+    ;;       actual* (apply-type actual $arg)]
+    ;;   (check* fixpoints expected actual*))
 
     [["lux;DataT" e!name] ["lux;DataT" a!name]]
     (if (= e!name a!name)
@@ -382,8 +468,8 @@
       (check* fixpoints* eO aO))
 
     [["lux;TupleT" e!members] ["lux;TupleT" a!members]]
-    (do (do (prn 'e!members (&/|length e!members))
-          (prn 'a!members (&/|length 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]
@@ -405,7 +491,7 @@
     [["lux;VariantT" e!cases] ["lux;VariantT" a!cases]]
     (if (= (&/|length e!cases) (&/|length a!cases))
       (|do [fixpoints* (&/fold% (fn [fixp slot]
-                                  (prn "lux;VariantT" slot)
+                                  (prn 'VARIANT_CASE slot)
                                   (if-let [e!type (&/|get slot e!cases)]
                                     (if-let [a!type (&/|get slot a!cases)]
                                       (|do [[fixp* _] (check* fixp e!type a!type)]
@@ -420,7 +506,7 @@
     [["lux;RecordT" e!fields] ["lux;RecordT" a!fields]]
     (if (= (&/|length e!fields) (&/|length a!fields))
       (|do [fixpoints* (&/fold% (fn [fixp slot]
-                                  (prn "lux;RecordT" slot)
+                                  (prn 'RECORD_FIELD slot)
                                   (if-let [e!type (&/|get slot e!fields)]
                                     (if-let [a!type (&/|get slot a!fields)]
                                       (|do [[fixp* _] (check* fixp e!type a!type)]
@@ -456,9 +542,10 @@
       (return output))
 
     [["lux;AllT" [local-env local-name local-arg local-def]]]
-    (|do [$var fresh-var
-          func* (apply-type func $var)]
-      (apply-lambda func* param))
+    (with-var
+      (fn [$arg]
+        (|do [func* (apply-type func $arg)]
+          (apply-lambda func* param))))
 
     [_]
     (fail (str "[Type System] Can't apply type " (show-type func) " to type " (show-type param)))
@@ -473,39 +560,3 @@
     [_]
     (return type)
     ))
-
-(def Any (&/V "lux;AnyT" nil))
-(def Nothing (&/V "lux;NothingT" nil))
-(def Bool (&/V "lux;DataT" "java.lang.Boolean"))
-(def Int (&/V "lux;DataT" "java.lang.Long"))
-(def Real (&/V "lux;DataT" "java.lang.Double"))
-(def Char (&/V "lux;DataT" "java.lang.Character"))
-(def Text (&/V "lux;DataT" "java.lang.String"))
-(def Unit (&/V "lux;TupleT" (&/|list)))
-
-(def List
-  (&/V "lux;AllT" (&/T (&/|table) "List" "a"
-                       (&/V "lux;VariantT" (&/|list (&/T "lux;Nil" (&/V "lux;TupleT" (&/|list)))
-                                                    (&/T "lux;Cons" (&/V "lux;TupleT" (&/|list (&/V "lux;BoundT" "a")
-                                                                                               (&/V "lux;AppT" (&/T (&/V "lux;BoundT" "List")
-                                                                                                                    (&/V "lux;BoundT" "a")))))))))))
-
-(def Type
-  (let [Type (&/V "lux;AppT" (&/T (&/V "lux;BoundT" "Type") (&/V "lux;BoundT" "_")))
-        TypeEnv (&/V "lux;AppT" (&/T List (&/V "lux;TupleT" (&/|list Text Type))))
-        Unit (&/V "lux;TupleT" (&/|list))
-        TypePair (&/V "lux;TupleT" (&/|list Type Type))]
-    (&/V "lux;AppT" (&/T (&/V "lux;AllT" (&/T (&/|list) "Type" "_"
-                                              (&/V "lux;VariantT" (&/|list (&/T "lux;AnyT" Unit)
-                                                                           (&/T "lux;NothingT" Unit)
-                                                                           (&/T "lux;DataT" Text)
-                                                                           (&/T "lux;TupleT" (&/V "lux;AppT" (&/T List Type)))
-                                                                           (&/T "lux;VariantT" TypeEnv)
-                                                                           (&/T "lux;RecordT" TypeEnv)
-                                                                           (&/T "lux;LambdaT" TypePair)
-                                                                           (&/T "lux;BoundT" Text)
-                                                                           (&/T "lux;VarT" Int)
-                                                                           (&/T "lux;AllT" (&/V "lux;TupleT" (&/|list TypeEnv Text Text Type)))
-                                                                           (&/T "lux;AppT" TypePair)
-                                                                           ))))
-                         (&/V "lux;NothingT" nil)))))