- Beginning to add type-system + type-inferencer.

- Removed exec, get@' & set@' special forms, as they are not primitive enough as to be part of the language.

11 files changed, 482 insertions, 400 deletions

diff --git a/src/lux.clj b/src/lux.clj
index 6d79b52bf..7bee8df16 100644
--- a/src/lux.clj
+++ b/src/lux.clj
@@ -15,6 +15,7 @@
   ;; Finish total-locals
   
   (time (&compiler/compile-all (&/|list "lux")))
+  (System/gc)
   (time (&compiler/compile-all (&/|list "lux" "test2")))
 
   ;; jar cvf test2.jar *.class test2 && java -cp "test2.jar" test2
diff --git a/src/lux/analyser.clj b/src/lux/analyser.clj
index e73423ffc..9ed75b83d 100644
--- a/src/lux/analyser.clj
+++ b/src/lux/analyser.clj
@@ -35,19 +35,19 @@
   (matchv ::M/objects [token]
     ;; Standard special forms
     [["lux;Meta" [meta ["lux;Bool" ?value]]]]
-    (return (&/|list (&/V "Expression" (&/T (&/V "bool" ?value) (&/V "lux;TData" (&/T "java.lang.Boolean" (&/V "lux;Nil" nil)))))))
+    (return (&/|list (&/V "Expression" (&/T (&/V "bool" ?value) (&/V "lux;DataT" (&/T "java.lang.Boolean" (&/V "lux;Nil" nil)))))))
 
     [["lux;Meta" [meta ["lux;Int" ?value]]]]
-    (return (&/|list (&/V "Expression" (&/T (&/V "int" ?value)  (&/V "lux;TData" (&/T "java.lang.Long" (&/V "lux;Nil" nil)))))))
+    (return (&/|list (&/V "Expression" (&/T (&/V "int" ?value)  (&/V "lux;DataT" (&/T "java.lang.Long" (&/V "lux;Nil" nil)))))))
 
     [["lux;Meta" [meta ["lux;Real" ?value]]]]
-    (return (&/|list (&/V "Expression" (&/T (&/V "real" ?value) (&/V "lux;TData" (&/T "java.lang.Double" (&/V "lux;Nil" nil)))))))
+    (return (&/|list (&/V "Expression" (&/T (&/V "real" ?value) (&/V "lux;DataT" (&/T "java.lang.Double" (&/V "lux;Nil" nil)))))))
 
     [["lux;Meta" [meta ["lux;Char" ?value]]]]
-    (return (&/|list (&/V "Expression" (&/T (&/V "char" ?value) (&/V "lux;TData" (&/T "java.lang.Character" (&/V "lux;Nil" nil)))))))
+    (return (&/|list (&/V "Expression" (&/T (&/V "char" ?value) (&/V "lux;DataT" (&/T "java.lang.Character" (&/V "lux;Nil" nil)))))))
 
     [["lux;Meta" [meta ["lux;Text" ?value]]]]
-    (return (&/|list (&/V "Expression" (&/T (&/V "text" ?value) (&/V "lux;TData" (&/T "java.lang.String" (&/V "lux;Nil" nil)))))))
+    (return (&/|list (&/V "Expression" (&/T (&/V "text" ?value) (&/V "lux;DataT" (&/T "java.lang.String" (&/V "lux;Nil" nil)))))))
 
     [["lux;Meta" [meta ["lux;Tuple" ?elems]]]]
     (&&lux/analyse-tuple analyse ?elems)
@@ -56,13 +56,13 @@
     (&&lux/analyse-record analyse ?elems)
 
     [["lux;Meta" [meta ["lux;Tag" [?module ?name]]]]]
-    (let [tuple-type (&/V "lux;Tuple" (&/V "lux;Nil" nil))
+    (let [tuple-type (&/V "lux;TupleT" (&/V "lux;Nil" nil))
           ?tag (str ?module ";" ?name)]
       (return (&/|list (&/V "Expression" (&/T (&/V "variant" (&/T ?tag (&/V "Expression" (&/T (&/V "tuple" (&/|list)) tuple-type))))
-                                              (&/V "lux;TVariant" (&/V "lux;Cons" (&/T (&/T ?tag tuple-type) (&/V "lux;Nil" nil)))))))))
+                                              (&/V "lux;VariantT" (&/V "lux;Cons" (&/T (&/T ?tag tuple-type) (&/V "lux;Nil" nil)))))))))
 
     [["lux;Meta" [meta ["lux;Symbol" [_ "jvm-null"]]]]]
-    (return (&/|list (&/V "Expression" (&/T (&/V "jvm-null" nil) (&/V "lux;TData" (&/T "null" (&/V "lux;Nil" nil)))))))
+    (return (&/|list (&/V "Expression" (&/T (&/V "jvm-null" nil) (&/V "lux;DataT" (&/T "null" (&/V "lux;Nil" nil)))))))
     
     [["lux;Meta" [meta ["lux;Symbol" ?ident]]]]
     (&&lux/analyse-ident analyse ?ident)
@@ -78,18 +78,6 @@
                                                                                        ["lux;Nil" _]]]]]]]]]]]]]
     (&&lux/analyse-lambda analyse ?self ?arg ?body)
 
-    [["lux;Meta" [meta ["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Symbol" [_ "get@'"]]]]
-                                                ["lux;Cons" [["lux;Meta" [_ ["lux;Tag" ?slot]]]
-                                                             ["lux;Cons" [?record ["lux;Nil" _]]]]]]]]]]]
-    (&&lux/analyse-get analyse ?slot ?record)
-
-    [["lux;Meta" [meta ["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Symbol" [_ "set@'"]]]]
-                                                ["lux;Cons" [["lux;Meta" [_ ["lux;Tag" ?slot]]]
-                                                             ["lux;Cons" [?value
-                                                                          ["lux;Cons" [?record
-                                                                                       ["lux;Nil" _]]]]]]]]]]]]]
-    (&&lux/analyse-set analyse ?slot ?value ?record)
-
     [["lux;Meta" [meta ["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Symbol" [_ "def'"]]]]
                                                 ["lux;Cons" [["lux;Meta" [_ ["lux;Symbol" [_ ?name]]]]
                                                              ["lux;Cons" [?value
@@ -98,7 +86,7 @@
         ;;   (prn "if" (&/show-ast ?value)))
         (&&lux/analyse-def analyse ?name ?value))
 
-    [["lux;Meta" [meta ["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Symbol" [_ "declare-macro"]]]]
+    [["lux;Meta" [meta ["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Symbol" [_ "declare-macro'"]]]]
                                                 ["lux;Cons" [["lux;Meta" [_ ["lux;Symbol" ?ident]]]
                                                              ["lux;Nil" _]]]]]]]]]
     (&&lux/analyse-declare-macro ?ident)
@@ -108,23 +96,19 @@
                                                              ["lux;Nil" _]]]]]]]]]
     (&&lux/analyse-import analyse ?path)
 
-    [["lux;Meta" [meta ["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Symbol" [_ ":"]]]]
-                                                ["lux;Cons" [?value
-                                                             ["lux;Cons" [?type
+    [["lux;Meta" [meta ["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Symbol" [_ "check'"]]]]
+                                                ["lux;Cons" [?type
+                                                             ["lux;Cons" [?value
                                                                           ["lux;Nil" _]]]]]]]]]]]
     (&&lux/analyse-check analyse eval! ?type ?value)
 
-    [["lux;Meta" [meta ["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Symbol" [_ "coerce"]]]]
+    [["lux;Meta" [meta ["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Symbol" [_ "coerce'"]]]]
                                                 ["lux;Cons" [?type
                                                              ["lux;Cons" [?value
                                                                           ["lux;Nil" _]]]]]]]]]]]
     (&&lux/analyse-coerce analyse eval! ?type ?value)
 
     ;; Host special forms
-    [["lux;Meta" [meta ["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Symbol" [_ "exec"]]]]
-                                                ?exprs]]]]]]
-    (&&host/analyse-exec analyse ?exprs)
-
     ;; Integer arithmetic
     [["lux;Meta" [meta ["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Symbol" [_ "jvm-iadd"]]]] ["lux;Cons" [?y ["lux;Cons" [?x ["lux;Nil" _]]]]]]]]]]]
     (&&host/analyse-jvm-iadd analyse ?x ?y)
@@ -448,7 +432,7 @@
              ;; :let [_ (prn 'POST-ASSERT)]
              =value (&&/analyse-1 (analyse-ast eval!) (&/|head ?values))
              =value-type (&&/expr-type =value)]
-        (return (&/|list (&/V "Expression" (&/T (&/V "variant" (&/T ?tag =value)) (&/V "lux;TVariant" (&/V "lux;Cons" (&/T (&/T ?tag =value-type) (&/V "lux;Nil" nil)))))))))
+        (return (&/|list (&/V "Expression" (&/T (&/V "variant" (&/T ?tag =value)) (&/V "lux;VariantT" (&/V "lux;Cons" (&/T (&/T ?tag =value-type) (&/V "lux;Nil" nil)))))))))
       
       [["lux;Meta" [meta ["lux;Form" ["lux;Cons" [?fn ?args]]]]]]
       (fn [state]
diff --git a/src/lux/analyser/host.clj b/src/lux/analyser/host.clj
index b8963f73f..cfc79c0b3 100644
--- a/src/lux/analyser/host.clj
+++ b/src/lux/analyser/host.clj
@@ -20,8 +20,8 @@
 
 ;; [Resources]
 (do-template [<name> <output-tag> <input-class> <output-class>]
-  (let [input-type (&/V "lux;TData" (to-array [<input-class> (&/V "lux;Nil" nil)]))
-        output-type (&/V "lux;TData" (to-array [<output-class> (&/V "lux;Nil" nil)]))]
+  (let [input-type (&/V "lux;DataT" (to-array [<input-class> (&/V "lux;Nil" nil)]))
+        output-type (&/V "lux;DataT" (to-array [<output-class> (&/V "lux;Nil" nil)]))]
     (defn <name> [analyse ?x ?y]
       (exec [[=x =y] (&&/analyse-2 analyse ?x ?y)
              =x-type (&&/expr-type =x)
@@ -126,17 +126,17 @@
 
 (defn analyse-jvm-null? [analyse ?object]
   (exec [=object (&&/analyse-1 analyse ?object)]
-    (return (&/|list (&/V "Expression" (&/T (&/V "jvm-null?" =object) (&/V "lux;TData" (&/T "java.lang.Boolean" (&/V "lux;Nil" nil)))))))))
+    (return (&/|list (&/V "Expression" (&/T (&/V "jvm-null?" =object) (&/V "lux;DataT" (&/T "java.lang.Boolean" (&/V "lux;Nil" nil)))))))))
 
 (defn analyse-jvm-new [analyse ?class ?classes ?args]
   (exec [=class (&host/full-class-name ?class)
          =classes (&/map% &host/extract-jvm-param ?classes)
          =args (&/flat-map% analyse ?args)]
-    (return (&/|list (&/V "Expression" (&/T (&/V "jvm-new" (&/T =class =classes =args)) (&/V "lux;TData" (&/T =class (&/V "lux;Nil" nil)))))))))
+    (return (&/|list (&/V "Expression" (&/T (&/V "jvm-new" (&/T =class =classes =args)) (&/V "lux;DataT" (&/T =class (&/V "lux;Nil" nil)))))))))
 
 (defn analyse-jvm-new-array [analyse ?class ?length]
   (exec [=class (&host/full-class-name ?class)]
-    (return (&/|list (&/V "Expression" (&/T (&/V "jvm-new-array" (&/T =class ?length)) (&/V "array" (&/T (&/V "lux;TData" (to-array [=class (&/V "lux;Nil" nil)]))
+    (return (&/|list (&/V "Expression" (&/T (&/V "jvm-new-array" (&/T =class ?length)) (&/V "array" (&/T (&/V "lux;DataT" (to-array [=class (&/V "lux;Nil" nil)]))
                                                                                                          (&/V "lux;Nil" nil)))))))))
 
 (defn analyse-jvm-aastore [analyse ?array ?idx ?elem]
@@ -195,16 +195,10 @@
          $module &/get-module-name]
     (return (&/|list (&/V "Statement" (&/V "jvm-interface" (&/T $module ?name =methods)))))))
 
-(defn analyse-exec [analyse ?exprs]
-  (exec [_ (&/assert! (count ?exprs) "\"exec\" expressions can't have empty bodies.")
-         =exprs (&/flat-map% analyse ?exprs)
-         =exprs-types (&/map% &&/expr-type =exprs)]
-    (return (&/|list (&/V "Expression" (&/T (&/V "exec" =exprs) (&/|head (&/|reverse =exprs-types))))))))
-
 (defn analyse-jvm-try [analyse ?body [?catches ?finally]]
   (exec [=body (&&/analyse-1 analyse ?body)
          =catches (&/map% (fn [[?ex-class ?ex-arg ?catch-body]]
-                            (&&env/with-local ?ex-arg (&/V "lux;TData" (&/T ?ex-class (&/V "lux;Nil" nil)))
+                            (&&env/with-local ?ex-arg (&/V "lux;DataT" (&/T ?ex-class (&/V "lux;Nil" nil)))
                               (exec [=catch-body (&&/analyse-1 analyse ?catch-body)]
                                 (return [?ex-class ?ex-arg =catch-body]))))
                           ?catches)
@@ -214,20 +208,20 @@
 
 (defn analyse-jvm-throw [analyse ?ex]
   (exec [=ex (&&/analyse-1 analyse ?ex)]
-    (return (&/|list (&/V "Expression" (&/T (&/V "jvm-throw" =ex) (&/V "lux;TNothing" nil)))))))
+    (return (&/|list (&/V "Expression" (&/T (&/V "jvm-throw" =ex) (&/V "lux;NothingT" nil)))))))
 
 (defn analyse-jvm-monitorenter [analyse ?monitor]
   (exec [=monitor (&&/analyse-1 analyse ?monitor)]
-    (return (&/|list (&/V "Expression" (&/T (&/V "jvm-monitorenter" =monitor) (&/V "lux;TTuple" (&/V "lux;Nil" nil))))))))
+    (return (&/|list (&/V "Expression" (&/T (&/V "jvm-monitorenter" =monitor) (&/V "lux;TupleT" (&/V "lux;Nil" nil))))))))
 
 (defn analyse-jvm-monitorexit [analyse ?monitor]
   (exec [=monitor (&&/analyse-1 analyse ?monitor)]
-    (return (&/|list (&/V "Expression" (&/T (&/V "jvm-monitorexit" =monitor) (&/V "lux;TTuple" (&/V "lux;Nil" nil))))))))
+    (return (&/|list (&/V "Expression" (&/T (&/V "jvm-monitorexit" =monitor) (&/V "lux;TupleT" (&/V "lux;Nil" nil))))))))
 
 (do-template [<name> <tag> <from-class> <to-class>]
   (defn <name> [analyse ?value]
     (exec [=value (&&/analyse-1 analyse ?value)]
-      (return (&/|list (&/V "Expression" (&/T (&/V <tag> =value) (&/V "lux;TData" (&/T <to-class> (&/V "lux;Nil" nil)))))))))
+      (return (&/|list (&/V "Expression" (&/T (&/V <tag> =value) (&/V "lux;DataT" (&/T <to-class> (&/V "lux;Nil" nil)))))))))
 
   analyse-jvm-d2f "jvm-d2f" "java.lang.Double"  "java.lang.Float"
   analyse-jvm-d2i "jvm-d2i" "java.lang.Double"  "java.lang.Integer"
@@ -252,7 +246,7 @@
 (do-template [<name> <tag> <from-class> <to-class>]
   (defn <name> [analyse ?value]
     (exec [=value (&&/analyse-1 analyse ?value)]
-      (return (&/|list (&/V "Expression" (&/T (&/V <tag> =value) (&/V "lux;TData" (&/T <to-class> (&/V "lux;Nil" nil)))))))))
+      (return (&/|list (&/V "Expression" (&/T (&/V <tag> =value) (&/V "lux;DataT" (&/T <to-class> (&/V "lux;Nil" nil)))))))))
 
   analyse-jvm-iand  "jvm-iand"  "java.lang.Integer" "java.lang.Integer"
   analyse-jvm-ior   "jvm-ior"   "java.lang.Integer" "java.lang.Integer"
@@ -267,6 +261,6 @@
   )
 
 (defn analyse-jvm-program [analyse ?args ?body]
-  (exec [=body (&&env/with-local ?args (&/V "lux;TAny" nil)
+  (exec [=body (&&env/with-local ?args (&/V "lux;AnyT" nil)
                  (&&/analyse-1 analyse ?body))]
     (return (&/|list (&/V "Statement" (&/V "jvm-program" =body))))))
diff --git a/src/lux/analyser/lux.clj b/src/lux/analyser/lux.clj
index e6dd0d1d0..aa205bf06 100644
--- a/src/lux/analyser/lux.clj
+++ b/src/lux/analyser/lux.clj
@@ -19,7 +19,7 @@
          =elems-types (&/map% &&/expr-type =elems)
          ;; :let [_ (prn 'analyse-tuple =elems)]
          ]
-    (return (&/|list (&/V "Expression" (&/T (&/V "tuple" =elems) (&/V "lux;TTuple" =elems-types)))))))
+    (return (&/|list (&/V "Expression" (&/T (&/V "tuple" =elems) (&/V "lux;TupleT" =elems-types)))))))
 
 (defn analyse-record [analyse ?elems]
   (exec [=elems (&/map% (fn [kv]
@@ -36,7 +36,7 @@
                               =elems)
          ;; :let [_ (prn 'analyse-tuple =elems)]
          ]
-    (return (&/|list (&/V "Expression" (&/T (&/V "lux;record" =elems) (&/V "lux;TRecord" =elems-types)))))))
+    (return (&/|list (&/V "Expression" (&/T (&/V "lux;record" =elems) (&/V "lux;RecordT" =elems-types)))))))
 
 (defn ^:private resolve-global [ident state]
   (|let [[?module ?name] ident
@@ -160,7 +160,7 @@
          ;; :let [_ (prn '=bodies =bodies)]
          ;; :let [_ (prn 'analyse-case/=bodies =bodies)]
          =body-types (&/map% &&/expr-type =bodies)
-         =case-type (&/fold% &type/merge (&/V "lux;TNothing" nil) =body-types)
+         =case-type (&/fold% &type/merge (&/V "lux;NothingT" nil) =body-types)
          :let [=branches (&/zip2 (&/|map &/|first branches) =bodies)]]
     (return (&/|list (&/V "Expression" (&/T (&/V "case" (&/T =value base-register max-locals =branches))
                                             =case-type))))))
@@ -169,39 +169,36 @@
   ;; (prn 'analyse-lambda ?self ?arg ?body)
   (exec [=lambda-type* &type/fresh-lambda]
     (matchv ::M/objects [=lambda-type*]
-      [["lux;TLambda" [=arg =return]]]
+      [["lux;LambdaT" [=arg =return]]]
       (exec [[=scope =captured =body] (&&lambda/with-lambda ?self =lambda-type*
                                         ?arg =arg
                                         (&&/analyse-1 analyse ?body))
              =body-type (&&/expr-type =body)
              ;; _ =body-type
-             =lambda-type (exec [_ (&type/solve =return =body-type)
-                                 =lambda-type** (&type/clean =return =lambda-type*)]
-                            (&type/clean =arg =lambda-type**))
+             =lambda-type (exec [_ (&type/solve &type/init-fixpoints =return =body-type)]
+                            (&type/clean =return =lambda-type*))
+             =bound-arg (&type/lookup =arg)
+             =lambda-type (matchv ::M/objects [=arg =bound-arg]
+                            [["lux;VarT" id] ["lux;Some" bound]]
+                            (&type/clean =arg =lambda-type)
+
+                            [["lux;VarT" id] ["lux;None" _]]
+                            (let [var-name (str (gensym ""))
+                                  bound (&/V "lux;BoundT" var-name)]
+                              (exec [_ (&type/reset id bound)
+                                     lambda-type (&type/clean =arg =lambda-type)]
+                                (return (&/V "lux;AllT" (&/T (&/|list) "" var-name lambda-type))))))
              ;; :let [_ (prn '=lambda-type =lambda-type)]
              ]
         (return (&/|list (&/V "Expression" (&/T (&/V "lambda" (&/T =scope =captured ?arg =body)) =lambda-type))))))))
 
-(defn analyse-get [analyse ?slot ?record]
-  (exec [=record (&&/analyse-1 analyse ?record)
-         =record-type (&&/expr-type =record)
-         =slot-type (&type/slot-type =record-type ?slot)]
-    (return (&/|list (&/V "Expression" (&/T (&/V "get" (?slot =record)) =slot-type))))))
-
-(defn analyse-set [analyse ?slot ?value ?record]
-  (exec [=value (&&/analyse-1 analyse ?value)
-         =record (&&/analyse-1 analyse ?record)
-         =record-type (&&/expr-type =record)
-         =slot-type (&type/slot-type =record-type ?slot)
-         _ (&type/solve =slot-type =value)]
-    (return (&/|list (&/V "Expression" (&/T (&/V "set" (&/T ?slot =value =record)) =slot-type))))))
-
 (defn analyse-def [analyse ?name ?value]
   ;; (prn 'analyse-def ?name ?value)
   (exec [module-name &/get-module-name]
     (&/if% (&&def/defined? module-name ?name)
            (fail (str "[Analyser Error] Can't redefine " ?name))
-           (exec [=value (&&/analyse-1 analyse ?value)
+           (exec [=value (&/with-scope ?name
+                           (&&/analyse-1 analyse ?value))
                   =value-type (&&/expr-type =value)
                   _ (&&def/define module-name ?name =value-type)]
              (return (&/|list (&/V "Statement" (&/V "def" (&/T ?name =value)))))))))
@@ -219,22 +216,32 @@
   (return (&/|list)))
 
 (defn analyse-check [analyse eval! ?type ?value]
+  (println "analyse-check#0")
   (exec [=type (&&/analyse-1 analyse ?type)
+         :let [_ (println "analyse-check#1")]
          =type-type (&&/expr-type =type)
-         _ (&type/solve &type/+type+ =type-type)
+         :let [_ (println "analyse-check#2")
+               _ (println 1 (&type/show-type &type/Type))
+               _ (println 2 (&type/show-type =type-type))]
+         _ (&type/solve &type/init-fixpoints &type/Type =type-type)
+         :let [_ (println "analyse-check#3")]
          ==type (eval! =type)
-         =value (&&/analyse-1 analyse ?value)]
+         :let [_ (println "analyse-check#4" (&type/show-type ==type))]
+         =value (&&/analyse-1 analyse ?value)
+         :let [_ (println "analyse-check#5")]]
     (matchv ::M/objects [=value]
       [["Expression" [?expr ?expr-type]]]
-      (exec [_ (&type/solve ==type ?expr-type)]
-        (return (&/V "Expression" (&/T ?expr ==type)))))))
+      (exec [:let [_ (println "analyse-check#6" (&type/show-type ?expr-type))]
+             _ (&type/solve &type/init-fixpoints ==type ?expr-type)
+             :let [_ (println "analyse-check#7")]]
+        (return (&/|list (&/V "Expression" (&/T ?expr ==type))))))))
 
 (defn analyse-coerce [analyse eval! ?type ?value]
   (exec [=type (&&/analyse-1 analyse ?type)
          =type-type (&&/expr-type =type)
-         _ (&type/solve &type/+type+ =type-type)
+         _ (&type/solve &type/init-fixpoints &type/Type =type-type)
          ==type (eval! =type)
          =value (&&/analyse-1 analyse ?value)]
     (matchv ::M/objects [=value]
       [["Expression" [?expr ?expr-type]]]
-      (return (&/V "Expression" (&/T ?expr ==type))))))
+      (return (&/|list (&/V "Expression" (&/T ?expr ==type)))))))
diff --git a/src/lux/base.clj b/src/lux/base.clj
index 089d1bf8a..29ecfd123 100644
--- a/src/lux/base.clj
+++ b/src/lux/base.clj
@@ -132,15 +132,23 @@
     (V "lux;Right" (T state value))))
 
 (defn bind [m-value step]
+  (when (not (fn? m-value))
+    (prn 'bind (aget m-value 0)))
+  (when (not (fn? step))
+    (prn 'bind (aget step 0)))
   ;; (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]]]
-        ((step ?datum) ?state)
+        (let [next-fn (step ?datum)]
+          (when (not (fn? next-fn))
+            (prn 'bind (aget next-fn 0)
+                 (aget next-fn 1)))
+          (next-fn ?state))
         
-        [_]
+        [["lux;Left" _]]
         inputs))))
 
 (defmacro exec [steps return]
@@ -598,7 +606,7 @@
   (exec [module get-current-module-env]
     (return (get$ "lux;name" module))))
 
-(defn ^:private with-scope [name body]
+(defn with-scope [name body]
   (fn [state]
     (let [output (body (update$ "lux;local-envs" #(|cons (env name) %) state))]
       (matchv ::M/objects [output]
diff --git a/src/lux/compiler.clj b/src/lux/compiler.clj
index 53787473b..bf724c768 100644
--- a/src/lux/compiler.clj
+++ b/src/lux/compiler.clj
@@ -76,12 +76,6 @@
           [["lambda" [?scope ?env ?args ?body]]]
           (&&lambda/compile-lambda compile-expression ?scope ?env ?args ?body)
 
-          [["get" [?slot ?record]]]
-          (&&lux/compile-get compile-expression ?type ?slot ?record)
-
-          [["set" [?slot ?value ?record]]]
-          (&&lux/compile-set compile-expression ?type ?slot ?value ?record)
-
           ;; Integer arithmetic
           [["jvm-iadd" [?x ?y]]]
           (&&host/compile-jvm-iadd compile-expression ?type ?x ?y)
@@ -334,9 +328,10 @@
     (fail "[Compiler Error] Can't compile expressions as top-level forms.")))
 
 (defn ^:private eval! [expr]
+  (prn 'eval! (aget expr 0))
+  ;; (assert false)
   (exec [eval-ctor &/get-eval-ctor
          :let [class-name (str eval-ctor)
-               class-file (str class-name ".class")
                =class (doto (new ClassWriter ClassWriter/COMPUTE_MAXS)
                         (.visit Opcodes/V1_5 (+ Opcodes/ACC_PUBLIC Opcodes/ACC_SUPER)
                                 class-name nil "java/lang/Object" nil)
@@ -354,7 +349,7 @@
                (return nil)))
          :let [bytecode (.toByteArray (doto =class
                                         .visitEnd))]
-         _ (&&/save-class! class-file bytecode)
+         _ (&&/save-class! class-name bytecode)
          loader &/loader]
     (-> (.loadClass loader class-name)
         (.getField "_eval")
diff --git a/src/lux/compiler/host.clj b/src/lux/compiler/host.clj
index c46684622..40ad7bb6d 100644
--- a/src/lux/compiler/host.clj
+++ b/src/lux/compiler/host.clj
@@ -40,22 +40,22 @@
       char-class "java.lang.Character"]
   (defn prepare-return! [*writer* *type*]
     (matchv ::M/objects [*type*]
-      [["lux;TNothing" nil]]
+      [["lux;NothingT" nil]]
       (.visitInsn *writer* Opcodes/ACONST_NULL)
 
-      [["lux;TData" ["char" _]]]
+      [["lux;DataT" ["char" _]]]
       (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host/->class char-class) "valueOf" (str "(C)" (&host/->type-signature char-class)))
 
-      [["lux;TData" ["int" _]]]
+      [["lux;DataT" ["int" _]]]
       (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host/->class integer-class) "valueOf" (str "(I)" (&host/->type-signature integer-class)))
 
-      [["lux;TData" ["long" _]]]
+      [["lux;DataT" ["long" _]]]
       (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host/->class long-class) "valueOf" (str "(J)" (&host/->type-signature long-class)))
 
-      [["lux;TData" ["boolean" _]]]
+      [["lux;DataT" ["boolean" _]]]
       (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host/->class boolean-class) "valueOf" (str "(Z)" (&host/->type-signature boolean-class)))
 
-      [["lux;TData" [_ _]]]
+      [["lux;DataT" [_ _]]]
       nil)
     *writer*))
 
diff --git a/src/lux/compiler/lambda.clj b/src/lux/compiler/lambda.clj
index 7d53fa739..cce87e978 100644
--- a/src/lux/compiler/lambda.clj
+++ b/src/lux/compiler/lambda.clj
@@ -65,7 +65,7 @@
                  $start (new Label)
                  $end (new Label)
                  _ (doto *writer*
-                     (-> (.visitLocalVariable (str &&/local-prefix idx) (&host/->java-sig (&/V "lux;TAny" nil)) nil $start $end (+ 2 idx))
+                     (-> (.visitLocalVariable (str &&/local-prefix idx) (&host/->java-sig (&/V "lux;AnyT" nil)) nil $start $end (+ 2 idx))
                          (->> (dotimes [idx num-locals])))
                      (.visitLabel $start))]
            ret (compile impl-body)
diff --git a/src/lux/compiler/lux.clj b/src/lux/compiler/lux.clj
index 412055956..a761f431a 100644
--- a/src/lux/compiler/lux.clj
+++ b/src/lux/compiler/lux.clj
@@ -132,99 +132,6 @@
          :let [_ (.visitMethodInsn *writer* Opcodes/INVOKEINTERFACE (&host/->class &host/function-class) "apply" &&/apply-signature)]]
     (return nil)))
 
-(defn compile-get [compile *type* ?slot ?record]
-  (exec [*writer* &/get-writer
-         _ (compile ?record)
-         :let [$then (new Label)
-               $test-else (new Label)
-               $end (new Label)
-               $start (new Label)
-               _ (doto *writer* ;; record
-                   (.visitInsn Opcodes/DUP) ;; record, record
-                   (.visitInsn Opcodes/ARRAYLENGTH) ;; record, length
-                   (.visitInsn Opcodes/ICONST_2) ;; record, length, 2
-                   (.visitInsn Opcodes/ISUB) ;; record, length--
-
-                   (.visitLabel $start)
-                   (.visitInsn Opcodes/DUP) ;; record, length, length
-                   (.visitLdcInsn (int -2)) ;; record, length, length, -2
-                   (.visitJumpInsn Opcodes/IF_ICMPEQ $then) ;; record, length
-                   ;;;
-                   (.visitInsn Opcodes/DUP2) ;; record, length, record, length
-                   (.visitInsn Opcodes/AALOAD) ;; record, length, aslot
-                   (.visitLdcInsn ?slot) ;; record, length, aslot, eslot
-                   (.visitMethodInsn Opcodes/INVOKEVIRTUAL (&host/->class "java.lang.Object") "equals" (str "(" (&host/->type-signature "java.lang.Object") ")Z")) ;; record, length, Z
-                   (.visitJumpInsn Opcodes/IFEQ $test-else) ;; record, length
-                   (.visitInsn Opcodes/ICONST_1) ;; record, length, 1
-                   (.visitInsn Opcodes/IADD) ;; record, length+
-                   (.visitInsn Opcodes/AALOAD) ;; value
-                   (.visitJumpInsn Opcodes/GOTO $end)
-                   (.visitLabel $test-else)
-                   (.visitInsn Opcodes/ICONST_2) ;; record, length, 2
-                   (.visitInsn Opcodes/ISUB) ;; record, length--
-                   (.visitJumpInsn Opcodes/GOTO $start)
-                   ;;;
-                   (.visitLabel $then)
-                   (.visitInsn Opcodes/POP) ;; record
-                   (.visitInsn Opcodes/POP) ;;
-                   (.visitInsn Opcodes/ACONST_NULL) ;; null
-                   (.visitLabel $end))]]
-    (return nil)))
-
-(let [o-sig (&host/->type-signature "java.lang.Object")]
-  (defn compile-set [compile *type* ?slot ?value ?record]
-    (exec [*writer* &/get-writer
-           _ (compile ?record)
-           :let [$then (new Label)
-                 $test-else (new Label)
-                 $end (new Label)
-                 $start (new Label)
-                 _ (doto *writer* ;; record1
-                     ;;;
-                     (.visitInsn Opcodes/DUP) ;; record1, record1
-                     (.visitInsn Opcodes/ARRAYLENGTH) ;; record1, length1
-                     (.visitTypeInsn Opcodes/ANEWARRAY (&host/->class "java.lang.Object")) ;; record1, record2
-                     (.visitInsn Opcodes/DUP_X1) ;; record2, record1, record2
-                     (.visitInsn Opcodes/ICONST_0) ;; record2, record1, record2, 0
-                     (.visitInsn Opcodes/SWAP) ;; record2, record1, 0, record2
-                     (.visitInsn Opcodes/DUP) ;; record2, record1, 0, record2, record2
-                     (.visitInsn Opcodes/ARRAYLENGTH) ;; record2, record1, 0, record2, length2
-                     (.visitInsn Opcodes/ICONST_0) ;; record2, record1, 0, record2, length2, 0
-                     (.visitInsn Opcodes/SWAP) ;; record2, record1, 0, record2, 0, length2
-                     (.visitMethodInsn Opcodes/INVOKESTATIC (&host/->class "java.lang.System") "arraycopy" (str "(" o-sig "I" o-sig "I" "I" ")V")) ;; record2
-                     ;;;
-                     (.visitInsn Opcodes/DUP) ;; record, record
-                     (.visitInsn Opcodes/ARRAYLENGTH) ;; record, length
-                     (.visitInsn Opcodes/ICONST_2) ;; record, length, 2
-                     (.visitInsn Opcodes/ISUB) ;; record, length--
-
-                     (.visitLabel $start)
-                     (.visitInsn Opcodes/DUP) ;; record, length, length
-                     (.visitLdcInsn (int -2)) ;; record, length, length, -2
-                     (.visitJumpInsn Opcodes/IF_ICMPEQ $then) ;; record, length
-                     ;;;
-                     (.visitInsn Opcodes/DUP2) ;; record, length, record, length
-                     (.visitInsn Opcodes/AALOAD) ;; record, length, aslot
-                     (.visitLdcInsn ?slot) ;; record, length, aslot, eslot
-                     (.visitMethodInsn Opcodes/INVOKEVIRTUAL (&host/->class "java.lang.Object") "equals" (str "(" (&host/->type-signature "java.lang.Object") ")Z")) ;; record, length, Z
-                     (.visitJumpInsn Opcodes/IFEQ $test-else) ;; record, length
-                     (.visitInsn Opcodes/DUP2) ;; record, length, record, length
-                     (.visitInsn Opcodes/ICONST_1) ;; record, length, record, length, 1
-                     (.visitInsn Opcodes/IADD) ;; record, length, record, length+
-                     (do (compile ?value)) ;; record, length, record, length+, value
-                     (.visitInsn Opcodes/AASTORE) ;; record, length
-                     (.visitInsn Opcodes/POP) ;; record
-                     (.visitJumpInsn Opcodes/GOTO $end)
-                     (.visitLabel $test-else)
-                     (.visitInsn Opcodes/ICONST_2) ;; record, length, 2
-                     (.visitInsn Opcodes/ISUB) ;; record, length--
-                     (.visitJumpInsn Opcodes/GOTO $start)
-                     ;;;
-                     (.visitLabel $then)
-                     (.visitInsn Opcodes/POP) ;; record
-                     (.visitLabel $end))]]
-      (return nil))))
-
 (defn compile-def [compile ?name ?body]
   (exec [*writer* &/get-writer
          module-name &/get-module-name
diff --git a/src/lux/host.clj b/src/lux/host.clj
index 6432a6d5f..1dda5de5d 100644
--- a/src/lux/host.clj
+++ b/src/lux/host.clj
@@ -19,8 +19,8 @@
                                               "")
                                             (.getSimpleName class)))]
     (if (= "void" base)
-      (return (&/V "lux;TNothing" nil))
-      (let [base* (&/V "lux;TData" (&/T base (&/V "lux;Nil" nil)))]
+      (return (&/V "lux;NothingT" nil))
+      (let [base* (&/V "lux;DataT" (&/T base (&/V "lux;Nil" nil)))]
         (if arr-level
           (return (reduce (fn [inner _]
                             (&/V "array" (&/V "lux;Cons" (&/T inner (&/V "lux;Nil" nil)))))
@@ -81,19 +81,19 @@
 
 (defn ->java-sig [type]
   (matchv ::M/objects [type]
-    [["lux;TAny" _]]
+    [["lux;AnyT" _]]
     (->type-signature "java.lang.Object")
 
-    [["lux;TNothing" _]]
+    [["lux;NothingT" _]]
     "V"
     
-    [["lux;TData" ["array" ["lux;Cons" [?elem ["lux;Nil" _]]]]]]
+    [["lux;DataT" ["array" ["lux;Cons" [?elem ["lux;Nil" _]]]]]]
     (str "[" (->java-sig ?elem))
 
-    [["lux;TData" [?name ?params]]]
+    [["lux;DataT" [?name ?params]]]
     (->type-signature ?name)
 
-    [["lux;TLambda" [_ _]]]
+    [["lux;LambdaT" [_ _]]]
     (->type-signature function-class)))
 
 (defn extract-jvm-param [token]
diff --git a/src/lux/type.clj b/src/lux/type.clj
index 68fb13b3d..7d05d65b4 100644
--- a/src/lux/type.clj
+++ b/src/lux/type.clj
@@ -2,12 +2,23 @@
   (:refer-clojure :exclude [deref apply merge])
   (:require [clojure.core.match :as M :refer [match matchv]]
             clojure.core.match.array
-            [lux.base :as & :refer [exec return* return fail fail* assert!]]))
+            [lux.base :as & :refer [exec return* return fail fail* assert! |let]]))
 
 ;; [Util]
 (def ^:private success (return nil))
 
-(defn ^:private deref [id]
+(defn lookup [type]
+  (matchv ::M/objects [type]
+    [["lux;VarT" id]]
+    (fn [state]
+      (if-let [type* (->> state (&/get$ "lux;types") (&/get$ "lux;mappings") (&/|get id))]
+        (return* state type*)
+        (fail* (str "Unknown type-var: " id))))
+
+    [_]
+    (fail "[Type Error] Can't lookup non-vars.")))
+
+(defn deref [id]
   (fn [state]
     (if-let [type* (->> state (&/get$ "lux;types") (&/get$ "lux;mappings") (&/|get id))]
       (matchv ::M/objects [type*]
@@ -18,7 +29,7 @@
         (fail* (str "Unbound type-var: " id)))
       (fail* (str "Unknown type-var: " id)))))
 
-(defn ^:private reset [id type]
+(defn reset [id type]
   (fn [state]
     (if-let [_ (->> state (&/get$ "lux;types") (&/get$ "lux;mappings") (&/|get id))]
       (return* (&/update$ "lux;types" (fn [ts] (&/update$ "lux;mappings" #(&/|put id (&/V "lux;Some" type) %)
@@ -35,147 +46,79 @@
                                             (&/update$ "lux;counter" inc)
                                             (&/update$ "lux;mappings" (fn [ms] (&/|put id (&/V "lux;None" nil) ms))))
                           state)
-               (&/V "lux;TVar" id)))))
+               (&/V "lux;VarT" id)))))
 
 (def fresh-lambda
   (exec [=arg fresh-var
          =return fresh-var]
-    (return (&/V "lux;TLambda" (&/T =arg =return)))))
-
-(defn ^:private ->type [pseudo-type]
-  (match pseudo-type
-    [::Any]
-    (&/V "lux;TAny" nil)
-
-    [::Nothing]
-    (&/V "lux;TNothing" nil)
-
-    [::Data ?name ?elems]
-    (&/V "lux;TData" (&/T ?name ?elems))
-
-    [::Tuple ?members]
-    (&/V "lux;TTuple" (&/|map ->type ?members))
-    
-    [::Variant ?members]
-    (&/V "lux;TVariant" (&/|map (fn [[k v]] (&/T k (->type v)))
-                                ?members))
-
-    [::Record ?members]
-    (&/V "lux;TRecord" (&/|map (fn [[k v]] (&/T k (->type v)))
-                               ?members))
-
-    [::Lambda ?input ?output]
-    (&/V "lux;TLambda" (&/T (->type ?input) (->type ?output)))
-    
-    [::App ?lambda ?param]
-    (&/V "lux;TApp" (&/T (->type ?lambda) (->type ?param)))
-
-    [::Bound ?name]
-    (&/V "lux;TBound" ?name)
-
-    [::Var ?id]
-    (&/V "lux;TVar" ?id)
-
-    [::All ?env ?name ?arg ?body]
-    (&/V "lux;TAll" (&/T (&/|map (fn [[k v]] (&/T k (->type v)))
-                                 ?env)
-                         ?name
-                         ?arg
-                         (->type ?body)))
-    ))
-
-(def +list+
-  [::All (&/|list) "List" "a"
-   [::Variant (&/|list ["lux;Cons" [::Tuple (&/|list [::Bound "a"] [::App [::Bound "List"] [::Bound "a"]])]]
-                       ["lux;Nil" [::Tuple (&/|list)]])]])
-
-(def +type+
-  (let [text [::Data "java.lang.String" (&/|list)]
-        type [::App [::Bound "Type"] [::Any]]
-        list-of-types [::App +list+ type]
-        string=>type [::App +list+ [::Tuple (&/|list text type)]]]
-    (->type [::All (&/|list) "Type" "_"
-             [::Variant (&/|list ["lux;TAny"  [::Tuple (&/|list)]]
-                                 ["lux;TNothing"  [::Tuple (&/|list)]]
-                                 ["lux;TData" [::Tuple (&/|list text list-of-types)]]
-                                 ["lux;TTuple" list-of-types]
-                                 ["lux;TVariant" string=>type]
-                                 ["lux;TRecord" string=>type]
-                                 ["lux;TLambda" [::Tuple (&/|list type
-                                                                  type)]]
-                                 ["lux;TApp" [::Tuple (&/|list type
-                                                               type)]]
-                                 ["lux;TBound" text]
-                                 ["lux;TVar" [::Data "java.lang.Long" (&/|list)]]
-                                 ["lux;TAll" [::Tuple (&/|list string=>type text text type)]]
-                                 )]])))
+    (return (&/V "lux;LambdaT" (&/T =arg =return)))))
 
 (defn clean [tvar type]
   (matchv ::M/objects [tvar]
-    [["lux;TVar" ?tid]]
+    [["lux;VarT" ?tid]]
     (matchv ::M/objects [type]
-      [["lux;TVar" ?id]]
+      [["lux;VarT" ?id]]
       (if (= ?tid ?id)
         (&/try-all% (&/|list (exec [=type (deref ?id)]
                                (clean tvar =type))
                              (return type)))
         (return type))
       
-      [["lux;TLambda" [?arg ?return]]]
+      [["lux;LambdaT" [?arg ?return]]]
       (exec [=arg (clean tvar ?arg)
              =return (clean tvar ?return)]
-        (return (&/V "lux;TLambda" (to-array [=arg =return]))))
+        (return (&/V "lux;LambdaT" (to-array [=arg =return]))))
 
-      [["lux;TApp" [?lambda ?param]]]
+      [["lux;AppT" [?lambda ?param]]]
       (exec [=lambda (clean tvar ?lambda)
              =param (clean tvar ?param)]
-        (return (&/V "lux;TApp" (to-array [=lambda =param]))))
+        (return (&/V "lux;AppT" (to-array [=lambda =param]))))
 
-      [["lux;TTuple" ?members]]
+      [["lux;TupleT" ?members]]
       (exec [=members (&/map% (partial clean tvar) ?members)]
-        (return (&/V "lux;TTuple" =members)))
+        (return (&/V "lux;TupleT" =members)))
       
-      [["lux;TVariant" ?members]]
+      [["lux;VariantT" ?members]]
       (exec [=members (&/map% (fn [[k v]]
                                 (exec [=v (clean tvar v)]
                                   (return (to-array [k =v]))))
                               ?members)]
-        (return (&/V "lux;TVariant" =members)))
+        (return (&/V "lux;VariantT" =members)))
 
-      [["lux;TRecord" ?members]]
+      [["lux;RecordT" ?members]]
       (exec [=members (&/map% (fn [[k v]]
                                 (exec [=v (clean tvar v)]
                                   (return (to-array [k =v]))))
                               ?members)]
-        (return (&/V "lux;TRecord" =members)))
+        (return (&/V "lux;RecordT" =members)))
 
-      [["lux;TAll" [?env ?name ?arg ?body]]]
+      [["lux;AllT" [?env ?name ?arg ?body]]]
       (exec [=env (&/map% (fn [[k v]]
                             (exec [=v (clean tvar v)]
                               (return (to-array [k =v]))))
                           ?env)]
-        (return (&/V "lux;TAll" (to-array [=env ?name ?arg ?body]))))
+        (return (&/V "lux;AllT" (to-array [=env ?name ?arg ?body]))))
 
       [_]
       (return type)
       )))
 
 (defn show-type [type]
-  (prn 'show-type (aget type 0))
+  ;; (prn 'show-type (aget type 0))
   (matchv ::M/objects [type]
-    [["lux;TAny" _]]
+    [["lux;AnyT" _]]
     "Any"
 
-    [["lux;TNothing" _]]
+    [["lux;NothingT" _]]
     "Nothing"
 
-    [["lux;TData" [name params]]]
+    [["lux;DataT" [name params]]]
     (str "(^ " name " [" (->> params (&/|map show-type) (&/|interpose " ") (&/fold str "")) "])")
 
-    [["lux;TTuple" elems]]
+    [["lux;TupleT" elems]]
     (str "(, " (->> elems (&/|map show-type) (&/|interpose " ") (&/fold str "")) ")")
 
-    [["lux;TVariant" cases]]
+    [["lux;VariantT" cases]]
     (str "(| " (->> cases
                     (&/|map (fn [kv]
                               (matchv ::M/objects [kv]
@@ -188,7 +131,7 @@
                     (&/fold str "")) ")")
     
 
-    [["lux;TRecord" fields]]
+    [["lux;RecordT" fields]]
     (str "(& " (->> fields
                     (&/|map (fn [kv]
                               (matchv ::M/objects [kv]
@@ -197,140 +140,146 @@
                     (&/|interpose " ")
                     (&/fold str "")) ")")
 
-    [["lux;TLambda" [input output]]]
+    [["lux;LambdaT" [input output]]]
     (str "(-> " (show-type input) " " (show-type output) ")")
 
-    [["lux;TVar" id]]
+    [["lux;VarT" id]]
     (str "⌈" id "⌋")
 
-    [["lux;TBound" name]]
+    [["lux;BoundT" name]]
     name
 
-    [["lux;TApp" [?lambda ?param]]]
+    [["lux;AppT" [?lambda ?param]]]
     (str "(" (show-type ?lambda) " " (show-type ?param) ")")
     
-    [["lux;TAll" [?env ?name ?arg ?body]]]
+    [["lux;AllT" [?env ?name ?arg ?body]]]
     (str "(All " ?name " " ?arg " " (show-type ?body) ")")
     ))
 
+(defn type= [x y]
+  (matchv ::M/objects [x y]
+    [["lux;AnyT" _] ["lux;AnyT" _]]
+    true
+
+    [["lux;NothingT" _] ["lux;NothingT" _]]
+    true
+
+    [["lux;DataT" [xname xparams]] ["lux;DataT" [yname yparams]]]
+    (&/fold (fn [old xy] (and old (type= (aget xy 0) (aget xy 1))))
+            (= xname yname)
+            (&/zip2 xparams yparams))
+
+    [["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]
+      [["lux;Nil" _]]
+      (&/V "lux;None" nil)
+
+      [["lux;Cons" [[[e* a*] v*] xs*]]]
+      (if (and (type= e e*)
+               (type= a a*))
+        (&/V "lux;Some" v*)
+        (fp-get k xs*))
+      )))
+
+(defn ^:private fp-put [k v fixpoints]
+  (&/|cons (&/T k v) fixpoints))
+
 (defn ^:private solve-error [expected actual]
   (str "Type " (show-type expected) " does not subsume type " (show-type actual)))
 
-(defn solve [expected actual]
-  ;; (prn 'solve expected actual)
-  ;; (prn 'solve (aget expected 0) (aget actual 0))
-  success
-  ;; (matchv ::M/objects [expected actual]
-  ;;   [["Any" _] _]
-  ;;   success
-
-  ;;   [_ ["Nothing" _]]
-  ;;   success
-
-  ;;   [["Data" [e!name e!params]] ["Data" [a!name a!params]]]
-  ;;   (if (or (= e!name a!name)
-  ;;           (.isAssignableFrom (Class/forName e!name) (Class/forName a!name)))
-  ;;     success
-  ;;     (fail (str "not (" actual " <= " expected ")")))
-  
-  ;;   [["Tuple" e!elems] ["Tuple" a!elems]]
-  ;;   (exec [_ (assert! (= (&/|length e!elems) (&/|length a!elems))
-  ;;                     "Tuples must have matching element sizes.")
-  ;;          _ (&/map% (fn [n g] (solve n g))
-  ;;                  (&/zip2 e!elems a!elems))]
-  ;;     success)
-
-  ;;   [["Variant" e!cases] ["Variant" a!cases]]
-  ;;   (exec [_ (&/map% (fn [slot]
-  ;;                    (solve (&/|get e!cases slot) (&/|get a!cases slot)))
-  ;;                  (&/|keys a!cases))]
-  ;;     success)
-
-  ;;   [["Record" e!fields] ["Record" a!fields]]
-  ;;   (exec [_ (&/map% (fn [slot]
-  ;;                    (solve (&/|get e!fields slot) (&/|get a!fields slot)))
-  ;;                  (&/|keys e!fields))]
-  ;;     success)
-
-  ;;   [["Lambda" [e!input e!output]] ["Lambda" [a!input a!output]]]
-  ;;   (exec [_ (solve a!input e!input)]
-  ;;     (solve e!output a!output))
-
-  ;;   [["Var" e!id] _]
-  ;;   (&/try-all% (&/|list (exec [=e!type (deref e!id)
-  ;;                               _ (solve =e!type actual)
-  ;;                               _ (reset e!id =e!type)]
-  ;;                          success)
-  ;;                        (exec [_ (reset e!id actual)]
-  ;;                          success)))
-
-  ;;   [_ ["Var" a!id]]
-  ;;   (&/try-all% (&/|list (exec [=a!type (deref a!id)
-  ;;                               _ (solve expected =a!type)
-  ;;                               _ (reset a!id =a!type)]
-  ;;                          success)
-  ;;                        (exec [_ (reset a!id expected)]
-  ;;                          success)))
-
-  ;;   [_ _]
-  ;;   (solve-error expected actual)
-  ;;   )
-  )
+(defn beta-reduce [env type]
+  ;; (prn 'beta-reduce (aget type 0))
+  (matchv ::M/objects [type]
+    [["lux;VariantT" ?cases]]
+    (&/V "lux;VariantT" (&/|map (fn [kv]
+                                  (|let [[k v] kv]
+                                    (&/T k (beta-reduce env v))))
+                                ?cases))
 
-(let [&& #(and %1 %2)]
-  (defn merge [x y]
-    (matchv ::M/objects [x y]
-      [_ ["lux;TAny" _]]
-      (return y)
+    [["lux;RecordT" ?fields]]
+    (&/V "lux;RecordT" (&/|map (fn [kv]
+                                 (|let [[k v] kv]
+                                   (&/T k (beta-reduce env v))))
+                               ?fields))
 
-      [["lux;TAny" _] _]
-      (return x)
+    [["lux;TupleT" ?members]]
+    (&/V "lux;TupleT" (&/|map (partial beta-reduce env) ?members))
 
-      [_ ["lux;TNothing" _]]
-      (return x)
+    [["lux;DataT" [?name ?params]]]
+    (&/V "lux;DataT" (&/T ?name (&/|map (partial beta-reduce env) ?params)))
 
-      [["lux;TNothing" _] _]
-      (return y)
+    [["lux;AppT" [?type-fn ?type-arg]]]
+    (&/V "lux;AppT" (&/T (beta-reduce env ?type-fn) (beta-reduce env ?type-arg)))
 
-      ;;;
-      
-      [_ _]
-      (return x)
+    [["lux;AllT" [?local-env ?local-name ?local-arg ?local-def]]]
+    (&/V "lux;AllT" (&/T (&/|merge ?local-env env) ?local-name ?local-arg ?local-def))
 
-      ;; [["Variant" x!cases] ["Variant" y!cases]]
-      ;; (if (and (reduce && true
-      ;;                  (for [[xslot xtype] (keys x!cases)]
-      ;;                    (if-let [ytype (get y!cases xslot)]
-      ;;                      (= xtype ytype)
-      ;;                      true)))
-      ;;          (reduce && true
-      ;;                  (for [[yslot ytype] (keys y!cases)]
-      ;;                    (if-let [xtype (get x!cases yslot)]
-      ;;                      (= xtype ytype)
-      ;;                      true))))
-      ;;   (return (&/V "Variant" (clojure.core/merge x!cases y!cases)))
-      ;;   (fail (str "Incompatible variants: " (pr-str x) " and " (pr-str y))))
-
-      ;; [["Record" x!fields] ["Record" y!fields]]
-      ;; (if (and (= (keys x!fields) (keys y!fields))
-      ;;          (->> (keys x!fields)
-      ;;               (map #(= (get x!fields %) (get y!fields %)))
-      ;;               (reduce && true)))
-      ;;   (return x)
-      ;;   (fail (str "Incompatible records: " (pr-str x) " and " (pr-str y))))
-      
-      [_ _]
-      (fail (str "[Type System] Can't merge types: " (pr-str x) " and " (pr-str y))))))
+    [["lux;LambdaT" [?input ?output]]]
+    (&/V "lux;LambdaT" (&/T (beta-reduce env ?input) (beta-reduce env ?output)))
 
-(defn apply-lambda [func param]
-  (matchv ::M/objects [func]
-    [["lux;TLambda" [input output]]]
-    (exec [_ (solve input param)]
-      (return output))
+    [["lux;BoundT" ?name]]
+    (if-let [bound (&/|get ?name env)]
+      (do ;; (prn 'beta-reduce "lux;BoundT" ?name (->> (&/|keys env) (&/|interpose " ") (&/fold str ""))
+          ;;      (show-type bound))
+        (beta-reduce env bound))
+      type)
 
     [_]
-    (return (&/V "lux;TAny" nil))
-    ;; (fail (str "[Type System] Can't apply type " (str func) " to type " (str param)))
+    type
     ))
 
 (defn slot-type [record slot]
@@ -342,4 +291,241 @@
       [["lux;Right" type]]
       (return* state type))))
 
-(def +dont-care+ (&/V "lux;TAny" nil))
+(def +dont-care+ (&/V "lux;AnyT" nil))
+
+(defn apply-type [type-fn param]
+  (prn 'apply-type (aget type-fn 0) (aget param 0))
+  (matchv ::M/objects [type-fn]
+    [["lux;AllT" [local-env local-name local-arg local-def]]]
+    (return (beta-reduce (->> local-env
+                              (&/|put local-name type-fn)
+                              (&/|put local-arg param))
+                         local-def))
+
+    [["lux;AppT" [F A]]]
+    (exec [type-fn* (apply-type F A)]
+      (apply-type type-fn* param))
+    
+    [_]
+    (fail (str "[Type System] Can't apply type function " (show-type type-fn) " to type " (show-type param)))))
+
+(def init-fixpoints (&/|list))
+
+(defn solve [fixpoints expected actual]
+  (prn 'solve (aget expected 0) (aget actual 0))
+  ;; (prn 'solve (show-type expected) (show-type actual))
+  (matchv ::M/objects [expected actual]
+    [["Any" _] _]
+    success
+
+    [_ ["Nothing" _]]
+    success
+
+    [["lux;VarT" ?id] _]
+    (&/try-all% (&/|list (exec [bound (deref ?id)]
+                           (solve fixpoints bound actual))
+                         (reset ?id actual)))
+    
+    [_ ["lux;VarT" ?id]]
+    (&/try-all% (&/|list (exec [bound (deref ?id)]
+                           (solve fixpoints expected bound))
+                         (reset ?id expected)))
+
+    [["lux;AppT" [F A]] _]
+    (exec [expected* (apply-type F A)
+           :let [fp-pair (&/T expected actual)]]
+      (matchv ::M/objects [(fp-get fp-pair fixpoints)]
+        [["lux;Some" ?]]
+        (if ?
+          success
+          (fail (solve-error expected actual)))
+
+        [["lux;None" _]]
+        (solve (fp-put fp-pair true fixpoints) expected* actual)))
+
+    [_ ["lux;AppT" [F A]]]
+    (exec [actual* (apply-type F A)]
+      (solve fixpoints expected actual*))
+
+    [["lux;AllT" _] _]
+    (exec [$var fresh-var
+           expected* (apply-type expected $var)]
+      (solve fixpoints expected* actual))
+
+    [_ ["lux;AllT" _]]
+    (exec [$var fresh-var
+           actual* (apply-type actual $var)]
+      (solve fixpoints expected actual*))
+
+    [["lux;DataT" [e!name e!params]] ["lux;DataT" [a!name a!params]]]
+    (cond (not= e!name a!name)
+          (fail (str "[Type Error] Names don't match: " e!name " & " a!name))
+          
+          (not= (&/|length e!params) (&/|length a!params))
+          (fail "[Type Error] Params don't match in size.")
+
+          :else
+          (exec [_ (&/map% (fn [ea]
+                             (|let [[e a] ea]
+                               (solve fixpoints e a)))
+                           (&/zip2 e!params a!params))]
+            success))
+
+    [["lux;LambdaT" [eI eO]] ["lux;LambdaT" [aI aO]]]
+    (exec [_ (solve fixpoints aI eI)]
+      (solve fixpoints eO aO))
+
+    [["lux;TupleT" e!members] ["lux;TupleT" a!members]]
+    (if (= (&/|length e!members) (&/|length a!members))
+      (exec [_ (&/map% (fn [ea]
+                         (|let [[e a] ea]
+                           (do (prn "lux;TupleT" 'ITER (show-type e) (show-type a))
+                             (solve fixpoints e a))))
+                       (&/zip2 e!members a!members))
+             :let [_ (prn "lux;TupleT" 'DONE)]]
+        success)
+      (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]]
+    (exec [_ (&/map% (fn [kv]
+                       (|let [[k av] kv]
+                         (if-let [ev (&/|get k e!cases)]
+                           (solve fixpoints ev av)
+                           (fail (str "[Type Error] The expected variant cannot handle case: #" k)))))
+                     a!cases)]
+      success)
+
+    [["lux;RecordT" e!fields] ["lux;RecordT" a!fields]]
+    (if (= (&/|length e!fields) (&/|length a!fields))
+      (exec [_ (&/map% (fn [slot]
+                         (if-let [e!type (&/|get e!fields slot)]
+                           (if-let [a!type (&/|get a!fields slot)]
+                             (solve fixpoints e!type a!type)
+                             (fail (solve-error expected actual)))
+                           (fail (solve-error expected actual))))
+                       (&/|keys e!fields))]
+        success)
+      (fail "[Type Error] Records don't match in size."))
+
+    [["lux;BoundT" name] _]
+    (do (prn "lux;BoundT" name)
+      (assert false))
+    ;; ...
+    
+    ;; [_ ["lux;BoundT" name]]
+    ;; ...
+    ))
+
+(defn apply-lambda [func param]
+  (matchv ::M/objects [func]
+    [["lux;LambdaT" [input output]]]
+    (exec [_ (solve init-fixpoints input param)]
+      (return output))
+
+    [_]
+    (fail (str "[Type System] Can't apply type " (show-type func) " to type " (show-type param)))
+    ))
+
+(def Any (&/V "lux;AnyT" nil))
+(def Int (&/V "lux;DataT" (&/T "java.lang.Long" (&/|list))))
+(def Text (&/V "lux;DataT" (&/T "java.lang.String" (&/|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))
+        TypeList (&/V "lux;AppT" (&/T List Type))
+        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" (&/V "lux;TupleT" (&/|list Text TypeList)))
+                                                                           (&/T "lux;TupleT" TypeList)
+                                                                           (&/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)))))
+
+(let [&& #(and %1 %2)]
+  (defn merge [x y]
+    (matchv ::M/objects [x y]
+      [_ ["lux;AnyT" _]]
+      (return y)
+
+      [["lux;AnyT" _] _]
+      (return x)
+
+      [_ ["lux;NothingT" _]]
+      (return x)
+
+      [["lux;NothingT" _] _]
+      (return y)
+
+      [["lux;VariantT" x!cases] ["lux;VariantT" y!cases]]
+      (exec [cases (&/fold% (fn [cases kv]
+                              (matchv ::M/objects [kv]
+                                [[k v]]
+                                (if-let [cv (&/|get k cases)]
+                                  (exec [_ (solve init-fixpoints cv v)]
+                                    (return cases))
+                                  (return (&/|put k v cases)))))
+                            x!cases
+                            y!cases)]
+        (return (&/V "lux;VariantT" cases)))
+      
+      [["lux;RecordT" x!fields] ["lux;RecordT" y!fields]]
+      (if (= (&/|length x!fields) (&/|length y!fields))
+        (exec [fields (&/fold% (fn [fields kv]
+                                 (matchv ::M/objects [kv]
+                                   [[k v]]
+                                   (if-let [cv (&/|get k fields)]
+                                     (exec [_ (solve init-fixpoints cv v)]
+                                       (return fields))
+                                     (fail (str "[Type System Error] Incompatible records: " (show-type x) " and " (show-type y))))))
+                               x!fields
+                               y!fields)]
+          (return (&/V "lux;RecordT" fields)))
+        (fail (str "[Type System Error] Incompatible records: " (show-type x) " and " (show-type y))))
+      
+      [_ _]
+      (fail (str "[Type System Error] Can't merge types: " (show-type x) " and " (show-type y))))))
+
+(comment
+  (do (def Real (&/V "lux;DataT" (&/T "java.lang.Long" (&/|list))))
+    (def RealT (&/V "lux;VariantT" (&/|list (&/T "lux;DataT" (&/V "lux;TupleT" (&/|list Text
+                                                                                        (&/V "lux;VariantT" (&/|list (&/T "lux;Nil" (&/V "lux;TupleT" (&/|list)))))))))))
+    )
+  
+  (matchv ::M/objects [((solve init-fixpoints Type RealT)
+                        (&/init-state nil))]
+    [["lux;Left" ?msg]]
+    (assert false ?msg)
+
+    [_]
+    (println "YEAH!"))
+
+  (matchv ::M/objects [((solve init-fixpoints List (&/V "lux;AppT" (&/T List Real)))
+                        (&/init-state nil))]
+    [["lux;Left" ?msg]]
+    (assert false ?msg)
+
+    [_]
+    (println "YEAH!"))
+  )