[2nd Super Refactoring That Breaks The System: Part 1]

- Finishing implementing the type-system.
- Migrating more of the data-structures used in the compiler to the ones used by Lux itself.

14 files changed, 651 insertions, 580 deletions

diff --git a/src/lux.clj b/src/lux.clj
index 508b45bb9..c7b000e5b 100644
--- a/src/lux.clj
+++ b/src/lux.clj
@@ -19,7 +19,3 @@
   ;; jar cvf test2.jar *.class test2 && java -cp "test2.jar" test2
   ;; cd output && jar cvf test2.jar * && java -cp "test2.jar" test2 && cd ..
   )
-
-
-
-
diff --git a/src/lux/analyser.clj b/src/lux/analyser.clj
index 8c8bb61d1..123783daa 100644
--- a/src/lux/analyser.clj
+++ b/src/lux/analyser.clj
@@ -3,7 +3,8 @@
             [clojure.core.match :as M :refer [match matchv]]
             clojure.core.match.array
             (lux [base :as & :refer [exec return fail
-                                     try-all-m map-m mapcat-m reduce-m
+                                     |list
+                                     try-all-m map-m |flat-map% reduce-m
                                      assert!]]
                  [parser :as &parser]
                  [type :as &type]
@@ -28,202 +29,208 @@
                                ["Nil" _]]]]]]]
     [catch+ ?finally-body]))
 
-(defn ^:private analyse-basic-ast [analyse-ast token]
+(defn ^:private analyse-basic-ast [analyse eval! token]
   ;; (prn 'analyse-basic-ast token (&/show-ast token))
   (matchv ::M/objects [token]
     ;; Standard special forms
     [["Bool" ?value]]
-    (return (list [::&&/Expression [::&&/bool ?value] [::&type/Data "java.lang.Boolean"]]))
+    (return (|list [::&&/Expression [::&&/bool ?value] (&/V "Data" (to-array ["java.lang.Boolean" (&/V "Nil" nil)]))]))
 
     [["Int" ?value]]
-    (return (list [::&&/Expression [::&&/int ?value]  [::&type/Data "java.lang.Long"]]))
+    (return (|list [::&&/Expression [::&&/int ?value]  (&/V "Data" (to-array ["java.lang.Long" (&/V "Nil" nil)]))]))
 
     [["Real" ?value]]
-    (return (list [::&&/Expression [::&&/real ?value] [::&type/Data "java.lang.Double"]]))
+    (return (|list [::&&/Expression [::&&/real ?value] (&/V "Data" (to-array ["java.lang.Double" (&/V "Nil" nil)]))]))
 
     [["Char" ?value]]
-    (return (list [::&&/Expression [::&&/char ?value] [::&type/Data "java.lang.Character"]]))
+    (return (|list [::&&/Expression [::&&/char ?value] (&/V "Data" (to-array ["java.lang.Character" (&/V "Nil" nil)]))]))
 
     [["Text" ?value]]
-    (return (list [::&&/Expression [::&&/text ?value] [::&type/Data "java.lang.String"]]))
+    (return (|list [::&&/Expression [::&&/text ?value] (&/V "Data" (to-array ["java.lang.String" (&/V "Nil" nil)]))]))
 
     [["Tuple" ?elems]]
-    (&&lux/analyse-tuple analyse-ast (&/->seq ?elems))
+    (&&lux/analyse-tuple analyse ?elems)
 
     [["Record" ?elems]]
-    (&&lux/analyse-record analyse-ast (&/->seq ?elems))
+    (&&lux/analyse-record analyse ?elems)
 
     [["Tag" ?tag]]
-    (let [tuple-type [::&type/Tuple (list)]]
-      (return (list [::&&/Expression [::&&/variant ?tag [::&&/Expression [::&&/tuple (list)] tuple-type]]
-                     [::&type/Variant (list [?tag tuple-type])]])))
+    (let [tuple-type (&/V "Tuple" (&/V "Nil" nil))]
+      (return (|list [::&&/Expression [::&&/variant ?tag [::&&/Expression [::&&/tuple (list)] tuple-type]]
+                     (&/V "Variant" (&/V "Cons" (to-array [(to-array [?tag tuple-type]) (&/V "Nil" nil)])))])))
 
     [["Ident" "jvm-null"]]
-    (return (list [::&&/Expression [::&&/jvm-null] [::&type/Data "null"]]))
+    (return (|list [::&&/Expression [::&&/jvm-null] (&/V "Data" (to-array ["null" (&/V "Nil" nil)]))]))
     
     [["Ident" ?ident]]
-    (&&lux/analyse-ident analyse-ast ?ident)
+    (&&lux/analyse-ident analyse ?ident)
 
     [["Form" ["Cons" [["Ident" "case'"]
                       ["Cons" [?variant ?branches]]]]]]
-    (&&lux/analyse-case analyse-ast ?variant (&/->seq ?branches))
+    (&&lux/analyse-case analyse ?variant (&/->seq ?branches))
     
     [["Form" ["Cons" [["Ident" "lambda'"]
                       ["Cons" [["Ident" ?self]
                                ["Cons" [["Ident" ?arg]
                                         ["Cons" [?body
                                                  ["Nil" _]]]]]]]]]]]
-    (&&lux/analyse-lambda analyse-ast ?self ?arg ?body)
+    (&&lux/analyse-lambda analyse ?self ?arg ?body)
 
     [["Form" ["Cons" [["Ident" "get@'"] ["Cons" [["Tag" ?slot] ["Cons" [?record ["Nil" _]]]]]]]]]
-    (&&lux/analyse-get analyse-ast ?slot ?record)
+    (&&lux/analyse-get analyse ?slot ?record)
 
     [["Form" ["Cons" [["Ident" "set@'"] ["Cons" [["Tag" ?slot] ["Cons" [?value ["Cons" [?record ["Nil" _]]]]]]]]]]]
-    (&&lux/analyse-set analyse-ast ?slot ?value ?record)
+    (&&lux/analyse-set analyse ?slot ?value ?record)
 
     [["Form" ["Cons" [["Ident" "def'"] ["Cons" [["Ident" ?name] ["Cons" [?value ["Nil" _]]]]]]]]]
-    (&&lux/analyse-def analyse-ast ?name ?value)
+    (&&lux/analyse-def analyse ?name ?value)
 
     [["Form" ["Cons" [["Ident" "declare-macro"] ["Cons" [["Ident" ?ident] ["Nil" _]]]]]]]
     (&&lux/analyse-declare-macro ?ident)
     
     [["Form" ["Cons" [["Ident" "import'"] ["Cons" [["Text" ?path] ["Nil" _]]]]]]]
-    (&&lux/analyse-import analyse-ast ?path)
+    (&&lux/analyse-import analyse ?path)
+
+    [["Form" ["Cons" [["Ident" ":"] ["Cons" [?value ["Cons" [?type ["Nil" _]]]]]]]]]
+    (&&lux/analyse-check analyse eval! ?type ?value)
+
+    [["Form" ["Cons" [["Ident" "coerce"] ["Cons" [?type ["Cons" [?value ["Nil" _]]]]]]]]]
+    (&&lux/analyse-coerce analyse eval! ?type ?value)
 
     ;; Host special forms
     [["Form" ["Cons" [["Ident" "exec"] ?exprs]]]]
-    (&&host/analyse-exec analyse-ast (&/->seq ?exprs))
+    (&&host/analyse-exec analyse (&/->seq ?exprs))
 
     ;; Integer arithmetic
     [["Form" ["Cons" [["Ident" "jvm-iadd"] ["Cons" [?y ["Cons" [?x ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-iadd analyse-ast ?x ?y)
+    (&&host/analyse-jvm-iadd analyse ?x ?y)
 
     [["Form" ["Cons" [["Ident" "jvm-isub"] ["Cons" [?y ["Cons" [?x ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-isub analyse-ast ?x ?y)
+    (&&host/analyse-jvm-isub analyse ?x ?y)
 
     [["Form" ["Cons" [["Ident" "jvm-imul"] ["Cons" [?y ["Cons" [?x ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-imul analyse-ast ?x ?y)
+    (&&host/analyse-jvm-imul analyse ?x ?y)
 
     [["Form" ["Cons" [["Ident" "jvm-idiv"] ["Cons" [?y ["Cons" [?x ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-idiv analyse-ast ?x ?y)
+    (&&host/analyse-jvm-idiv analyse ?x ?y)
 
     [["Form" ["Cons" [["Ident" "jvm-irem"] ["Cons" [?y ["Cons" [?x ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-irem analyse-ast ?x ?y)
+    (&&host/analyse-jvm-irem analyse ?x ?y)
 
     [["Form" ["Cons" [["Ident" "jvm-ieq"] ["Cons" [?y ["Cons" [?x ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-ieq analyse-ast ?x ?y)
+    (&&host/analyse-jvm-ieq analyse ?x ?y)
 
     [["Form" ["Cons" [["Ident" "jvm-ilt"] ["Cons" [?y ["Cons" [?x ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-ilt analyse-ast ?x ?y)
+    (&&host/analyse-jvm-ilt analyse ?x ?y)
 
     [["Form" ["Cons" [["Ident" "jvm-igt"] ["Cons" [?y ["Cons" [?x ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-igt analyse-ast ?x ?y)
+    (&&host/analyse-jvm-igt analyse ?x ?y)
 
     ;; Long arithmetic
     [["Form" ["Cons" [["Ident" "jvm-ladd"] ["Cons" [?y ["Cons" [?x ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-ladd analyse-ast ?x ?y)
+    (&&host/analyse-jvm-ladd analyse ?x ?y)
 
     [["Form" ["Cons" [["Ident" "jvm-lsub"] ["Cons" [?y ["Cons" [?x ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-lsub analyse-ast ?x ?y)
+    (&&host/analyse-jvm-lsub analyse ?x ?y)
 
     [["Form" ["Cons" [["Ident" "jvm-lmul"] ["Cons" [?y ["Cons" [?x ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-lmul analyse-ast ?x ?y)
+    (&&host/analyse-jvm-lmul analyse ?x ?y)
 
     [["Form" ["Cons" [["Ident" "jvm-ldiv"] ["Cons" [?y ["Cons" [?x ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-ldiv analyse-ast ?x ?y)
+    (&&host/analyse-jvm-ldiv analyse ?x ?y)
 
     [["Form" ["Cons" [["Ident" "jvm-lrem"] ["Cons" [?y ["Cons" [?x ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-lrem analyse-ast ?x ?y)
+    (&&host/analyse-jvm-lrem analyse ?x ?y)
 
     [["Form" ["Cons" [["Ident" "jvm-leq"] ["Cons" [?y ["Cons" [?x ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-leq analyse-ast ?x ?y)
+    (&&host/analyse-jvm-leq analyse ?x ?y)
 
     [["Form" ["Cons" [["Ident" "jvm-llt"] ["Cons" [?y ["Cons" [?x ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-llt analyse-ast ?x ?y)
+    (&&host/analyse-jvm-llt analyse ?x ?y)
 
     [["Form" ["Cons" [["Ident" "jvm-lgt"] ["Cons" [?y ["Cons" [?x ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-lgt analyse-ast ?x ?y)
+    (&&host/analyse-jvm-lgt analyse ?x ?y)
 
     ;; Float arithmetic
     [["Form" ["Cons" [["Ident" "jvm-fadd"] ["Cons" [?y ["Cons" [?x ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-fadd analyse-ast ?x ?y)
+    (&&host/analyse-jvm-fadd analyse ?x ?y)
 
     [["Form" ["Cons" [["Ident" "jvm-fsub"] ["Cons" [?y ["Cons" [?x ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-fsub analyse-ast ?x ?y)
+    (&&host/analyse-jvm-fsub analyse ?x ?y)
 
     [["Form" ["Cons" [["Ident" "jvm-fmul"] ["Cons" [?y ["Cons" [?x ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-fmul analyse-ast ?x ?y)
+    (&&host/analyse-jvm-fmul analyse ?x ?y)
 
     [["Form" ["Cons" [["Ident" "jvm-fdiv"] ["Cons" [?y ["Cons" [?x ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-fdiv analyse-ast ?x ?y)
+    (&&host/analyse-jvm-fdiv analyse ?x ?y)
 
     [["Form" ["Cons" [["Ident" "jvm-frem"] ["Cons" [?y ["Cons" [?x ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-frem analyse-ast ?x ?y)
+    (&&host/analyse-jvm-frem analyse ?x ?y)
 
     [["Form" ["Cons" [["Ident" "jvm-feq"] ["Cons" [?y ["Cons" [?x ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-feq analyse-ast ?x ?y)
+    (&&host/analyse-jvm-feq analyse ?x ?y)
 
     [["Form" ["Cons" [["Ident" "jvm-flt"] ["Cons" [?y ["Cons" [?x ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-flt analyse-ast ?x ?y)
+    (&&host/analyse-jvm-flt analyse ?x ?y)
 
     [["Form" ["Cons" [["Ident" "jvm-fgt"] ["Cons" [?y ["Cons" [?x ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-fgt analyse-ast ?x ?y)
+    (&&host/analyse-jvm-fgt analyse ?x ?y)
 
     ;; Double arithmetic
     [["Form" ["Cons" [["Ident" "jvm-dadd"] ["Cons" [?y ["Cons" [?x ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-dadd analyse-ast ?x ?y)
+    (&&host/analyse-jvm-dadd analyse ?x ?y)
 
     [["Form" ["Cons" [["Ident" "jvm-dsub"] ["Cons" [?y ["Cons" [?x ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-dsub analyse-ast ?x ?y)
+    (&&host/analyse-jvm-dsub analyse ?x ?y)
 
     [["Form" ["Cons" [["Ident" "jvm-dmul"] ["Cons" [?y ["Cons" [?x ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-dmul analyse-ast ?x ?y)
+    (&&host/analyse-jvm-dmul analyse ?x ?y)
 
     [["Form" ["Cons" [["Ident" "jvm-ddiv"] ["Cons" [?y ["Cons" [?x ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-ddiv analyse-ast ?x ?y)
+    (&&host/analyse-jvm-ddiv analyse ?x ?y)
 
     [["Form" ["Cons" [["Ident" "jvm-drem"] ["Cons" [?y ["Cons" [?x ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-drem analyse-ast ?x ?y)
+    (&&host/analyse-jvm-drem analyse ?x ?y)
 
     [["Form" ["Cons" [["Ident" "jvm-deq"] ["Cons" [?y ["Cons" [?x ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-deq analyse-ast ?x ?y)
+    (&&host/analyse-jvm-deq analyse ?x ?y)
 
     [["Form" ["Cons" [["Ident" "jvm-dlt"] ["Cons" [?y ["Cons" [?x ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-dlt analyse-ast ?x ?y)
+    (&&host/analyse-jvm-dlt analyse ?x ?y)
 
     [["Form" ["Cons" [["Ident" "jvm-dgt"] ["Cons" [?y ["Cons" [?x ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-dgt analyse-ast ?x ?y)
+    (&&host/analyse-jvm-dgt analyse ?x ?y)
 
     ;; Objects
     [["Form" ["Cons" [["Ident" "jvm-null?"] ["Cons" [?object ["Nil" _]]]]]]]
-    (&&host/analyse-jvm-null? analyse-ast ?object)
+    (&&host/analyse-jvm-null? analyse ?object)
     
     [["Form" ["Cons" [["Ident" "jvm-new"]
                       ["Cons" [["Ident" ?class]
                                ["Cons" [["Tuple" ?classes]
                                         ["Cons" [["Tuple" ?args]
                                                  ["Nil" _]]]]]]]]]]]
-    (&&host/analyse-jvm-new analyse-ast ?class ?classes ?args)
+    (&&host/analyse-jvm-new analyse ?class ?classes ?args)
 
     [["Form" ["Cons" [["Ident" "jvm-getstatic"]
                       ["Cons" [["Ident" ?class]
                                ["Cons" [["Text" ?field]
                                         ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-getstatic analyse-ast ?class ?field)
+    (&&host/analyse-jvm-getstatic analyse ?class ?field)
 
     [["Form" ["Cons" [["Ident" "jvm-getfield"]
                       ["Cons" [["Ident" ?class]
                                ["Cons" [["Text" ?field]
                                         ["Cons" [?object
                                                  ["Nil" _]]]]]]]]]]]
-    (&&host/analyse-jvm-getfield analyse-ast ?class ?field ?object)
+    (&&host/analyse-jvm-getfield analyse ?class ?field ?object)
 
     [["Form" ["Cons" [["Ident" "jvm-putstatic"]
                       ["Cons" [["Ident" ?class]
                                ["Cons" [["Text" ?field]
                                         ["Cons" [?value
                                                  ["Nil" _]]]]]]]]]]]
-    (&&host/analyse-jvm-putstatic analyse-ast ?class ?field ?value)
+    (&&host/analyse-jvm-putstatic analyse ?class ?field ?value)
 
     [["Form" ["Cons" [["Ident" "jvm-putfield"]
                       ["Cons" [["Ident" ?class]
@@ -231,7 +238,7 @@
                                         ["Cons" [?object
                                                  ["Cons" [?value
                                                           ["Nil" _]]]]]]]]]]]]]
-    (&&host/analyse-jvm-putfield analyse-ast ?class ?field ?object ?value)
+    (&&host/analyse-jvm-putfield analyse ?class ?field ?object ?value)
 
     [["Form" ["Cons" [["Ident" "jvm-invokestatic"]
                       ["Cons" [["Ident" ?class]
@@ -239,7 +246,7 @@
                                         ["Cons" [["Tuple" ?classes]
                                                  ["Cons" [["Tuple" ?args]
                                                           ["Nil" _]]]]]]]]]]]]]
-    (&&host/analyse-jvm-invokestatic analyse-ast ?class ?method (&/->seq ?classes) (&/->seq ?args))
+    (&&host/analyse-jvm-invokestatic analyse ?class ?method (&/->seq ?classes) (&/->seq ?args))
 
     [["Form" ["Cons" [["Ident" "jvm-invokevirtual"]
                       ["Cons" [["Ident" ?class]
@@ -248,7 +255,7 @@
                                                  ["Cons" [?object
                                                           ["Cons" [["Tuple" ?args]
                                                                    ["Nil" _]]]]]]]]]]]]]]]
-    (&&host/analyse-jvm-invokevirtual analyse-ast ?class ?method (&/->seq ?classes) ?object (&/->seq ?args))
+    (&&host/analyse-jvm-invokevirtual analyse ?class ?method (&/->seq ?classes) ?object (&/->seq ?args))
 
     [["Form" ["Cons" [["Ident" "jvm-invokeinterface"]
                       ["Cons" [["Ident" ?class]
@@ -257,7 +264,7 @@
                                                  ["Cons" [?object
                                                           ["Cons" [["Tuple" ?args]
                                                                    ["Nil" _]]]]]]]]]]]]]]]
-    (&&host/analyse-jvm-invokeinterface analyse-ast ?class ?method (&/->seq ?classes) ?object (&/->seq ?args))
+    (&&host/analyse-jvm-invokeinterface analyse ?class ?method (&/->seq ?classes) ?object (&/->seq ?args))
 
     [["Form" ["Cons" [["Ident" "jvm-invokespecial"]
                       ["Cons" [["Ident" ?class]
@@ -266,152 +273,153 @@
                                                  ["Cons" [?object
                                                           ["Cons" [["Tuple" ?args]
                                                                    ["Nil" _]]]]]]]]]]]]]]]
-    (&&host/analyse-jvm-invokespecial analyse-ast ?class ?method (&/->seq ?classes) ?object (&/->seq ?args))
+    (&&host/analyse-jvm-invokespecial analyse ?class ?method (&/->seq ?classes) ?object (&/->seq ?args))
     
     ;; Exceptions
     [["Form" ["Cons" [["Ident" "jvm-try"]
                       ["Cons" [?body
                                ?handlers]]]]]]
-    (&&host/analyse-jvm-try analyse-ast ?body (reduce parse-handler [(list) nil] (&/->seq ?handlers)))
+    (&&host/analyse-jvm-try analyse ?body (reduce parse-handler [(list) nil] (&/->seq ?handlers)))
 
     [["Form" ["Cons" [["Ident" "jvm-throw"]
                       ["Cons" [?ex
                                ["Nil" _]]]]]]]
-    (&&host/analyse-jvm-throw analyse-ast ?ex)
+    (&&host/analyse-jvm-throw analyse ?ex)
 
     ;; Syncronization/monitos
     [["Form" ["Cons" [["Ident" "jvm-monitorenter"]
                       ["Cons" [?monitor
                                ["Nil" _]]]]]]]
-    (&&host/analyse-jvm-monitorenter analyse-ast ?monitor)
+    (&&host/analyse-jvm-monitorenter analyse ?monitor)
 
     [["Form" ["Cons" [["Ident" "jvm-monitorexit"]
                       ["Cons" [?monitor
                                ["Nil" _]]]]]]]
-    (&&host/analyse-jvm-monitorexit analyse-ast ?monitor)
+    (&&host/analyse-jvm-monitorexit analyse ?monitor)
 
     ;; Primitive conversions
     [["Form" ["Cons" [["Ident" "jvm-d2f"] ["Cons" [?value ["Nil" _]]]]]]]
-    (&&host/analyse-jvm-d2f analyse-ast ?value)
+    (&&host/analyse-jvm-d2f analyse ?value)
 
     [["Form" ["Cons" [["Ident" "jvm-d2i"] ["Cons" [?value ["Nil" _]]]]]]]
-    (&&host/analyse-jvm-d2i analyse-ast ?value)
+    (&&host/analyse-jvm-d2i analyse ?value)
 
     [["Form" ["Cons" [["Ident" "jvm-d2l"] ["Cons" [?value ["Nil" _]]]]]]]
-    (&&host/analyse-jvm-d2l analyse-ast ?value)
+    (&&host/analyse-jvm-d2l analyse ?value)
 
     [["Form" ["Cons" [["Ident" "jvm-f2d"] ["Cons" [?value ["Nil" _]]]]]]]
-    (&&host/analyse-jvm-f2d analyse-ast ?value)
+    (&&host/analyse-jvm-f2d analyse ?value)
 
     [["Form" ["Cons" [["Ident" "jvm-f2i"] ["Cons" [?value ["Nil" _]]]]]]]
-    (&&host/analyse-jvm-f2i analyse-ast ?value)
+    (&&host/analyse-jvm-f2i analyse ?value)
 
     [["Form" ["Cons" [["Ident" "jvm-f2l"] ["Cons" [?value ["Nil" _]]]]]]]
-    (&&host/analyse-jvm-f2l analyse-ast ?value)
+    (&&host/analyse-jvm-f2l analyse ?value)
 
     [["Form" ["Cons" [["Ident" "jvm-i2b"] ["Cons" [?value ["Nil" _]]]]]]]
-    (&&host/analyse-jvm-i2b analyse-ast ?value)
+    (&&host/analyse-jvm-i2b analyse ?value)
 
     [["Form" ["Cons" [["Ident" "jvm-i2c"] ["Cons" [?value ["Nil" _]]]]]]]
-    (&&host/analyse-jvm-i2c analyse-ast ?value)
+    (&&host/analyse-jvm-i2c analyse ?value)
 
     [["Form" ["Cons" [["Ident" "jvm-i2d"] ["Cons" [?value ["Nil" _]]]]]]]
-    (&&host/analyse-jvm-i2d analyse-ast ?value)
+    (&&host/analyse-jvm-i2d analyse ?value)
 
     [["Form" ["Cons" [["Ident" "jvm-i2f"] ["Cons" [?value ["Nil" _]]]]]]]
-    (&&host/analyse-jvm-i2f analyse-ast ?value)
+    (&&host/analyse-jvm-i2f analyse ?value)
 
     [["Form" ["Cons" [["Ident" "jvm-i2l"] ["Cons" [?value ["Nil" _]]]]]]]
-    (&&host/analyse-jvm-i2l analyse-ast ?value)
+    (&&host/analyse-jvm-i2l analyse ?value)
 
     [["Form" ["Cons" [["Ident" "jvm-i2s"] ["Cons" [?value ["Nil" _]]]]]]]
-    (&&host/analyse-jvm-i2s analyse-ast ?value)
+    (&&host/analyse-jvm-i2s analyse ?value)
 
     [["Form" ["Cons" [["Ident" "jvm-l2d"] ["Cons" [?value ["Nil" _]]]]]]]
-    (&&host/analyse-jvm-l2d analyse-ast ?value)
+    (&&host/analyse-jvm-l2d analyse ?value)
 
     [["Form" ["Cons" [["Ident" "jvm-l2f"] ["Cons" [?value ["Nil" _]]]]]]]
-    (&&host/analyse-jvm-l2f analyse-ast ?value)
+    (&&host/analyse-jvm-l2f analyse ?value)
 
     [["Form" ["Cons" [["Ident" "jvm-l2i"] ["Cons" [?value ["Nil" _]]]]]]]
-    (&&host/analyse-jvm-l2i analyse-ast ?value)
+    (&&host/analyse-jvm-l2i analyse ?value)
 
     ;; Bitwise operators
     [["Form" ["Cons" [["Ident" "jvm-iand"] ["Cons" [?x ["Cons" [?y ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-iand analyse-ast ?x ?y)
+    (&&host/analyse-jvm-iand analyse ?x ?y)
 
     [["Form" ["Cons" [["Ident" "jvm-ior"] ["Cons" [?x ["Cons" [?y ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-ior analyse-ast ?x ?y)
+    (&&host/analyse-jvm-ior analyse ?x ?y)
 
     [["Form" ["Cons" [["Ident" "jvm-land"] ["Cons" [?x ["Cons" [?y ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-land analyse-ast ?x ?y)
+    (&&host/analyse-jvm-land analyse ?x ?y)
 
     [["Form" ["Cons" [["Ident" "jvm-lor"] ["Cons" [?x ["Cons" [?y ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-lor analyse-ast ?x ?y)
+    (&&host/analyse-jvm-lor analyse ?x ?y)
 
     [["Form" ["Cons" [["Ident" "jvm-lxor"] ["Cons" [?x ["Cons" [?y ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-lxor analyse-ast ?x ?y)
+    (&&host/analyse-jvm-lxor analyse ?x ?y)
 
     [["Form" ["Cons" [["Ident" "jvm-lshl"] ["Cons" [?x ["Cons" [?y ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-lshl analyse-ast ?x ?y)
+    (&&host/analyse-jvm-lshl analyse ?x ?y)
 
     [["Form" ["Cons" [["Ident" "jvm-lshr"] ["Cons" [?x ["Cons" [?y ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-lshr analyse-ast ?x ?y)
+    (&&host/analyse-jvm-lshr analyse ?x ?y)
 
     [["Form" ["Cons" [["Ident" "jvm-lushr"] ["Cons" [?x ["Cons" [?y ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-lushr analyse-ast ?x ?y)
+    (&&host/analyse-jvm-lushr analyse ?x ?y)
     
     ;; Arrays
     [["Form" ["Cons" [["Ident" "jvm-new-array"] ["Cons" [["Ident" ?class] ["Cons" [["Int" ?length] ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-new-array analyse-ast ?class ?length)
+    (&&host/analyse-jvm-new-array analyse ?class ?length)
 
     [["Form" ["Cons" [["Ident" "jvm-aastore"] ["Cons" [?array ["Cons" [["Int" ?idx] ["Cons" [?elem ["Nil" _]]]]]]]]]]]
-    (&&host/analyse-jvm-aastore analyse-ast ?array ?idx ?elem)
+    (&&host/analyse-jvm-aastore analyse ?array ?idx ?elem)
 
     [["Form" ["Cons" [["Ident" "jvm-aaload"] ["Cons" [?array ["Cons" [["Int" ?idx] ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-aaload analyse-ast ?array ?idx)
+    (&&host/analyse-jvm-aaload analyse ?array ?idx)
 
     ;; Classes & interfaces
     [["Form" ["Cons" [["Ident" "jvm-class"] ["Cons" [["Ident" ?name] ["Cons" [["Ident" ?super-class] ["Cons" [["Tuple" ?fields] ["Nil" _]]]]]]]]]]]
-    (&&host/analyse-jvm-class analyse-ast ?name ?super-class (&/->seq ?fields))
+    (&&host/analyse-jvm-class analyse ?name ?super-class (&/->seq ?fields))
 
     [["Form" ["Cons" [["Ident" "jvm-interface"] ["Cons" [["Ident" ?name] ?members]]]]]]
-    (&&host/analyse-jvm-interface analyse-ast ?name ?members)
+    (&&host/analyse-jvm-interface analyse ?name ?members)
 
     ;; Programs
     [["Form" ["Cons" [["Ident" "jvm-program"] ["Cons" [["Ident" ?args] ["Cons" [?body ["Nil" _]]]]]]]]]
-    (&&host/analyse-jvm-program analyse-ast ?args ?body)
+    (&&host/analyse-jvm-program analyse ?args ?body)
     
     [_]
     (fail (str "[Analyser Error] Unmatched token: " (&/show-ast token)))))
 
-(defn ^:private analyse-ast [token]
-  ;; (prn 'analyse-ast token)
-  (matchv ::M/objects [token]
-    [["Form" ["Cons" [["Tag" ?tag] ?values]]]]
-    (exec [;; :let [_ (prn 'PRE-ASSERT)]
-           :let [?values (&/->seq ?values)]
-           :let [_ (assert (= 1 (count ?values)) (str "[Analyser Error] Can only tag 1 value: " (pr-str token)))]
-           ;; :let [_ (prn 'POST-ASSERT)]
-           =value (&&/analyse-1 analyse-ast (first ?values))
-           =value-type (&&/expr-type =value)]
-      (return (list [::&&/Expression [::&&/variant ?tag =value] [::&type/Variant (list [?tag =value-type])]])))
-    
-    [["Form" ["Cons" [?fn ?args]]]]
-    (fn [state]
-      (match ((&&/analyse-1 analyse-ast ?fn) state)
-        [::&/ok [state* =fn]]
-        ((&&lux/analyse-call analyse-ast =fn ?args) state*)
-
-        _
-        ((analyse-basic-ast analyse-ast token) state)))
-    
-    [_]
-    (analyse-basic-ast analyse-ast token)))
+(defn ^:private analyse-ast [eval!]
+  (fn [token]
+    ;; (prn 'analyse-ast token)
+    (matchv ::M/objects [token]
+      [["Form" ["Cons" [["Tag" ?tag] ?values]]]]
+      (exec [;; :let [_ (prn 'PRE-ASSERT)]
+             :let [?values (&/->seq ?values)]
+             :let [_ (assert (= 1 (count ?values)) (str "[Analyser Error] Can only tag 1 value: " (pr-str token)))]
+             ;; :let [_ (prn 'POST-ASSERT)]
+             =value (&&/analyse-1 (analyse-ast eval!) (first ?values))
+             =value-type (&&/expr-type =value)]
+        (return (|list [::&&/Expression [::&&/variant ?tag =value] (&/V "Variant" (&/V "Cons" (to-array [(to-array [?tag =value-type]) (&/V "Nil" nil)])))])))
+      
+      [["Form" ["Cons" [?fn ?args]]]]
+      (fn [state]
+        (match ((&&/analyse-1 (analyse-ast eval!) ?fn) state)
+          [::&/ok [state* =fn]]
+          ((&&lux/analyse-apply (analyse-ast eval!) =fn ?args) state*)
+
+          _
+          ((analyse-basic-ast (analyse-ast eval!) eval! token) state)))
+      
+      [_]
+      (analyse-basic-ast (analyse-ast eval!) eval! token))))
 
 ;; [Resources]
-(def analyse
+(defn analyse [eval!]
   (exec [asts &parser/parse
          ;; :let [_ (prn 'analyse/asts asts)]
          ]
-    (mapcat-m analyse-ast asts)))
+    (|flat-map% (analyse-ast eval!) asts)))
diff --git a/src/lux/analyser/base.clj b/src/lux/analyser/base.clj
index 66451e97b..43bcd1181 100644
--- a/src/lux/analyser/base.clj
+++ b/src/lux/analyser/base.clj
@@ -1,8 +1,10 @@
 (ns lux.analyser.base
-  (:require [clojure.core.match :refer [match]]
+  (:require [clojure.core.match :as M :refer [match matchv]]
+            clojure.core.match.array
             (lux [base :as & :refer [exec return fail
                                      try-all-m map-m mapcat-m reduce-m
-                                     assert!]])))
+                                     assert!]]
+                 [type :as &type])))
 
 ;; [Resources]
 (defn expr-type [syntax+]
@@ -31,3 +33,11 @@
 
       :else
       (fail "[Analyser Error] Can't expand to other than 2 elements."))))
+
+(defn with-var [k]
+  (exec [=var &type/fresh-var
+         =ret (k =var)]
+    (match =ret
+      [::Expression ?expr ?type]
+      (exec [=type (&type/clean =var ?type)]
+        (return [::Expression ?expr =type])))))
diff --git a/src/lux/analyser/case.clj b/src/lux/analyser/case.clj
index 0980b2865..9ae2f736b 100644
--- a/src/lux/analyser/case.clj
+++ b/src/lux/analyser/case.clj
@@ -27,9 +27,11 @@
 (defn analyse-branch [analyse max-registers [bindings body]]
   ;; (prn 'analyse-branch max-registers bindings body)
   (reduce (fn [body* name]
-            (&env/with-local name &type/+dont-care-type+ body*))
+            (&&/with-var
+              (fn [=var]
+                (&env/with-local name =var body*))))
           (reduce (fn [body* _]
-                    (&env/with-local "" &type/+dont-care-type+ body*))
+                    (&env/with-local "" &type/+dont-care+ body*))
                   (&&/analyse-1 analyse body)
                   (range (- max-registers (count bindings))))
           (reverse bindings)))
diff --git a/src/lux/analyser/host.clj b/src/lux/analyser/host.clj
index 59022a0e0..3d94aac59 100644
--- a/src/lux/analyser/host.clj
+++ b/src/lux/analyser/host.clj
@@ -3,7 +3,8 @@
             [clojure.core.match :as M :refer [match matchv]]
             clojure.core.match.array
             (lux [base :as & :refer [exec return fail
-                                     try-all-m map-m mapcat-m reduce-m
+                                     |list
+                                     try-all-m map-m reduce-m
                                      assert!]]
                  [parser :as &parser]
                  [type :as &type]
@@ -29,68 +30,52 @@
     (fail "[Analyser Error] Can't extract Ident.")))
 
 ;; [Resources]
-(do-template [<name> <output-tag> <wrapper-class>]
-  (let [elem-type [::&type/Data <wrapper-class>]]
-    (defn <name> [analyse ?x ?y]
-      (exec [[=x =y] (&&/analyse-2 analyse ?x ?y)
-             ;; =x-type (&&/expr-type =x)
-             ;; =y-type (&&/expr-type =y)
-             ;; _ (&type/solve elem-type =x-type)
-             ;; _ (&type/solve elem-type =y-type)
-             ]
-        (return (list [::&&/Expression [<output-tag> =x =y] elem-type])))))
-
-  analyse-jvm-iadd ::&&/jvm-iadd "java.lang.Integer"
-  analyse-jvm-isub ::&&/jvm-isub "java.lang.Integer"
-  analyse-jvm-imul ::&&/jvm-imul "java.lang.Integer"
-  analyse-jvm-idiv ::&&/jvm-idiv "java.lang.Integer"
-  analyse-jvm-irem ::&&/jvm-irem "java.lang.Integer"
-
-  analyse-jvm-ladd ::&&/jvm-ladd "java.lang.Long"
-  analyse-jvm-lsub ::&&/jvm-lsub "java.lang.Long"
-  analyse-jvm-lmul ::&&/jvm-lmul "java.lang.Long"
-  analyse-jvm-ldiv ::&&/jvm-ldiv "java.lang.Long"
-  analyse-jvm-lrem ::&&/jvm-lrem "java.lang.Long"
-
-  analyse-jvm-fadd ::&&/jvm-fadd "java.lang.Float"
-  analyse-jvm-fsub ::&&/jvm-fsub "java.lang.Float"
-  analyse-jvm-fmul ::&&/jvm-fmul "java.lang.Float"
-  analyse-jvm-fdiv ::&&/jvm-fdiv "java.lang.Float"
-  analyse-jvm-frem ::&&/jvm-frem "java.lang.Float"
-
-  analyse-jvm-dadd ::&&/jvm-dadd "java.lang.Double"
-  analyse-jvm-dsub ::&&/jvm-dsub "java.lang.Double"
-  analyse-jvm-dmul ::&&/jvm-dmul "java.lang.Double"
-  analyse-jvm-ddiv ::&&/jvm-ddiv "java.lang.Double"
-  analyse-jvm-drem ::&&/jvm-drem "java.lang.Double"
-  )
-
 (do-template [<name> <output-tag> <input-class> <output-class>]
-  (let [elem-type [::&type/Data <output-class>]]
+  (let [input-type (&/V "Data" (to-array [<input-class> (&/V "Nil" nil)]))
+        output-type (&/V "Data" (to-array [<output-class> (&/V "Nil" nil)]))]
     (defn <name> [analyse ?x ?y]
       (exec [[=x =y] (&&/analyse-2 analyse ?x ?y)
-             ;; =x-type (&&/expr-type =x)
-             ;; =y-type (&&/expr-type =y)
-             ;; _ (&type/solve elem-type =x-type)
-             ;; _ (&type/solve elem-type =y-type)
-             ]
-        (return (list [::&&/Expression [<output-tag> =x =y] elem-type])))))
-
-  analyse-jvm-ieq ::&&/jvm-ieq "java.lang.Integer" "java.lang.Boolean"
-  analyse-jvm-ilt ::&&/jvm-ilt "java.lang.Integer" "java.lang.Boolean"
-  analyse-jvm-igt ::&&/jvm-igt "java.lang.Integer" "java.lang.Boolean"
-
-  analyse-jvm-leq ::&&/jvm-leq "java.lang.Long"    "java.lang.Boolean"
-  analyse-jvm-llt ::&&/jvm-llt "java.lang.Long"    "java.lang.Boolean"
-  analyse-jvm-lgt ::&&/jvm-lgt "java.lang.Long"    "java.lang.Boolean"
-
-  analyse-jvm-feq ::&&/jvm-feq "java.lang.Float"   "java.lang.Boolean"
-  analyse-jvm-flt ::&&/jvm-flt "java.lang.Float"   "java.lang.Boolean"
-  analyse-jvm-fgt ::&&/jvm-fgt "java.lang.Float"   "java.lang.Boolean"
-
-  analyse-jvm-deq ::&&/jvm-deq "java.lang.Double"  "java.lang.Boolean"
-  analyse-jvm-dlt ::&&/jvm-dlt "java.lang.Double"  "java.lang.Boolean"
-  analyse-jvm-dgt ::&&/jvm-dgt "java.lang.Double"  "java.lang.Boolean"
+             =x-type (&&/expr-type =x)
+             =y-type (&&/expr-type =y)
+             _ (&type/solve input-type =x-type)
+             _ (&type/solve input-type =y-type)]
+        (return (|list [::&&/Expression [<output-tag> =x =y] output-type])))))
+
+  analyse-jvm-iadd ::&&/jvm-iadd "java.lang.Integer" "java.lang.Integer"
+  analyse-jvm-isub ::&&/jvm-isub "java.lang.Integer" "java.lang.Integer"
+  analyse-jvm-imul ::&&/jvm-imul "java.lang.Integer" "java.lang.Integer"
+  analyse-jvm-idiv ::&&/jvm-idiv "java.lang.Integer" "java.lang.Integer"
+  analyse-jvm-irem ::&&/jvm-irem "java.lang.Integer" "java.lang.Integer"
+  analyse-jvm-ieq  ::&&/jvm-ieq  "java.lang.Integer" "java.lang.Boolean"
+  analyse-jvm-ilt  ::&&/jvm-ilt  "java.lang.Integer" "java.lang.Boolean"
+  analyse-jvm-igt  ::&&/jvm-igt  "java.lang.Integer" "java.lang.Boolean"
+
+  analyse-jvm-ladd ::&&/jvm-ladd "java.lang.Long"    "java.lang.Long"
+  analyse-jvm-lsub ::&&/jvm-lsub "java.lang.Long"    "java.lang.Long"
+  analyse-jvm-lmul ::&&/jvm-lmul "java.lang.Long"    "java.lang.Long"
+  analyse-jvm-ldiv ::&&/jvm-ldiv "java.lang.Long"    "java.lang.Long"
+  analyse-jvm-lrem ::&&/jvm-lrem "java.lang.Long"    "java.lang.Long"
+  analyse-jvm-leq  ::&&/jvm-leq  "java.lang.Long"    "java.lang.Boolean"
+  analyse-jvm-llt  ::&&/jvm-llt  "java.lang.Long"    "java.lang.Boolean"
+  analyse-jvm-lgt  ::&&/jvm-lgt  "java.lang.Long"    "java.lang.Boolean"
+
+  analyse-jvm-fadd ::&&/jvm-fadd "java.lang.Float"   "java.lang.Float"
+  analyse-jvm-fsub ::&&/jvm-fsub "java.lang.Float"   "java.lang.Float"
+  analyse-jvm-fmul ::&&/jvm-fmul "java.lang.Float"   "java.lang.Float"
+  analyse-jvm-fdiv ::&&/jvm-fdiv "java.lang.Float"   "java.lang.Float"
+  analyse-jvm-frem ::&&/jvm-frem "java.lang.Float"   "java.lang.Float"
+  analyse-jvm-feq  ::&&/jvm-feq  "java.lang.Float"   "java.lang.Boolean"
+  analyse-jvm-flt  ::&&/jvm-flt  "java.lang.Float"   "java.lang.Boolean"
+  analyse-jvm-fgt  ::&&/jvm-fgt  "java.lang.Float"   "java.lang.Boolean"
+
+  analyse-jvm-dadd ::&&/jvm-dadd "java.lang.Double"  "java.lang.Double"
+  analyse-jvm-dsub ::&&/jvm-dsub "java.lang.Double"  "java.lang.Double"
+  analyse-jvm-dmul ::&&/jvm-dmul "java.lang.Double"  "java.lang.Double"
+  analyse-jvm-ddiv ::&&/jvm-ddiv "java.lang.Double"  "java.lang.Double"
+  analyse-jvm-drem ::&&/jvm-drem "java.lang.Double"  "java.lang.Double"
+  analyse-jvm-deq  ::&&/jvm-deq  "java.lang.Double"  "java.lang.Boolean"
+  analyse-jvm-dlt  ::&&/jvm-dlt  "java.lang.Double"  "java.lang.Boolean"
+  analyse-jvm-dgt  ::&&/jvm-dgt  "java.lang.Double"  "java.lang.Boolean"
   )
 
 (defn analyse-jvm-getstatic [analyse ?class ?field]
@@ -99,13 +84,13 @@
          =type (&host/lookup-static-field =class ?field)
          ;; :let [_ (prn 'analyse-jvm-getstatic/=type =type)]
          ]
-    (return (list [::&&/Expression [::&&/jvm-getstatic =class ?field] =type]))))
+    (return (|list [::&&/Expression [::&&/jvm-getstatic =class ?field] =type]))))
 
 (defn analyse-jvm-getfield [analyse ?class ?field ?object]
   (exec [=class (&host/full-class-name ?class)
          =type (&host/lookup-static-field =class ?field)
          =object (&&/analyse-1 analyse ?object)]
-    (return (list [::&&/Expression [::&&/jvm-getfield =class ?field =object] =type]))))
+    (return (|list [::&&/Expression [::&&/jvm-getfield =class ?field =object] =type]))))
 
 (defn analyse-jvm-putstatic [analyse ?class ?field ?value]
   (exec [=class (&host/full-class-name ?class)
@@ -113,21 +98,21 @@
          =type (&host/lookup-static-field =class ?field)
          ;; :let [_ (prn 'analyse-jvm-getstatic/=type =type)]
          =value (&&/analyse-1 analyse ?value)]
-    (return (list [::&&/Expression [::&&/jvm-putstatic =class ?field =value] =type]))))
+    (return (|list [::&&/Expression [::&&/jvm-putstatic =class ?field =value] =type]))))
 
 (defn analyse-jvm-putfield [analyse ?class ?field ?object ?value]
   (exec [=class (&host/full-class-name ?class)
          =type (&host/lookup-static-field =class ?field)
          =object (&&/analyse-1 analyse ?object)
          =value (&&/analyse-1 analyse ?value)]
-    (return (list [::&&/Expression [::&&/jvm-putfield =class ?field =object =value] =type]))))
+    (return (|list [::&&/Expression [::&&/jvm-putfield =class ?field =object =value] =type]))))
 
 (defn analyse-jvm-invokestatic [analyse ?class ?method ?classes ?args]
   (exec [=class (&host/full-class-name ?class)
          =classes (map-m &host/extract-jvm-param ?classes)
          =return (&host/lookup-virtual-method =class ?method =classes)
          =args (mapcat-m analyse ?args)]
-    (return (list [::&&/Expression [::&&/jvm-invokestatic =class ?method =classes =args] =return]))))
+    (return (|list [::&&/Expression [::&&/jvm-invokestatic =class ?method =classes =args] =return]))))
 
 (do-template [<name> <tag>]
   (defn <name> [analyse ?class ?method ?classes ?object ?args]
@@ -142,7 +127,7 @@
            =args (mapcat-m analyse ?args)
            ;; :let [_ (prn 'analyse-jvm-invokevirtual/=args =args)]
            ]
-      (return (list [::&&/Expression [<tag> =class ?method =classes =object =args] =return]))))
+      (return (|list [::&&/Expression [<tag> =class ?method =classes =object =args] =return]))))
 
   analyse-jvm-invokevirtual   ::&&/jvm-invokevirtual
   analyse-jvm-invokeinterface ::&&/jvm-invokeinterface
@@ -151,27 +136,28 @@
 
 (defn analyse-jvm-null? [analyse ?object]
   (exec [=object (&&/analyse-1 analyse ?object)]
-    (return (list [::&&/Expression [::&&/jvm-null? =object] [::&type/Data "java.lang.Boolean"]]))))
+    (return (|list [::&&/Expression [::&&/jvm-null? =object] (&/V "Data" (to-array ["java.lang.Boolean" (&/V "Nil" nil)]))]))))
 
 (defn analyse-jvm-new [analyse ?class ?classes ?args]
   (exec [=class (&host/full-class-name ?class)
          =classes (map-m &host/extract-jvm-param ?classes)
          =args (mapcat-m analyse ?args)]
-    (return (list [::&&/Expression [::&&/jvm-new =class =classes =args] [::&type/Data =class]]))))
+    (return (|list [::&&/Expression [::&&/jvm-new =class =classes =args] (&/V "Data" (to-array [=class (&/V "Nil" nil)]))]))))
 
 (defn analyse-jvm-new-array [analyse ?class ?length]
   (exec [=class (&host/full-class-name ?class)]
-    (return (list [::&&/Expression [::&&/jvm-new-array =class ?length] [::&type/Array [::&type/Data =class]]]))))
+    (return (|list [::&&/Expression [::&&/jvm-new-array =class ?length] (&/V "array" (to-array [(&/V "Data" (to-array [=class (&/V "Nil" nil)]))
+                                                                                                (&/V "Nil" nil)]))]))))
 
 (defn analyse-jvm-aastore [analyse ?array ?idx ?elem]
   (exec [[=array =elem] (&&/analyse-2 analyse ?array ?elem)
          =array-type (&&/expr-type =array)]
-    (return (list [::&&/Expression [::&&/jvm-aastore =array ?idx =elem] =array-type]))))
+    (return (|list [::&&/Expression [::&&/jvm-aastore =array ?idx =elem] =array-type]))))
 
 (defn analyse-jvm-aaload [analyse ?array ?idx]
   (exec [=array (&&/analyse-1 analyse ?array)
          =array-type (&&/expr-type =array)]
-    (return (list [::&&/Expression [::&&/jvm-aaload =array ?idx] =array-type]))))
+    (return (|list [::&&/Expression [::&&/jvm-aaload =array ?idx] =array-type]))))
 
 (defn analyse-jvm-class [analyse ?name ?super-class ?fields]
   (exec [?fields (map-m (fn [?field]
@@ -186,7 +172,7 @@
                                   [field {:access :public
                                           :type class}]))]
          $module &/get-module-name]
-    (return (list [::&&/Statement [::&&/jvm-class $module ?name ?super-class =fields {}]]))))
+    (return (|list [::&&/Statement [::&&/jvm-class $module ?name ?super-class =fields {}]]))))
 
 (defn analyse-jvm-interface [analyse ?name ?members]
   ;; (prn 'analyse-jvm-interface ?name ?members)
@@ -211,41 +197,41 @@
                                    [method {:access :public
                                             :type [inputs output]}]))]
          $module &/get-module-name]
-    (return (list [::&&/Statement [::&&/jvm-interface $module ?name =methods]]))))
+    (return (|list [::&&/Statement [::&&/jvm-interface $module ?name =methods]]))))
 
 (defn analyse-exec [analyse ?exprs]
   (exec [_ (assert! (count ?exprs) "\"exec\" expressions can't have empty bodies.")
          =exprs (mapcat-m analyse ?exprs)
          =exprs-types (map-m &&/expr-type =exprs)]
-    (return (list [::&&/Expression [::&&/exec =exprs] (last =exprs-types)]))))
+    (return (|list [::&&/Expression [::&&/exec =exprs] (last =exprs-types)]))))
 
 (defn analyse-jvm-try [analyse ?body [?catches ?finally]]
   (exec [=body (&&/analyse-1 analyse ?body)
          =catches (map-m (fn [[?ex-class ?ex-arg ?catch-body]]
-                           (&&env/with-local ?ex-arg [::&type/Data ?ex-class]
+                           (&&env/with-local ?ex-arg (&/V "Data" (to-array [?ex-class (&/V "Nil" nil)]))
                              (exec [=catch-body (&&/analyse-1 analyse ?catch-body)]
                                (return [?ex-class ?ex-arg =catch-body]))))
                          ?catches)
          =finally (&&/analyse-1 analyse ?finally)
          =body-type (&&/expr-type =body)]
-    (return (list [::&&/Expression [::&&/jvm-try =body =catches =finally] =body-type]))))
+    (return (|list [::&&/Expression [::&&/jvm-try =body =catches =finally] =body-type]))))
 
 (defn analyse-jvm-throw [analyse ?ex]
   (exec [=ex (&&/analyse-1 analyse ?ex)]
-    (return (list [::&&/Expression [::&&/jvm-throw =ex] [::&type/Nothing]]))))
+    (return (|list [::&&/Expression [::&&/jvm-throw =ex] (&/V "Nothing" nil)]))))
 
 (defn analyse-jvm-monitorenter [analyse ?monitor]
   (exec [=monitor (&&/analyse-1 analyse ?monitor)]
-    (return (list [::&&/Expression [::&&/jvm-monitorenter =monitor] [::&type/Any]]))))
+    (return (|list [::&&/Expression [::&&/jvm-monitorenter =monitor] (&/V "Tuple" (&/V "Nil" nil))]))))
 
 (defn analyse-jvm-monitorexit [analyse ?monitor]
   (exec [=monitor (&&/analyse-1 analyse ?monitor)]
-    (return (list [::&&/Expression [::&&/jvm-monitorexit =monitor] [::&type/Any]]))))
+    (return (|list [::&&/Expression [::&&/jvm-monitorexit =monitor] (&/V "Tuple" (&/V "Nil" nil))]))))
 
 (do-template [<name> <tag> <from-class> <to-class>]
   (defn <name> [analyse ?value]
     (exec [=value (&&/analyse-1 analyse ?value)]
-      (return (list [::&&/Expression [<tag> =value] [::&type/Data <to-class>]]))))
+      (return (|list [::&&/Expression [<tag> =value] (&/V "Data" (to-array [<to-class> (&/V "Nil" nil)]))]))))
 
   analyse-jvm-d2f ::&&/jvm-d2f "java.lang.Double"  "java.lang.Float"
   analyse-jvm-d2i ::&&/jvm-d2i "java.lang.Double"  "java.lang.Integer"
@@ -270,7 +256,7 @@
 (do-template [<name> <tag> <from-class> <to-class>]
   (defn <name> [analyse ?value]
     (exec [=value (&&/analyse-1 analyse ?value)]
-      (return (list [::&&/Expression [<tag> =value] [::&type/Data <to-class>]]))))
+      (return (|list [::&&/Expression [<tag> =value] (&/V "Data" (to-array [<to-class> (&/V "Nil" nil)]))]))))
 
   analyse-jvm-iand  ::&&/jvm-iand  "java.lang.Integer" "java.lang.Integer"
   analyse-jvm-ior   ::&&/jvm-ior   "java.lang.Integer" "java.lang.Integer"
@@ -285,6 +271,6 @@
   )
 
 (defn analyse-jvm-program [analyse ?args ?body]
-  (exec [=body (&&env/with-local ?args [::&type/Any]
+  (exec [=body (&&env/with-local ?args (&/V "Any" nil)
                  (&&/analyse-1 analyse ?body))]
-    (return (list [::&&/Statement [::&&/jvm-program =body]]))))
+    (return (|list [::&&/Statement [::&&/jvm-program =body]]))))
diff --git a/src/lux/analyser/lux.clj b/src/lux/analyser/lux.clj
index 077799144..f3d00015d 100644
--- a/src/lux/analyser/lux.clj
+++ b/src/lux/analyser/lux.clj
@@ -1,8 +1,10 @@
 (ns lux.analyser.lux
   (:require (clojure [template :refer [do-template]])
-            [clojure.core.match :refer [match]]
+            [clojure.core.match :as M :refer [match matchv]]
+            clojure.core.match.array
             (lux [base :as & :refer [exec return fail
-                                     if-m try-all-m map-m mapcat-m reduce-m
+                                     |list
+                                     if-m try-all-m |map% |flat-map% |fold% map-m mapcat-m reduce-m
                                      assert!]]
                  [parser :as &parser]
                  [type :as &type]
@@ -16,24 +18,28 @@
 
 ;; [Resources]
 (defn analyse-tuple [analyse ?elems]
-  (exec [=elems (mapcat-m analyse ?elems)
-         =elems-types (map-m &&/expr-type =elems)
+  (exec [=elems (|flat-map% analyse ?elems)
+         =elems-types (|map% &&/expr-type =elems)
          ;; :let [_ (prn 'analyse-tuple =elems)]
          ]
-    (return (list [::&&/Expression [::&&/tuple =elems] [::&type/Tuple =elems-types]]))))
+    (return (|list [::&&/Expression [::&&/tuple =elems] (&/V "Tuple" (&/|->list =elems-types))]))))
 
 (defn analyse-record [analyse ?elems]
-  (exec [=elems (mapcat-m (fn [[k v]]
-                            (exec [=v (&&/analyse-1 analyse v)]
-                              (return [k =v])))
-                          ?elems)
-         =elems-types (map-m (fn [[k v]]
-                               (exec [=v (&&/expr-type v)]
-                                 (return [k =v])))
+  (exec [=elems (|map% (fn [kv]
+                         (matchv ::M/objects [kv]
+                           [[k v]]
+                           (exec [=v (&&/analyse-1 analyse v)]
+                             (return (to-array [k =v])))))
+                       ?elems)
+         =elems-types (|map% (fn [kv]
+                               (matchv ::M/objects [kv]
+                                 [[k v]]
+                                 (exec [=v (&&/expr-type v)]
+                                   (return (to-array [k =v])))))
                              =elems)
          ;; :let [_ (prn 'analyse-tuple =elems)]
          ]
-    (return (list [::&&/Expression [::&&/record =elems] [::&type/Record =elems-types]]))))
+    (return (|list [::&&/Expression [::&&/record =elems] (&/V "Record" (&/|->list =elems-types))]))))
 
 (defn analyse-ident [analyse ident]
   (exec [module-name &/get-module-name]
@@ -41,13 +47,13 @@
       (let [[top & stack*] (::&/local-envs state)]
         (if-let [=bound (or (get-in top [:locals  :mappings ident])
                             (get-in top [:closure :mappings ident]))]
-          [::&/ok [state (list =bound)]]
+          [::&/ok [state (|list =bound)]]
           (let [no-binding? #(and (-> % :locals  :mappings (contains? ident) not)
                                   (-> % :closure :mappings (contains? ident) not))
                 [inner outer] (split-with no-binding? stack*)]
             (if (empty? outer)
               (if-let [global (get-in state [::&/global-env ident])]
-                [::&/ok [state (list global)]]
+                [::&/ok [state (|list global)]]
                 [::&/failure (str "[Analyser Error] Unresolved identifier: " ident)])
               (let [in-stack (cons top inner)
                     scopes (rest (reductions #(cons (:name %2) %1) (map :name outer) (reverse in-stack)))
@@ -60,12 +66,23 @@
                                              '()]
                                             (map vector (reverse in-stack) scopes)
                                             )]
-                [::&/ok [(assoc state ::&/local-envs (concat inner* outer)) (list =local)]])
+                [::&/ok [(assoc state ::&/local-envs (concat inner* outer)) (|list =local)]])
               ))
           ))
       )))
 
-(defn analyse-call [analyse =fn ?args]
+(defn ^:private analyse-apply* [analyse =fn ?args]
+  (exec [=args (|flat-map% analyse ?args)
+         =fn-type (&&/expr-type =fn)
+         :let [[=apply =apply-type] (|fold% (fn [[=fn =fn-type] =input]
+                                              (exec [=input-type (&&/expr-type =input)
+                                                     =output-type (&type/apply-lambda =fn-type =input-type)]
+                                                [[::&&/apply =fn =input] =output-type]))
+                                            [=fn =fn-type]
+                                            =args)]]
+    (return (|list [::&&/Expression =apply =apply-type]))))
+
+(defn analyse-apply [analyse =fn ?args]
   (exec [loader &/loader]
     (match =fn
       [::&&/Expression =fn-form =fn-type]
@@ -75,20 +92,18 @@
           (if macro?
             (let [macro-class (&host/location (list ?module ?name))]
               (exec [macro-expansion (&macro/expand loader macro-class ?args)]
-                (mapcat-m analyse (&/->seq macro-expansion))))
-            (exec [=args (mapcat-m analyse (&/->seq ?args))]
-              (return (list [::&&/Expression [::&&/call =fn =args] &type/+dont-care-type+])))))
-
+                (return (&/->seq (|flat-map% analyse macro-expansion)))))
+            (analyse-apply* analyse =fn ?args)))
+        
         _
-        (exec [=args (mapcat-m analyse (&/->seq ?args))]
-          (return (list [::&&/Expression [::&&/call =fn =args] &type/+dont-care-type+]))))
+        (analyse-apply* analyse =fn ?args))
 
       :else
       (fail "[Analyser Error] Can't call a statement!"))
     ))
 
-(defn analyse-case [analyse ?variant ?branches]
-  ;; (prn 'analyse-case ?variant ?branches)
+(defn analyse-case [analyse ?value ?branches]
+  ;; (prn 'analyse-case ?value ?branches)
   (exec [:let [num-branches (count ?branches)]
          _ (assert! (and (> num-branches 0) (even? num-branches))
                     "[Analyser Error] Unbalanced branches in \"case'\" expression.")
@@ -98,37 +113,43 @@
          ;; :let [_ (prn '[branches locals-per-branch max-locals] [branches locals-per-branch max-locals])]
          base-register &&env/next-local-idx
          ;; :let [_ (prn 'base-register base-register)]
-         =variant (reduce (fn [body* _] (&&env/with-local "" &type/+dont-care-type+ body*))
-                          (&&/analyse-1 analyse ?variant)
-                          (range max-locals))
-         ;; :let [_ (prn '=variant =variant)]
+         =value (&&/analyse-1 analyse ?value)
+         ;; :let [_ (prn '=value =value)]
          =bodies (map-m (partial &&case/analyse-branch analyse max-locals)
                         (map vector locals-per-branch (map second branches)))
          ;; :let [_ (prn '=bodies =bodies)]
          ;; :let [_ (prn 'analyse-case/=bodies =bodies)]
          =body-types (map-m &&/expr-type =bodies)
-         =case-type (return [::&type/Any]) ;; (reduce-m &type/merge [::&type/Nothing] =body-types)
+         =case-type (reduce-m &type/merge (&/V "Nothing" nil) =body-types)
          :let [=branches (map vector (map first branches) =bodies)]]
-    (return (list [::&&/Expression [::&&/case =variant base-register max-locals =branches] =case-type]))))
+    (return (|list [::&&/Expression [::&&/case =value base-register max-locals =branches] =case-type]))))
 
 (defn analyse-lambda [analyse ?self ?arg ?body]
-  (exec [[_ =arg =return :as =lambda-type] &type/fresh-function
-         [=scope =captured =body] (&&lambda/with-lambda ?self =lambda-type
-                                    ?arg =arg
-                                    (&&/analyse-1 analyse ?body))
-         =body-type (&&/expr-type =body)
-         =lambda-type (exec [_ (&type/solve =return =body-type)]
-                        (&type/clean =lambda-type))]
-    (return (list [::&&/Expression [::&&/lambda =scope =captured ?arg =body] =lambda-type]))))
+  (exec [=lambda-type* &type/fresh-lambda]
+    (matchv ::M/objects [=lambda-type*]
+      [["Lambda" [=arg =return]]]
+      (exec [[=scope =captured =body] (&&lambda/with-lambda ?self =lambda-type*
+                                        ?arg =arg
+                                        (&&/analyse-1 analyse ?body))
+             =body-type (&&/expr-type =body)
+             =lambda-type (exec [_ (&type/solve =return =body-type)
+                                 =lambda-type** (&type/clean =return =lambda-type*)]
+                            (&type/clean =arg =lambda-type**))]
+        (return (|list [::&&/Expression [::&&/lambda =scope =captured ?arg =body] =lambda-type]))))))
 
 (defn analyse-get [analyse ?slot ?record]
-  (exec [=record (&&/analyse-1 analyse ?record)]
-    (return (list [::&&/Expression [::&&/get ?slot =record] &type/+dont-care-type+]))))
+  (exec [=record (&&/analyse-1 analyse ?record)
+         =record-type (&&/expr-type =record)
+         =slot-type (&type/slot-type =record-type ?slot)]
+    (return (|list [::&&/Expression [::&&/get ?slot =record] =slot-type]))))
 
 (defn analyse-set [analyse ?slot ?value ?record]
   (exec [=value (&&/analyse-1 analyse ?value)
-         =record (&&/analyse-1 analyse ?record)]
-    (return (list [::&&/Expression [::&&/set ?slot =value =record] &type/+dont-care-type+]))))
+         =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 [::&&/Expression [::&&/set ?slot =value =record] =slot-type]))))
 
 (defn analyse-def [analyse ?name ?value]
   ;; (prn 'analyse-def ?name ?value)
@@ -138,13 +159,34 @@
           (exec [=value (&&/analyse-1 analyse ?value)
                  =value-type (&&/expr-type =value)
                  _ (&&def/define module-name ?name =value-type)]
-            (return (list [::&&/Statement [::&&/def ?name =value]]))))))
+            (return (|list [::&&/Statement [::&&/def ?name =value]]))))))
 
 (defn analyse-declare-macro [?ident]
   (exec [module-name &/get-module-name
          _ (&&def/declare-macro module-name ?ident)]
-    (return (list))))
+    (return (|list))))
 
 (defn analyse-import [analyse ?path]
   (assert false)
-  (return (list)))
+  (return (|list)))
+
+(defn analyse-check [analyse eval! ?type ?value]
+  (exec [=type (&&/analyse-1 analyse ?type)
+         =type-type (&&/expr-type =type)
+         _ (&type/solve &type/+type+ =type-type)
+         ==type (eval! =type)
+         =value (&&/analyse-1 analyse ?value)]
+    (match =value
+      [::&&/Expression ?expr ?expr-type]
+      (exec [_ (&type/solve ==type ?expr-type)]
+        (return [::&&/Expression ?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 (eval! =type)
+         =value (&&/analyse-1 analyse ?value)]
+    (match =value
+      [::&&/Expression ?expr ?expr-type]
+      (return [::&&/Expression ?expr ==type]))))
diff --git a/src/lux/base.clj b/src/lux/base.clj
index aa39d591b..d2d06c6ea 100644
--- a/src/lux/base.clj
+++ b/src/lux/base.clj
@@ -101,17 +101,6 @@
       then-m
       else-m)))
 
-(do-template [<name> <joiner>]
-  (defn <name> [f inputs]
-    (if (empty? inputs)
-      (return '())
-      (exec [output (f (first inputs))
-             outputs (<name> f (rest inputs))]
-        (return (<joiner> output outputs)))))
-
-  map-m    cons
-  mapcat-m concat)
-
 (defn reduce-m [f init inputs]
   (if (empty? inputs)
     (return init)
@@ -208,7 +197,12 @@
    ::local-envs (list)
    ::types +init-bindings+
    ::writer nil
-   ::loader (-> (java.io.File. "./output/") .toURL vector into-array java.net.URLClassLoader.)})
+   ::loader (-> (java.io.File. "./output/") .toURL vector into-array java.net.URLClassLoader.)
+   ::eval-ctor 0})
+
+(def get-eval-ctor
+  (fn [state]
+    (return* (update-in state [::eval-ctor] inc) (::eval-ctor state))))
 
 (def get-writer
   (fn [state]
@@ -274,9 +268,15 @@
 (defn run-state [monad state]
   (monad state))
 
+(defn T [& elems]
+  (to-array elems))
+
 (defn V [tag value]
   (to-array [tag value]))
 
+(defn R [& kvs]
+  (to-array (reduce concat '() kvs)))
+
 (defn ->seq [xs]
   (matchv ::M/objects [xs]
     [["Nil" _]]
@@ -314,3 +314,64 @@
     [["Form" ?elems]]
     (str "(" (->> (->seq ?elems) (map show-ast) (interpose " ") (apply str)) ")")
     ))
+
+(defn |map [f xs]
+  (matchv ::M/objects [xs]
+    [["Nil" _]]
+    xs
+
+    [["Cons" [x xs*]]]
+    (V "Cons" (to-array [(f x) (|map f xs*)]))))
+
+(defn |->list [seq]
+  (reduce (fn [tail head]
+            (V "Cons" (to-array [head tail])))
+          (V "Nil" nil)
+          seq))
+
+(let [cons% (fn [head tail]
+              (V "Cons" (to-array [head tail])))
+      ++% (fn ++% [xs ys]
+            (matchv ::M/objects [xs]
+              [["Nil" _]]
+              ys
+
+              [["Cons" [x xs*]]]
+              (V "Cons" (to-array [x (++% xs* ys)]))))]
+  (do-template [<name> <joiner>]
+    (defn <name> [f xs]
+      (matchv ::M/objects [xs]
+        [["Nil" _]]
+        (return xs)
+
+        [["Cons" [x xs*]]]
+        (exec [y (f x)
+               ys (<name> f xs*)]
+          (return (<joiner> y ys)))))
+
+    |map%      cons%
+    |flat-map% ++%))
+
+(defn |fold% [f init xs]
+  (matchv ::M/objects [xs]
+    [["Nil" _]]
+    init
+    
+    [["Cons" [x xs*]]]
+    (|fold% f (f init x) xs*)))
+
+(defn |get [record slot]
+  (matchv ::M/objects [record]
+    [["Nil" _]]
+    (V "Error" (str "Not found: " slot))
+    
+    [["Cons" [[k v] record*]]]
+    (if (= k slot)
+      (V "Ok" v)
+      (|get record* slot))))
+
+(defmacro |list [elems]
+  (reduce (fn [tail head]
+            `(V "Cons" (to-array [~head ~tail])))
+          `(V "Nil" nil)
+          elems))
diff --git a/src/lux/compiler.clj b/src/lux/compiler.clj
index 6fea4f405..6f626c2eb 100644
--- a/src/lux/compiler.clj
+++ b/src/lux/compiler.clj
@@ -331,7 +331,35 @@
     _
     (fail "[Compiler Error] Can't compile expressions as top-level forms.")))
 
-(let [compiler-step (exec [analysis+ &optimizer/optimize
+(defn ^:private eval! [expr]
+  (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)
+                        (-> (.visitField (+ Opcodes/ACC_PUBLIC Opcodes/ACC_FINAL Opcodes/ACC_STATIC) "_eval" "Ljava/lang/Object;" nil nil)
+                            (doto (.visitEnd))))]
+         _ (&/with-writer (.visitMethod =class Opcodes/ACC_PUBLIC "<clinit>" "()V" nil nil)
+             (exec [*writer* &/get-writer
+                    :let [_ (.visitCode *writer*)]
+                    _ (compile-expression expr)
+                    :let [_ (doto *writer*
+                              (.visitFieldInsn Opcodes/PUTSTATIC class-name "_eval" "Ljava/lang/Object;")
+                              (.visitInsn Opcodes/RETURN)
+                              (.visitMaxs 0 0)
+                              (.visitEnd))]]
+               (return nil)))
+         :let [bytecode (.toByteArray (doto =class
+                                        .visitEnd))]
+         _ (&&/save-class! class-file bytecode)
+         loader &/loader]
+    (-> (.loadClass loader class-name)
+        (.getField "_eval")
+        (.get nil)
+        return)))
+
+(let [compiler-step (exec [analysis+ (&optimizer/optimize eval!)
                            ;; :let [_ (prn 'analysis+ analysis+)]
                            ]
                       (mapcat-m compile-statement analysis+))]
diff --git a/src/lux/compiler/host.clj b/src/lux/compiler/host.clj
index 81b8f3981..5d2b06d76 100644
--- a/src/lux/compiler/host.clj
+++ b/src/lux/compiler/host.clj
@@ -2,7 +2,8 @@
   (:require (clojure [string :as string]
                      [set :as set]
                      [template :refer [do-template]])
-            [clojure.core.match :refer [match]]
+            [clojure.core.match :as M :refer [match matchv]]
+            clojure.core.match.array
             (lux [base :as & :refer [exec return* return fail fail*
                                      repeat-m exhaust-m try-m try-all-m map-m reduce-m
                                      apply-m
@@ -41,25 +42,24 @@
       long-class "java.lang.Long"
       char-class "java.lang.Character"]
   (defn prepare-return! [*writer* *type*]
-    (match *type*
-      [::&type/Nothing]
+    (matchv ::M/objects [*type*]
+      [["Nothing" nil]]
       (.visitInsn *writer* Opcodes/ACONST_NULL)
 
-      [::&type/Data "char"]
+      [["Data" ["char" _]]]
       (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host/->class char-class) "valueOf" (str "(C)" (&host/->type-signature char-class)))
 
-      [::&type/Data "int"]
+      [["Data" ["int" _]]]
       (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host/->class integer-class) "valueOf" (str "(I)" (&host/->type-signature integer-class)))
 
-      [::&type/Data "long"]
+      [["Data" ["long" _]]]
       (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host/->class long-class) "valueOf" (str "(J)" (&host/->type-signature long-class)))
 
-      [::&type/Data "boolean"]
+      [["Data" ["boolean" _]]]
       (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host/->class boolean-class) "valueOf" (str "(Z)" (&host/->type-signature boolean-class)))
 
-      [::&type/Data _]
-      nil
-      )
+      [["Data" [_ _]]]
+      nil)
     *writer*))
 
 ;; [Resources]
diff --git a/src/lux/compiler/lambda.clj b/src/lux/compiler/lambda.clj
index 004f09743..c6595fc5e 100644
--- a/src/lux/compiler/lambda.clj
+++ b/src/lux/compiler/lambda.clj
@@ -66,7 +66,7 @@
                  $start (new Label)
                  $end (new Label)
                  _ (doto *writer*
-                     (-> (.visitLocalVariable (str &&/local-prefix idx) (&host/->java-sig [::&type/Any]) nil $start $end (+ 2 idx))
+                     (-> (.visitLocalVariable (str &&/local-prefix idx) (&host/->java-sig (&/V "Any" nil)) nil $start $end (+ 2 idx))
                          (->> (dotimes [idx num-locals])))
                      (.visitLabel $start))]
            ret (compile impl-body)
diff --git a/src/lux/host.clj b/src/lux/host.clj
index ef4f1ca54..767b331e7 100644
--- a/src/lux/host.clj
+++ b/src/lux/host.clj
@@ -21,11 +21,11 @@
                                               "")
                                             (.getSimpleName class)))]
     (if (= "void" base)
-      (return [::&type/Nothing])
-      (let [base* [::&type/Data base]]
+      (return (&/V "Nothing" nil))
+      (let [base* (&/V "Data" (to-array [base (&/V "Nil" nil)]))]
         (if arr-level
           (return (reduce (fn [inner _]
-                            [::&type/Array inner])
+                            (&/V "array" (&/V "Cons" (to-array [inner (&/V "Nil" nil)]))))
                           base*
                           (range (/ (count arr-level) 2.0))))
           (return base*)))
@@ -80,20 +80,20 @@
     ))
 
 (defn ->java-sig [type]
-  (match type
-    [::&type/Any]
+  (matchv ::M/objects [type]
+    [["Any" _]]
     (->type-signature "java.lang.Object")
 
-    [::&type/Nothing]
+    [["Nothing" _]]
     "V"
     
-    [::&type/Data ?name]
-    (->type-signature ?name)
-
-    [::&type/Array ?elem]
+    [["Data" ["array" ["Cons" [?elem ["Nil" _]]]]]]
     (str "[" (->java-sig ?elem))
 
-    [::&type/Lambda _ _]
+    [["Data" [?name ?params]]]
+    (->type-signature ?name)
+
+    [["Lambda" [_ _]]]
     (->type-signature function-class)))
 
 (defn extract-jvm-param [token]
diff --git a/src/lux/optimizer.clj b/src/lux/optimizer.clj
index 0daabe2b5..5c93bfbfb 100644
--- a/src/lux/optimizer.clj
+++ b/src/lux/optimizer.clj
@@ -13,4 +13,5 @@
 ;; Convert pattern-matching on booleans into regular if-then-else structures
 
 ;; [Exports]
-(def optimize &analyser/analyse)
+(defn optimize [eval!]
+  (&analyser/analyse eval!))
diff --git a/src/lux/parser.clj b/src/lux/parser.clj
index f506f5dc2..d60458b2f 100644
--- a/src/lux/parser.clj
+++ b/src/lux/parser.clj
@@ -10,9 +10,9 @@
     (exec [elems (repeat-m parse)
            token &lexer/lex]
       (if (= <close-token> token)
-        (return (list (&/V <tag> (reduce #(&/V "Cons" (to-array [%2 %1]))
-                                         (&/V "Nil" nil)
-                                         (reverse (apply concat elems))))))
+        (return (|list (&/V <tag> (reduce #(&/V "Cons" (to-array [%2 %1]))
+                                          (&/V "Nil" nil)
+                                          (reverse (apply concat elems))))))
         (fail (str "[Parser Error] Unbalanced " <description> ".")))))
 
   ^:private parse-form  [::&lexer/close-paren]   "parantheses" "Form"
@@ -30,9 +30,9 @@
           (fail (str "[Parser Error] Records must have an even number of elements."))
 
           :else
-          (return (list (&/V "Record" (reduce #(&/V "Cons" (to-array [%2 %1]))
-                                              (&/V "Nil" nil)
-                                              (reverse elems))))))))
+          (return (|list (&/V "Record" (reduce #(&/V "Cons" (to-array [%2 %1]))
+                                               (&/V "Nil" nil)
+                                               (reverse elems))))))))
 
 ;; [Interface]
 (def parse
@@ -41,31 +41,31 @@
          ]
     (match token
       [::&lexer/white-space _]
-      (return (list))
+      (return (|list))
 
       [::&lexer/comment _]
-      (return (list))
+      (return (|list))
       
       [::&lexer/bool ?value]
-      (return (list (&/V "Bool" (Boolean/parseBoolean ?value))))
+      (return (|list (&/V "Bool" (Boolean/parseBoolean ?value))))
 
       [::&lexer/int ?value]
-      (return (list (&/V "Int" (Integer/parseInt ?value))))
+      (return (|list (&/V "Int" (Integer/parseInt ?value))))
 
       [::&lexer/real ?value]
-      (return (list (&/V "Real" (Float/parseFloat ?value))))
+      (return (|list (&/V "Real" (Float/parseFloat ?value))))
 
       [::&lexer/char ?value]
-      (return (list (&/V "Char" (.charAt ?value 0))))
+      (return (|list (&/V "Char" (.charAt ?value 0))))
 
       [::&lexer/text ?value]
-      (return (list (&/V "Text" ?value)))
+      (return (|list (&/V "Text" ?value)))
 
       [::&lexer/ident ?value]
-      (return (list (&/V "Ident" ?value)))
+      (return (|list (&/V "Ident" ?value)))
 
       [::&lexer/tag ?value]
-      (return (list (&/V "Tag" ?value)))
+      (return (|list (&/V "Tag" ?value)))
 
       [::&lexer/open-paren]
       (parse-form parse)
diff --git a/src/lux/type.clj b/src/lux/type.clj
index 339a030d9..9c3e6f35b 100644
--- a/src/lux/type.clj
+++ b/src/lux/type.clj
@@ -1,7 +1,9 @@
 (ns lux.type
   (:refer-clojure :exclude [deref apply merge])
-  (:require [clojure.core.match :refer [match]]
+  (:require [clojure.core.match :as M :refer [match matchv]]
+            clojure.core.match.array
             [lux.base :as & :refer [exec return* return fail fail*
+                                    |get
                                     repeat-m try-m try-all-m map-m
                                     sequence-m
                                     apply-m assert!]]))
@@ -11,326 +13,261 @@
 
 (defn ^:private deref [id]
   (fn [state]
-    (if-let [top+bottom (get-in state [::&/types :mappings id])]
-      [::&/ok [state top+bottom]]
+    (if-let [type (get-in state [::&/types :mappings id])]
+      [::&/ok [state type]]
       [::&/failure (str "Unknown type-var: " id)])))
 
-(defn ^:private update [id top bottom]
+(defn ^:private reset [id type]
   (fn [state]
-    (if-let [top+bottom (get-in state [::&/types :mappings id])]
-      [::&/ok [(assoc-in state [::&/types :mappings id] [top bottom]) nil]]
+    (if-let [_ (get-in state [::&/types :mappings id])]
+      [::&/ok [(assoc-in state [::&/types :mappings id] (&/V "Some" type)) nil]]
       [::&/failure (str "Unknown type-var: " id)])))
 
-;; [Interface]
+;; [Exports]
 (def fresh-var
   (fn [state]
     (let [id (-> state ::&/types :counter)]
       [::&/ok [(update-in state [::&/types]
                           #(-> %
                                (update-in [:counter] inc)
-                               (assoc-in [:mappings id] [[::Any] [::Nothing]])))
-               [::Var id]]])))
+                               (assoc-in [:mappings id] (&/V "None" nil))))
+               (&/V "Var" id)]])))
 
-(def fresh-function
+(def fresh-lambda
   (exec [=arg fresh-var
          =return fresh-var]
-    (return [::Lambda =arg =return])))
-
-;; (defn solve [expected actual]
-;;   ;; (prn 'solve expected actual)
-;;   (match [expected actual]
-;;     [::any _]
-;;     success
-
-;;     [_ ::nothing]
-;;     success
-
-;;     [_ [::var ?id]]
-;;     (exec [[=top =bottom] (deref ?id)]
-;;       (try-all-m [(exec [_ (solve expected =top)]
-;;                     success)
-;;                   (exec [_ (solve =top expected)
-;;                          _ (solve expected =bottom)
-;;                          _ (update ?id expected =bottom)]
-;;                     success)]))
-
-;;     [[::var ?id] _]
-;;     (exec [[=top =bottom] (deref ?id)]
-;;       (try-all-m [(exec [_ (solve =bottom actual)]
-;;                     success)
-;;                   (exec [_ (solve actual =bottom)
-;;                          _ (solve =top actual)
-;;                          _ (update ?id =top actual)]
-;;                     success)]))
-
-;;     ;; [[::primitive ?prim] _]
-;;     ;; (let [as-obj (case ?prim
-;;     ;;                "boolean" [:lang.type/object "java.lang.Boolean" []]
-;;     ;;                "int"     [:lang.type/object "java.lang.Integer" []]
-;;     ;;                "long"    [:lang.type/object "java.lang.Long" []]
-;;     ;;                "char"    [:lang.type/object "java.lang.Character" []]
-;;     ;;                "float"   [:lang.type/object "java.lang.Float" []]
-;;     ;;                "double"  [:lang.type/object "java.lang.Double" []])]
-;;     ;;   (solve as-obj actual))
-
-;;     [[::primitive ?e-prim] [::primitive ?a-prim]]
-;;     (if (= ?e-prim ?a-prim)
-;;       success
-;;       (fail (str "Can't solve types: " (pr-str expected actual))))
-
-;;     [[::object ?eclass []] [::object ?aclass []]]
-;;     (if (.isAssignableFrom (Class/forName ?eclass) (Class/forName ?aclass))
-;;       success
-;;       (fail (str "Can't solve types: " (pr-str expected actual))))
-
-;;     [_ _]
-;;     (fail (str "Can't solve types: " (pr-str expected actual)))
-;;     ))
-
-;; (defn pick-matches [methods args]
-;;   (if (empty? methods)
-;;     (fail "No matches.")
-;;     (try-all-m [(match (-> methods first second)
-;;                   [::function ?args ?return]
-;;                   (exec [_ (assert! (= (count ?args) (count args)) "Args-size doesn't match.")
-;;                          _ (map-m (fn [[e a]] (solve e a)) (map vector ?args args))]
-;;                     (return (first methods))))
-;;                 (pick-matches (rest methods) args)])))
+    (return (&/V "Lambda" (to-array [=arg =return])))))
+
+(defn ^:private ->type [pseudo-type]
+  (match pseudo-type
+    [::Any]
+    (&/V "Any" nil)
+
+    [::Nothing]
+    (&/V "Nothing" nil)
+
+    [::Data ?name ?elems]
+    (&/V "Data" (to-array [?name ?elems]))
+
+    [::Tuple ?members]
+    (&/V "Tuple" (&/|map ->type ?members))
+    
+    [::Variant ?members]
+    (&/V "Variant" (&/|map (fn [[k v]] (to-array [k (->type v)]))
+                           ?members))
+
+    [::Record ?members]
+    (&/V "Record" (&/|map (fn [[k v]] (to-array [k (->type v)]))
+                          ?members))
+
+    [::Lambda ?input ?output]
+    (&/V "Lambda" (to-array [(->type ?input) (->type ?output)]))
+    
+    [::App ?lambda ?param]
+    (&/V "App" (to-array [(->type ?lambda) (->type ?param)]))
+
+    [::Bound ?name]
+    (&/V "Bound" ?name)
 
-(defn clean [type]
-  (match type
     [::Var ?id]
-    (exec [[=top =bottom] (deref ?id)]
-      (clean =top))
+    (&/V "Var" ?id)
+
+    [::All ?env ?name ?arg ?body]
+    (&/V "All" (to-array [(&/|map (fn [[k v]] (to-array [k (->type v)]))
+                                  ?env)
+                          ?name
+                          ?arg
+                          (->type ?body)]))
+    ))
+
+(def +list+
+  [::All (&/|->list (list)) "List" "a"
+   [::Variant (&/|->list (list ["Cons" [::Tuple (&/|->list (list [::Bound "a"] [::App [::Bound "List"] [::Bound "a"]]))]]
+                               ["Nil" [::Tuple (&/|->list (list))]]
+                               ))]])
+
+(def +type+
+  (let [text [::Data "java.lang.String" (&/|->list (list))]
+        type [::App [::Bound "Type"] [::Any]]
+        list-of-types [::App +list+ type]
+        string=>type [::App +list+ [::Tuple (&/|->list (list text type))]]]
+    (->type [::All (&/|->list (list)) "Type" "_"
+             [::Variant (&/|->list (list ["Any"  [::Tuple (&/|->list (list))]]
+                                         ["Nothing"  [::Tuple (&/|->list (list))]]
+                                         ["Data" [::Tuple (&/|->list (list text list-of-types))]]
+                                         ["Tuple" list-of-types]
+                                         ["Variant" string=>type]
+                                         ["Record" string=>type]
+                                         ["Lambda" [::Tuple (&/|->list (list type
+                                                                             type))]]
+                                         ["App" [::Tuple (&/|->list (list type
+                                                                          type))]]
+                                         ["Bound" text]
+                                         ["Var" [::Data "java.lang.Long" (&/|->list (list))]]
+                                         ["All" [::Tuple (&/|->list (list string=>type text text type))]]
+                                         ))]])))
 
-    [::Lambda ?arg ?return]
+(defn clean [type]
+  (matchv ::M/objects [type]
+    [["Var" ?id]]
+    (exec [=type (deref ?id)]
+      (clean =type))
+
+    [["Lambda" [?arg ?return]]]
     (exec [=arg (clean ?arg)
            =return (clean ?return)]
-      (return [::Lambda =arg =return]))
+      (return (&/V "Lambda" (to-array [=arg =return]))))
+
+    [["App" [?lambda ?param]]]
+    (exec [=lambda (clean ?lambda)
+           =param (clean ?param)]
+      (return (&/V "App" (to-array [=lambda =param]))))
 
-    _
+    [["Tuple" ?members]]
+    (exec [=members (&/|map% clean ?members)]
+      (return (&/V "Tuple" =members)))
+    
+    [["Variant" ?members]]
+    (exec [=members (&/|map% (fn [[k v]]
+                               (exec [=v (clean v)]
+                                 (return (to-array [k =v]))))
+                             ?members)]
+      (return (&/V "Variant" =members)))
+
+    [["Record" ?members]]
+    (exec [=members (&/|map% (fn [[k v]]
+                               (exec [=v (clean v)]
+                                 (return (to-array [k =v]))))
+                             ?members)]
+      (return (&/V "Record" =members)))
+
+    [["All" [?env ?name ?arg ?body]]]
+    (exec [=env (&/|map% (fn [[k v]]
+                           (exec [=v (clean v)]
+                             (return (to-array [k =v]))))
+                         ?env)]
+      (return (&/V "All" (to-array [=env ?name ?arg ?body]))))
+
+    [_]
     (return type)
     ))
 
-;; Java Reflection
-(def success (return nil))
-
-(defn solve [needed given]
-  (match [needed given]
-    [[::Any] _]
+(defn solve [expected actual]
+  (matchv ::M/objects [expected actual]
+    [["Any" _] _]
     success
 
-    [_ [::Nothing]]
+    [_ ["Nothing" _]]
     success
 
-    [[::Data n!name] [::Data g!name]]
-    (cond (or (= n!name g!name)
-              (.isAssignableFrom (Class/forName n!name) (Class/forName g!name)))
-          success
-
-          :else
-          (fail (str "not (" given " <= " needed ")")))
+    [["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 n!elems] [::Tuple g!elems]]
-    (exec [_ (assert! (= (count n!elems) (count g!elems))
+    [["Tuple" e!elems] ["Tuple" a!elems]]
+    (exec [:let [e!elems (&/->seq e!elems)
+                 a!elems (&/->seq a!elems)]
+           _ (assert! (= (count e!elems) (count a!elems))
                       "Tuples must have matching element sizes.")
            _ (map-m (fn [n g] (solve n g))
-                    (map vector n!elems g!elems))]
+                    (map vector e!elems a!elems))]
       success)
 
-    [[::Variant n!cases] [::Variant g!cases]]
-    (exec [_ (assert! (every? (partial contains? n!cases) (keys g!cases))
+    [["Variant" e!cases] ["Variant" a!cases]]
+    (exec [:let [e!cases (reduce #(assoc %1 (aget %2 0) (aget %2 1)) {} (&/->seq e!cases))
+                 a!cases (reduce #(assoc %1 (aget %2 0) (aget %2 1)) {} (&/->seq a!cases))]
+           _ (assert! (every? (partial contains? e!cases) (keys a!cases))
                       "The given variant contains unhandled cases.")
            _ (map-m (fn [label]
-                      (solve (get n!cases label) (get g!cases label)))
-                    (keys g!cases))]
+                      (solve (get e!cases label) (get a!cases label)))
+                    (keys a!cases))]
       success)
 
-    [[::Record n!fields] [::Record g!fields]]
-    (exec [_ (assert! (every? (partial contains? g!fields) (keys n!fields))
+    [["Record" e!fields] ["Record" a!fields]]
+    (exec [:let [e!fields (reduce #(assoc %1 (aget %2 0) (aget %2 1)) {} (&/->seq e!fields))
+                 a!fields (reduce #(assoc %1 (aget %2 0) (aget %2 1)) {} (&/->seq a!fields))]
+           _ (assert! (every? (partial contains? a!fields) (keys e!fields))
                       "The given record lacks necessary fields.")
            _ (map-m (fn [label]
-                      (solve (get n!fields label) (get g!fields label)))
-                    (keys n!fields))]
+                      (solve (get e!fields label) (get a!fields label)))
+                    (keys e!fields))]
       success)
 
-    [[::Lambda n!input n!output] [::Lambda g!input g!output]]
-    (exec [_ (solve g!input n!input)]
-      (solve n!output g!output))
+    [["Lambda" [e!input e!output]] ["Lambda" [a!input a!output]]]
+    (exec [_ (solve a!input e!input)]
+      (solve e!output a!output))
 
-    [[::Var n!id] _]
-    (exec [[n!top n!bottom] (deref n!id)
-           _ (solve n!top given)
-           _ (solve given n!bottom)
-           _ (update n!id n!top given)]
+    [["Var" e!id] _]
+    (exec [=e!type (deref e!id)
+           _ (solve =e!type actual)
+           _ (reset e!id =e!type)]
+      success)
+
+    [_ ["Var" a!id]]
+    (exec [=a!type (deref a!id)
+           _ (solve expected =a!type)
+           _ (reset a!id =a!type)]
       success)
     ))
 
 (let [&& #(and %1 %2)]
   (defn merge [x y]
-    (match [x y]
-      [_ [::Nothing]]
+    (matchv ::M/objects [x y]
+      [_ ["Any" _]]
+      (return y)
+
+      [["Any" _] _]
       (return x)
 
-      [[::Nothing] _]
+      [_ ["Nothing" _]]
+      (return x)
+
+      [["Nothing" _] _]
       (return y)
 
-      [[::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 [::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))))
+      ;; [["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))))
       
-      :else
+      [_ _]
       (fail (str "Can't merge types: " (pr-str x) " and " (pr-str y))))))
 
-(def +dont-care-type+ [::Any])
-
-(comment
-  ;; Types
-  [::Any]
-  [::Nothing]
-  [::Tuple (list)]
-  [::Lambda input output]
-  [::Variant {}]
-  [::Record {}]
-  [::Data name]
-  [::All self {} arg body]
-  [::Exists evar body]
-  [::Bound name]
-
-  ;; ???
-  [::Alias name args type]
-  [::Var id]
-  
-
-  ;; (deftype #rec Type
-  ;;   (| #Any
-  ;;     #Nothing
-  ;;     (#Tuple (List Type))
-  ;;     (#Lambda Type Type)
-  ;;     (#Variant (List [Text Type]))
-  ;;     (#Record (List [Text Type]))
-  ;;     (#Data Text)))
-  
-  
-  
-  ;; (deftype #rec Kind
-  ;;   (| (#Type Type)
-  ;;     (#All Text (List [Text Kind]) Text Kind)))
-
-  ;; (deftype (Higher lower)
-  ;;     (| (#Lower lower)
-  ;;        (#Apply (Higher lower) (Higher lower))
-  ;;        (#All Text (List [Text lower]) Text (Higher lower))
-  ;;        (#Exists (List [Text lower]) Text (Higher lower))))
-
-  ;; (deftype Kind (Higher Type))
-  ;; (deftype Sort (Higher Kind))
-  
-  
-  
-  ;; (deftype HList (| (#Cons (Exists x x) HList)
-  ;;                   #Nil))
-
-  ;; (def success (return nil))
-
-  ;; (defn apply [type-lambda input]
-  ;;   (match type-lambda
-  ;;     [::All ?self ?env ?arg ?body]
-  ;;     (let [env* (-> ?env
-  ;;                    (assoc ?arg input)
-  ;;                    (assoc ?self type-lambda))]
-  ;;       (match ?body
-  ;;         [::All ?sub-self _ ?sub-arg ?sub-body]
-  ;;         [::All ?sub-self env* ?sub-arg ?sub-body]
-
-  ;;         _
-  ;;         (beta-reduce env* ?body)))))
-  
-  ;; (defn solve [needed given]
-  ;;   (match [needed given]
-  ;;     [[::Any] _]
-  ;;     success
-
-  ;;     [_ [::Nothing]]
-  ;;     success
-  
-  ;;     [[::Tuple n!elems] [::Tuple g!elems]]
-  ;;     (exec [_ (assert! (= (count n!elems) (count g!elems))
-  ;;                       "Tuples must have matching element sizes.")
-  ;;            _ (map-m (fn [[n g]] (solve n g))
-  ;;                     (map vector n!elems g!elems))]
-  ;;       success)
-  
-  ;;     [[::Variant n!cases] [::Variant g!cases]]
-  ;;     (exec [_ (assert! (every? (partial contains? n!cases) (keys g!cases))
-  ;;                       "The given variant contains unhandled cases.")
-  ;;            _ (map-m (fn [label]
-  ;;                       (solve (get n!cases label) (get g!cases label)))
-  ;;                     (keys g!cases))]
-  ;;       success)
-
-  ;;     [[::Record n!fields] [::Record g!fields]]
-  ;;     (exec [_ (assert! (every? (partial contains? g!fields) (keys n!fields))
-  ;;                       "The given record lacks necessary fields.")
-  ;;            _ (map-m (fn [label]
-  ;;                       (solve (get n!fields label) (get g!fields label)))
-  ;;                     (keys n!fields))]
-  ;;       success)
-
-  ;;     [[::Lambda n!input n!output] [::Lambda g!input g!output]]
-  ;;     (exec [_ (solve g!input n!input)
-  ;;            _ (solve n!output g!output)]
-  ;;       success)
-  ;;     ))
-
-  ;; (deftype (List x)
-  ;;     (| (#Cons x (List x))
-  ;;        #Nil))
-
-  ;; (deftype List
-  ;;     (All List [x]
-  ;;          (| (#Cons x (List x))
-  ;;             #Nil)))
-
-  ;; (def List
-  ;;   [::All "List" {} x
-  ;;    [::Variant {"Cons" [::Tuple (list [::Local x] [::Apply {} [::Local "List"] [::Local x]])]
-  ;;                "Nil" [::Tuple (list)]}]])
-
-  ;; (deftype User
-  ;;     {#name Text
-  ;;      #email Text
-  ;;      #password Text
-  ;;      #joined Time
-  ;;      #last-login Time})
-
-  ;; (deftype (Pair x y)
-  ;;     [x y])
-
-  ;; (deftype (State s a)
-  ;;     (-> s [a s]))
-
-  ;; (: + (-> Int Int Int))
-  ;; (def (+ x y)
-  ;;   (jvm:ladd x y))
-
-  
-  )
+(defn apply-lambda [func param]
+  (matchv ::M/objects [func]
+    [["Lambda" [input output]]]
+    (exec [_ (solve input param)]
+      (return output))
+
+    [_]
+    (fail (str "Can't apply type " (str func) " to type " (str param)))))
+
+(defn slot-type [record slot]
+  (fn [state]
+    (matchv ::M/objects [(|get record slot)]
+      [["Error" msg]]
+      (fail* msg)
+
+      [["Ok" type]]
+      (return* state type))))
+
+(def +dont-care+ (&/V "Any" nil))