- Fixed a few type-related bugs.

- Variants now need types to be specified both when constructing them as when deconstructing them (in pattern-matching).
- Simplified DataT types by no-longer requiring a list of params, so only the tame name is necessary.

10 files changed, 468 insertions, 499 deletions

diff --git a/source/lux.lux b/source/lux.lux
index 34d766b52..357366d58 100644
--- a/source/lux.lux
+++ b/source/lux.lux
@@ -25,11 +25,11 @@
 
 ## Basic types
 (def' Any #AnyT)
-(def' Bool (#DataT ["java.lang.Boolean" #Nil]))
-(def' Int (#DataT ["java.lang.Long" #Nil]))
-(def' Real (#DataT ["java.lang.Double" #Nil]))
-(def' Char (#DataT ["java.lang.Character" #Nil]))
-(def' Text (#DataT ["java.lang.String" #Nil]))
+(def' Bool (#DataT "java.lang.Boolean"))
+(def' Int (#DataT "java.lang.Long"))
+(def' Real (#DataT "java.lang.Double"))
+(def' Char (#DataT "java.lang.Character"))
+(def' Text (#DataT "java.lang.String"))
 
 ## (deftype (List a)
 ##   (| #Nil
@@ -62,7 +62,7 @@
                 (#AppT [(#AllT [#Nil "Type" ""
                                 (#VariantT (#Cons [["lux;AnyT" (#TupleT #Nil)]
                                                    (#Cons [["lux;NothingT" (#TupleT #Nil)]
-                                                           (#Cons [["lux;DataT" (#TupleT (#Cons [Text (#Cons [(#AppT [List Type]) #Nil])]))]
+                                                           (#Cons [["lux;DataT" Text]
                                                                    (#Cons [["lux;TupleT" (#AppT [List (#AppT [(#BoundT "Type") (#BoundT "")])])]
                                                                            (#Cons [["lux;VariantT" TypeEnv]
                                                                                    (#Cons [["lux;RecordT" TypeEnv]
@@ -74,175 +74,187 @@
                                                                                                                                    #Nil])])])])])])])])])])]))])
                         #NothingT]))))
 
-## (deftype (Maybe a)
-##   (| #None
-##      (#Some a)))
-(def' Maybe
-  (#AllT [#Nil "Maybe" "a"
-          (#VariantT (#Cons [["lux;None" (#TupleT #Nil)]
-                             (#Cons [["lux;Some" (#BoundT "a")]
-                                     #Nil])]))]))
+## ## (deftype (Maybe a)
+## ##   (| #None
+## ##      (#Some a)))
+## (def' Maybe
+##   (#AllT [#Nil "Maybe" "a"
+##           (#VariantT (#Cons [["lux;None" (#TupleT #Nil)]
+##                              (#Cons [["lux;Some" (#BoundT "a")]
+##                                      #Nil])]))]))
+
+## ## (deftype (Bindings k v)
+## ##   (& #counter Int
+## ##      #mappings (List (, k v))))
+## (def' Bindings
+##   (#AllT [#Nil "Bindings" "k"
+##           (#AllT [#Nil "" "v"
+##                   (#RecordT (#Cons [["lux;counter" Int]
+##                                     (#Cons [["lux;mappings" (#AppT [List
+##                                                                     (#TupleT (#Cons [(#BoundT "k")
+##                                                                                      (#Cons [(#BoundT "v")
+##                                                                                              #Nil])]))])]
+##                                             #Nil])]))])]))
+
+## ## (deftype (Env k v)
+## ##   (& #name Text
+## ##      #inner-closures Int
+## ##      #locals  (Bindings k v)
+## ##      #closure (Bindings k v)))
+## (def' Env
+##   (#AllT [#Nil "Env" "k"
+##           (#AllT [#Nil "" "v"
+##                   (#RecordT (#Cons [["lux;name" Text]
+##                                     (#Cons [["lux;inner-closures" Int]
+##                                             (#Cons [["lux;locals" (#AppT [(#AppT [Bindings (#BoundT "k")])
+##                                                                           (#BoundT "v")])]
+##                                                     (#Cons [["lux;closure" (#AppT [(#AppT [Bindings (#BoundT "k")])
+##                                                                                    (#BoundT "v")])]
+##                                                             #Nil])])])]))])]))
+
+## ## (deftype Cursor
+## ##   (, Text Int Int))
+## (def' Cursor
+##   (#TupleT (#Cons [Text (#Cons [Int (#Cons [Int #Nil])])])))
+
+## ## (deftype (Meta m v)
+## ##   (| (#Meta (, m v))))
+## (def' Meta
+##   (#AllT [#Nil "Meta" "m"
+##           (#AllT [#Nil "" "v"
+##                   (#VariantT (#Cons [["lux;Meta" (#TupleT (#Cons [(#BoundT "m")
+##                                                                   (#Cons [(#BoundT "v")
+##                                                                           #Nil])]))]
+##                                      #Nil]))])]))
+
+## ## (def' Reader
+## ##   (List (Meta Cursor Text)))
+## (def' Reader
+##   (#AppT [List
+##           (#AppT [(#AppT [Meta Cursor])
+##                   Text])]))
+
+## ## (deftype Compiler_State
+## ##   (& #source         (Maybe Reader)
+## ##      #modules        (List Any)
+## ##      #module-aliases (List Any)
+## ##      #global-env     (Maybe (Env Text Any))
+## ##      #local-envs     (List (Env Text Any))
+## ##      #types          (Bindings Int Type)
+## ##      #writer         (^ org.objectweb.asm.ClassWriter)
+## ##      #loader         (^ java.net.URLClassLoader)
+## ##      #eval-ctor      Int))
+## (def' Compiler_State
+##   (#RecordT (#Cons [["lux;source" (#AppT [Maybe Reader])]
+##                     (#Cons [["lux;modules" (#AppT [List Any])]
+##                             (#Cons [["lux;module-aliases" (#AppT [List Any])]
+##                                     (#Cons [["lux;global-env" (#AppT [Maybe (#AppT [(#AppT [Env Text]) Any])])]
+##                                             (#Cons [["lux;local-envs" (#AppT [List (#AppT [(#AppT [Env Text]) Any])])]
+##                                                     (#Cons [["lux;types" (#AppT [(#AppT [Bindings Int]) Type])]
+##                                                             (#Cons [["lux;writer" (#DataT "org.objectweb.asm.ClassWriter")]
+##                                                                     (#Cons [["lux;loader" (#DataT "java.lang.ClassLoader")]
+##                                                                             (#Cons [["lux;eval-ctor" Int]
+##                                                                                     #Nil])])])])])])])])])))
 
-## (deftype (Bindings k v)
-##   (& #counter Int
-##      #mappings (List (, k v))))
-(def' Bindings
-  (#AllT [#Nil "Bindings" "k"
-          (#AllT [#Nil "" "v"
-                  (#RecordT (#Cons [["lux;counter" Int]
-                                    (#Cons [["lux;mappings" (#AppT [List
-                                                                    (#TupleT (#Cons [(#BoundT "k")
-                                                                                     (#Cons [(#BoundT "v")
-                                                                                             #Nil])]))])]
-                                            #Nil])]))])]))
-
-## (deftype (Env k v)
-##   (& #name Text
-##      #inner-closures Int
-##      #locals  (Bindings k v)
-##      #closure (Bindings k v)))
-(def' Env
-  (#AllT [#Nil "Env" "k"
-          (#AllT [#Nil "" "v"
-                  (#RecordT (#Cons [["lux;name" Text]
-                                    (#Cons [["lux;inner-closures" Int]
-                                            (#Cons [["lux;locals" (#AppT [(#AppT [Bindings (#BoundT "k")])
-                                                                          (#BoundT "v")])]
-                                                    (#Cons [["lux;closure" (#AppT [(#AppT [Bindings (#BoundT "k")])
-                                                                                   (#BoundT "v")])]
-                                                            #Nil])])])]))])]))
-
-## (deftype Cursor
-##   (, Text Int Int))
-(def' Cursor
-  (#TupleT (#Cons [Text (#Cons [Int (#Cons [Int #Nil])])])))
-
-## (deftype (Meta m v)
-##   (| (#Meta (, m v))))
-(def' Meta
-  (#AllT [#Nil "Meta" "m"
-          (#AllT [#Nil "" "v"
-                  (#VariantT (#Cons [["lux;Meta" (#TupleT (#Cons [(#BoundT "m")
-                                                                  (#Cons [(#BoundT "v")
-                                                                          #Nil])]))]
-                                     #Nil]))])]))
+## ## (deftype #rec Syntax
+## ##   (Meta Cursor (| (#Bool Bool)
+## ##                   (#Int Int)
+## ##                   (#Real Real)
+## ##                   (#Char Char)
+## ##                   (#Text Text)
+## ##                   (#Form (List Syntax))
+## ##                   (#Tuple (List Syntax))
+## ##                   (#Record (List (, Text Syntax))))))
+## (def' Syntax
+##   (case' (#AppT [(#BoundT "Syntax") (#BoundT "")])
+##          Syntax
+##          (case' (#AppT [List Syntax])
+##                 SyntaxList
+##                 (#AppT [(#AllT [#Nil "Syntax" ""
+##                                 (#VariantT (#Cons [["lux;Bool" Bool]
+##                                                    (#Cons [["lux;Int" Int]
+##                                                            (#Cons [["lux;Real" Real]
+##                                                                    (#Cons [["lux;Char" Char]
+##                                                                            (#Cons [["lux;Text" Text]
+##                                                                                    (#Cons [["lux;Form" SyntaxList]
+##                                                                                            (#Cons [["lux;Tuple" SyntaxList]
+##                                                                                                    (#Cons [["lux;Record" (#AppT [List (#TupleT (#Cons [Text (#Cons [Syntax #Nil])]))])]
+##                                                                                                            #Nil])])])])])])])]))])
+##                         #NothingT]))))
 
-## (def' Reader
-##   (List (Meta Cursor Text)))
-(def' Reader
-  (#AppT [List
-          (#AppT [(#AppT [Meta Cursor])
-                  Text])]))
-
-## (deftype CompilerState
-##   (& #source         (Maybe Reader)
-##      #modules        (List Any)
-##      #module-aliases (List Any)
-##      #global-env     (Maybe (Env Text Any))
-##      #local-envs     (List (Env Text Any))
-##      #types          (Bindings Int Type)
-##      #writer         (^ org.objectweb.asm.ClassWriter)
-##      #loader         (^ java.net.URLClassLoader)
-##      #eval-ctor      Int))
-(def' CompilerState
-  (#RecordT (#Cons [["lux;source" (#AppT [Maybe Reader])]
-                    (#Cons [["lux;modules" (#AppT [List Any])]
-                            (#Cons [["lux;module-aliases" (#AppT [List Any])]
-                                    (#Cons [["lux;global-env" (#AppT [Maybe (#AppT [(#AppT [Env Text]) Any])])]
-                                            (#Cons [["lux;local-envs" (#AppT [List (#AppT [(#AppT [Env Text]) Any])])]
-                                                    (#Cons [["lux;types" (#AppT [(#AppT [Bindings Int]) Type])]
-                                                            (#Cons [["lux;writer" (#DataT ["org.objectweb.asm.ClassWriter" #Nil])]
-                                                                    (#Cons [["lux;loader" (#DataT ["java.lang.ClassLoader" #Nil])]
-                                                                            (#Cons [["lux;eval-ctor" Int]
-                                                                                    #Nil])])])])])])])])])))
-
-## (deftype #rec Syntax
-##   (Meta Cursor (| (#Bool Bool)
-##                   (#Int Int)
-##                   (#Real Real)
-##                   (#Char Char)
-##                   (#Text Text)
-##                   (#Form (List Syntax))
-##                   (#Tuple (List Syntax))
-##                   (#Record (List (, Text Syntax))))))
-(def' Syntax
-  (case' (#AppT [(#BoundT "Syntax") (#BoundT "")])
-         Syntax
-         (case' (#AppT [List Syntax])
-                SyntaxList
-                (#AppT [(#AllT [#Nil "Syntax" ""
-                                (#VariantT (#Cons [["lux;Bool" Bool]
-                                                   (#Cons [["lux;Int" Int]
-                                                           (#Cons [["lux;Real" Real]
-                                                                   (#Cons [["lux;Char" Char]
-                                                                           (#Cons [["lux;Text" Text]
-                                                                                   (#Cons [["lux;Form" SyntaxList]
-                                                                                           (#Cons [["lux;Tuple" SyntaxList]
-                                                                                                   (#Cons [["lux;Record" (#AppT [List (#TupleT (#Cons [Text (#Cons [Syntax #Nil])]))])]
-                                                                                                           #Nil])])])])])])])]))])
-                        #NothingT]))))
+## ## (deftype (Either l r)
+## ##   (| (#Left l)
+## ##      (#Right r)))
+## (def' Either
+##   (#AllT [#Nil "_" "l"
+##           (#AllT [#Nil "" "r"
+##                   (#VariantT (#Cons [["lux;Left" (#BoundT "l")]
+##                                      (#Cons [["lux;Right" (#BoundT "r")]
+##                                              #Nil])]))])]))
 
-## (deftype (Either l r)
-##   (| (#Left l)
-##      (#Right r)))
-(def' Either
-  (#AllT [#Nil "Either" "l"
-          (#AllT [#Nil "" "r"
-                  (#VariantT (#Cons [["lux;Left" (#BoundT "l")]
-                                     (#Cons [["lux;Right" (#BoundT "r")]
-                                             #Nil])]))])]))
-
-## (deftype Macro
-##   (-> (List Syntax) CompilerState
-##       (Either Text [CompilerState (List Syntax)])))
-(def' Macro
-  (case' (#AppT [List Syntax])
-         SyntaxList
-         (#LambdaT [SyntaxList
-                    (#LambdaT [CompilerState
-                               (#AppT [(#AppT [Either Text])
-                                       (#TupleT (#Cons [CompilerState
-                                                        (#Cons [SyntaxList #Nil])]))])])])))
-
-## Base functions & macros
-## (def (_meta data)
-##   (All [a] (-> a (Meta Cursor a)))
-##   (#Meta [["" -1 -1] data]))
-(def' _meta
-  (check' (#AllT [#Nil "" "a"
-                  (#LambdaT [(#BoundT "a")
-                             (#AppT [(#AppT [Meta Cursor])
-                                     (#BoundT "a")])])])
-          (lambda' _ data
-                   (#Meta [["" -1 -1] data]))))
+## ## (deftype Macro
+## ##   (-> (List Syntax) Compiler_State
+## ##       (Either Text [Compiler_State (List Syntax)])))
+## (def' Macro
+##   (case' (#AppT [List Syntax])
+##          SyntaxList
+##          (#LambdaT [SyntaxList
+##                     (#LambdaT [CompilerState
+##                                (#AppT [(#AppT [Either Text])
+##                                        (#TupleT (#Cons [CompilerState
+##                                                         (#Cons [SyntaxList #Nil])]))])])])))
+
+## ## Base functions & macros
+## ## (def (_meta data)
+## ##   (All [a] (-> a (Meta Cursor a)))
+## ##   (#Meta [["" -1 -1] data]))
+## (def' _meta
+##   (check' (#AllT [#Nil "_" "a"
+##                   (#LambdaT [(#BoundT "a")
+##                              (#AppT [(#AppT [Meta Cursor])
+##                                      (#BoundT "a")])])])
+##           (lambda' _ data
+##                    (#Meta [["" -1 -1] data]))))
+
+## ## (def' let'
+## ##   (check' Macro
+## ##           (lambda' _ tokens
+## ##                    (lambda' _ state
+## ##                        (case' tokens
+## ##                               (#Cons [lhs (#Cons [rhs (#Cons [body #Nil])])])
+## ##                               (#Right [state
+## ##                                        (#Cons [(_meta (#Form (#Cons [(_meta (#Symbol ["" "case'"]))
+## ##                                                                      (#Cons [rhs (#Cons [lhs (#Cons [body #Nil])])])])))
+## ##                                                #Nil])])
+
+## ##                               _
+## ##                               (#Left "Wrong syntax for let'"))
+## ##                        ))))
+## ## (def' let'
+## ##   (check' Macro
+## ##           (lambda' _ tokens
+## ##               (lambda' _ state
+## ##                   (#Left "Wrong syntax for let'")
+## ##                   ))))
+## (def' let'
+##   (check' (#AppT [(#AppT [Either Text])
+##                   (#TupleT (#Cons [CompilerState
+##                                    (#Cons [(#AppT [List Syntax]) #Nil])]))])
+##           (#Left "Wrong syntax for let'")))
 
 ## (def' let'
-##   (check' Macro
-##           (lambda' _ tokens
-##                    (lambda' _ state
-##                        (case' tokens
-##                               (#Cons [lhs (#Cons [rhs (#Cons [body #Nil])])])
-##                               (#Right [state
-##                                        (#Cons [(_meta (#Form (#Cons [(_meta (#Symbol ["" "case'"]))
-##                                                                      (#Cons [rhs (#Cons [lhs (#Cons [body #Nil])])])])))
-##                                                #Nil])])
-
-##                               _
-##                               (#Left "Wrong syntax for let'"))
-##                        ))))
-(def' let'
-  (lambda' _ tokens
-      (lambda' _ state
-          (case' tokens
-                 (#Cons [lhs (#Cons [rhs (#Cons [body #Nil])])])
-                 (#Right [state
-                          (#Cons [(_meta (#Form (#Cons [(_meta (#Symbol ["" "case'"]))
-                                                        (#Cons [rhs (#Cons [lhs (#Cons [body #Nil])])])])))
-                                  #Nil])])
-
-                 _
-                 (#Left "Wrong syntax for let'"))
-          )))
+##   (lambda' _ tokens
+##       (lambda' _ state
+##           (case' tokens
+##                  (#Cons [lhs (#Cons [rhs (#Cons [body #Nil])])])
+##                  (#Right [state
+##                           (#Cons [(_meta (#Form (#Cons [(_meta (#Symbol ["" "case'"]))
+##                                                         (#Cons [rhs (#Cons [lhs (#Cons [body #Nil])])])])))
+##                                   #Nil])])
+
+##                  _
+##                  (#Left "Wrong syntax for let'"))
+##           )))
 ## (declare-macro' let')
 
 ## ## ## (All  21268
@@ -1048,10 +1060,8 @@
 ## ## (defmacro (^ tokens)
 ## ##   (case' tokens
 ## ##          (#Cons [(#Meta [_ (#Symbol [_ class-name])]) #Nil])
-## ##          (return (list (` (#DataT [(~ (_meta (#Text class-name))) (list)]))))
-
-## ##          (#Cons [(#Meta [_ (#Symbol [_ class-name])]) (#Cons [(#Meta [_ (#Tuple params)]) #Nil])])
-## ##          (return (list (` (#DataT [(~ (_meta (#Text class-name))) (~ (untemplate-list params))]))))))
+## ##          (return (list (` (#DataT (~ (_meta (#Text class-name)))))))
+## ##          ))
 
 ## ## (defmacro (, members)
 ## ##   (return (list (_meta (#Form (list+ (_meta (#Tag ["lux" "TupleT"])) (untemplate-list members)))))))
diff --git a/src/lux/analyser.clj b/src/lux/analyser.clj
index 156af6631..39eaf9e16 100644
--- a/src/lux/analyser.clj
+++ b/src/lux/analyser.clj
@@ -38,19 +38,19 @@
   (matchv ::M/objects [token]
     ;; Standard special forms
     [["lux;Meta" [meta ["lux;Bool" ?value]]]]
-    (return (&/|list (&/V "Expression" (&/T (&/V "bool" ?value) (&/V "lux;DataT" (&/T "java.lang.Boolean" (|list)))))))
+    (return (&/|list (&/V "Expression" (&/T (&/V "bool" ?value) &type/Bool))))
 
     [["lux;Meta" [meta ["lux;Int" ?value]]]]
-    (return (&/|list (&/V "Expression" (&/T (&/V "int" ?value)  (&/V "lux;DataT" (&/T "java.lang.Long" (|list)))))))
+    (return (&/|list (&/V "Expression" (&/T (&/V "int" ?value)  &type/Int))))
 
     [["lux;Meta" [meta ["lux;Real" ?value]]]]
-    (return (&/|list (&/V "Expression" (&/T (&/V "real" ?value) (&/V "lux;DataT" (&/T "java.lang.Double" (|list)))))))
+    (return (&/|list (&/V "Expression" (&/T (&/V "real" ?value) &type/Real))))
 
     [["lux;Meta" [meta ["lux;Char" ?value]]]]
-    (return (&/|list (&/V "Expression" (&/T (&/V "char" ?value) (&/V "lux;DataT" (&/T "java.lang.Character" (|list)))))))
+    (return (&/|list (&/V "Expression" (&/T (&/V "char" ?value) &type/Char))))
 
     [["lux;Meta" [meta ["lux;Text" ?value]]]]
-    (return (&/|list (&/V "Expression" (&/T (&/V "text" ?value) (&/V "lux;DataT" (&/T "java.lang.String" (|list)))))))
+    (return (&/|list (&/V "Expression" (&/T (&/V "text" ?value) &type/Text))))
 
     [["lux;Meta" [meta ["lux;Tuple" ?elems]]]]
     (&&lux/analyse-tuple analyse exo-type ?elems)
@@ -62,7 +62,7 @@
     (&&lux/analyse-variant analyse exo-type ?ident (_meta (&/V "lux;Tuple" (|list))))
     
     [["lux;Meta" [meta ["lux;Symbol" [_ "jvm-null"]]]]]
-    (return (&/|list (&/V "Expression" (&/T (&/V "jvm-null" nil) (&/V "lux;DataT" (&/T "null" (|list)))))))
+    (return (&/|list (&/V "Expression" (&/T (&/V "jvm-null" nil) (&/V "lux;DataT" "null")))))
     
     [["lux;Meta" [meta ["lux;Symbol" ?ident]]]]
     (&&lux/analyse-symbol analyse exo-type ?ident)
@@ -422,7 +422,7 @@
     (fail (str "[Analyser Error] Unmatched token: " (&/show-ast token)))))
 
 (defn ^:private analyse-ast [eval! exo-type token]
-  ;; (prn 'analyse-ast token)
+  ;; (prn 'analyse-ast (aget token 0))
   (matchv ::M/objects [token]
     [["lux;Meta" [meta ["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Tag" ?ident]]] ?values]]]]]]
     (do (assert (= 1 (&/|length ?values)) "[Analyser Error] Can only tag 1 value.")
diff --git a/src/lux/analyser/base.clj b/src/lux/analyser/base.clj
index b287b545f..0d2d8304a 100644
--- a/src/lux/analyser/base.clj
+++ b/src/lux/analyser/base.clj
@@ -11,7 +11,7 @@
   (matchv ::M/objects [syntax+]
     [["Expression" [_ type]]]
     (do ;; (prn 'expr-type (&type/show-type type))
-      (return type))
+        (return type))
     
     [["Statement" _]]
     (fail (str "[Analyser Error] Can't retrieve the type of a statement: " (pr-str syntax+)))))
@@ -19,26 +19,26 @@
 (defn analyse-1 [analyse exo-type elem]
   (|do [output (analyse exo-type elem)]
     (do ;; (prn 'analyse-1 (aget output 0))
-      (matchv ::M/objects [output]
-        [["lux;Cons" [x ["lux;Nil" _]]]]
-        (return x)
+        (matchv ::M/objects [output]
+          [["lux;Cons" [x ["lux;Nil" _]]]]
+          (return x)
 
-        [_]
-        (fail "[Analyser Error] Can't expand to other than 1 element.")))))
+          [_]
+          (fail "[Analyser Error] Can't expand to other than 1 element.")))))
 
 (defn analyse-2 [analyse el1 el2]
   (|do [output (&/flat-map% analyse (&/|list el1 el2))]
     (do ;; (prn 'analyse-2 (aget output 0))
-      (matchv ::M/objects [output]
-        [["lux;Cons" [x ["lux;Cons" [y ["lux;Nil" _]]]]]]
-        (return [x y])
+        (matchv ::M/objects [output]
+          [["lux;Cons" [x ["lux;Cons" [y ["lux;Nil" _]]]]]]
+          (return [x y])
 
-        [_]
-        (fail "[Analyser Error] Can't expand to other than 2 elements.")))))
+          [_]
+          (fail "[Analyser Error] Can't expand to other than 2 elements.")))))
 
 (defn with-var [k]
   (|do [=var &type/fresh-var
-         =ret (k =var)]
+        =ret (k =var)]
     (matchv ::M/objects [=ret]
       [["Expression" [?expr ?type]]]
       (|do [=type (&type/clean =var ?type)]
diff --git a/src/lux/analyser/case.clj b/src/lux/analyser/case.clj
index c33e32af1..6b2fe7a03 100644
--- a/src/lux/analyser/case.clj
+++ b/src/lux/analyser/case.clj
@@ -9,9 +9,7 @@
 
 ;; [Utils]
 (defn ^:private analyse-variant [analyse-pattern idx value-type tag value]
-  (|do [=var &type/fresh-var
-        _ (&type/check value-type (&/V "lux;VariantT" (&/|list (&/T tag =var))))
-        [idx* test] (analyse-pattern idx =var value)]
+  (|do [[idx* test] (analyse-pattern idx value-type value)]
     (return (&/T idx* (&/V "VariantTestAC" (&/T tag test))))))
 
 (defn ^:private analyse-pattern [idx value-type pattern]
@@ -19,17 +17,17 @@
   (matchv ::M/objects [pattern]
     [["lux;Meta" [_ pattern*]]]
     ;; (assert false)
-    (do (prn 'analyse-pattern/pattern* (aget pattern* 0))
-      (when (= "lux;Form" (aget pattern* 0))
-        (prn 'analyse-pattern/_2 (aget pattern* 1 0)) ;; "lux;Cons"
-        (prn 'analyse-pattern/_2 (aget pattern* 1 1 0 0)) ;; "lux;Meta"
-        (prn 'analyse-pattern/_2 (alength (aget pattern* 1 1 0 1)))
-        (prn 'analyse-pattern/_2 (aget pattern* 1 1 0 1 1 0)) ;; "lux;Tag"
-        (prn 'analyse-pattern/_2 [(aget pattern* 1 1 0 1 1 1 0) (aget pattern* 1 1 0 1 1 1 1)]) ;; ["" "Cons"]
-        (prn 'analyse-pattern/_2 (aget pattern* 1 1 1 0)) ;; "lux;Cons"
-        (prn 'analyse-pattern/_2 (aget pattern* 1 1 1 1 0)) ;; #<Object[] [Ljava.lang.Object;@63c7c38b>
-        (prn 'analyse-pattern/_2 (aget pattern* 1 1 1 1 1 0)) ;; "lux;Nil"
-        )
+    (do ;; (prn 'analyse-pattern/pattern* (aget pattern* 0))
+      ;; (when (= "lux;Form" (aget pattern* 0))
+      ;;   (prn 'analyse-pattern/_2 (aget pattern* 1 0)) ;; "lux;Cons"
+      ;;   (prn 'analyse-pattern/_2 (aget pattern* 1 1 0 0)) ;; "lux;Meta"
+      ;;   (prn 'analyse-pattern/_2 (alength (aget pattern* 1 1 0 1)))
+      ;;   (prn 'analyse-pattern/_2 (aget pattern* 1 1 0 1 1 0)) ;; "lux;Tag"
+      ;;   (prn 'analyse-pattern/_2 [(aget pattern* 1 1 0 1 1 1 0) (aget pattern* 1 1 0 1 1 1 1)]) ;; ["" "Cons"]
+      ;;   (prn 'analyse-pattern/_2 (aget pattern* 1 1 1 0)) ;; "lux;Cons"
+      ;;   (prn 'analyse-pattern/_2 (aget pattern* 1 1 1 1 0)) ;; #<Object[] [Ljava.lang.Object;@63c7c38b>
+      ;;   (prn 'analyse-pattern/_2 (aget pattern* 1 1 1 1 1 0)) ;; "lux;Nil"
+      ;;   )
       ;; ["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Tag" [?module ?name]]]]
       ;;                          ["lux;Cons" [?value
       ;;                                       ["lux;Nil" _]]]]]]
@@ -281,8 +279,10 @@
                   (every? true? totals))))
 
     [_ ["VariantTotal" [?total ?structs]]]
-    (|do [real-type (resolve-type value-type)]
-      (assert false))
+    (&/try-all% (&/|list (|do [real-type (resolve-type value-type)
+                               :let [_ (prn 'real-type (&type/show-type real-type))]]
+                           (assert false))
+                         (fail "[Pattern-maching error] Can't pattern-match on an unknown variant type.")))
     
     [_ ["DefaultTotal" true]]
     (return true)
diff --git a/src/lux/analyser/host.clj b/src/lux/analyser/host.clj
index 6fce672de..33ceb2b22 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;DataT" (to-array [<input-class> (&/V "lux;Nil" nil)]))
-        output-type (&/V "lux;DataT" (to-array [<output-class> (&/V "lux;Nil" nil)]))]
+  (let [input-type (&/V "lux;DataT" <input-class>)
+        output-type (&/V "lux;DataT" <output-class>)]
     (defn <name> [analyse ?x ?y]
       (|do [[=x =y] (&&/analyse-2 analyse ?x ?y)
              =x-type (&&/expr-type =x)
@@ -126,17 +126,17 @@
 
 (defn analyse-jvm-null? [analyse ?object]
   (|do [=object (&&/analyse-1 analyse ?object)]
-    (return (&/|list (&/V "Expression" (&/T (&/V "jvm-null?" =object) (&/V "lux;DataT" (&/T "java.lang.Boolean" (&/V "lux;Nil" nil)))))))))
+    (return (&/|list (&/V "Expression" (&/T (&/V "jvm-null?" =object) (&/V "lux;DataT" "java.lang.Boolean")))))))
 
 (defn analyse-jvm-new [analyse ?class ?classes ?args]
   (|do [=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;DataT" (&/T =class (&/V "lux;Nil" nil)))))))))
+    (return (&/|list (&/V "Expression" (&/T (&/V "jvm-new" (&/T =class =classes =args)) (&/V "lux;DataT" =class)))))))
 
 (defn analyse-jvm-new-array [analyse ?class ?length]
   (|do [=class (&host/full-class-name ?class)]
-    (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)]))
+    (return (&/|list (&/V "Expression" (&/T (&/V "jvm-new-array" (&/T =class ?length)) (&/V "array" (&/T (&/V "lux;DataT" =class)
                                                                                                          (&/V "lux;Nil" nil)))))))))
 
 (defn analyse-jvm-aastore [analyse ?array ?idx ?elem]
@@ -198,7 +198,7 @@
 (defn analyse-jvm-try [analyse ?body [?catches ?finally]]
   (|do [=body (&&/analyse-1 analyse ?body)
          =catches (&/map% (fn [[?ex-class ?ex-arg ?catch-body]]
-                            (&&env/with-local ?ex-arg (&/V "lux;DataT" (&/T ?ex-class (&/V "lux;Nil" nil)))
+                            (&&env/with-local ?ex-arg (&/V "lux;DataT" ?ex-class)
                               (|do [=catch-body (&&/analyse-1 analyse ?catch-body)]
                                 (return [?ex-class ?ex-arg =catch-body]))))
                           ?catches)
@@ -221,7 +221,7 @@
 (do-template [<name> <tag> <from-class> <to-class>]
   (defn <name> [analyse ?value]
     (|do [=value (&&/analyse-1 analyse ?value)]
-      (return (&/|list (&/V "Expression" (&/T (&/V <tag> =value) (&/V "lux;DataT" (&/T <to-class> (&/V "lux;Nil" nil)))))))))
+      (return (&/|list (&/V "Expression" (&/T (&/V <tag> =value) (&/V "lux;DataT" <to-class>)))))))
 
   analyse-jvm-d2f "jvm-d2f" "java.lang.Double"  "java.lang.Float"
   analyse-jvm-d2i "jvm-d2i" "java.lang.Double"  "java.lang.Integer"
@@ -246,7 +246,7 @@
 (do-template [<name> <tag> <from-class> <to-class>]
   (defn <name> [analyse ?value]
     (|do [=value (&&/analyse-1 analyse ?value)]
-      (return (&/|list (&/V "Expression" (&/T (&/V <tag> =value) (&/V "lux;DataT" (&/T <to-class> (&/V "lux;Nil" nil)))))))))
+      (return (&/|list (&/V "Expression" (&/T (&/V <tag> =value) (&/V "lux;DataT" <to-class>)))))))
 
   analyse-jvm-iand  "jvm-iand"  "java.lang.Integer" "java.lang.Integer"
   analyse-jvm-ior   "jvm-ior"   "java.lang.Integer" "java.lang.Integer"
diff --git a/src/lux/analyser/lux.clj b/src/lux/analyser/lux.clj
index 61ca08b42..a9a42ffe3 100644
--- a/src/lux/analyser/lux.clj
+++ b/src/lux/analyser/lux.clj
@@ -19,30 +19,53 @@
 
 ;; [Exports]
 (defn analyse-tuple [analyse exo-type ?elems]
-  (|do [=elems (&/map% (analyse-1+ analyse) ?elems)
-        =elems-types (&/map% &&/expr-type =elems)
-        ;; :let [_ (prn 'analyse-tuple =elems)]
-        :let [endo-type (&/V "lux;TupleT" =elems-types)]
-        _ (&type/check exo-type endo-type)
-        ;; :let [_ (prn 'analyse-tuple 'DONE)]
-        ]
+  (prn 'analyse-tuple (str "[" (->> ?elems (&/|map &/show-ast) (&/|interpose " ") (&/fold str "")) "]")
+       (&type/show-type exo-type))
+  (|do [members-vars (&/map% (constantly &type/fresh-var) ?elems)
+        _ (&type/check exo-type (&/V "lux;TupleT" members-vars))
+        =elems (&/map% (fn [ve]
+                         (|let [[=var elem] ve]
+                           (|do [output (&&/analyse-1 analyse =var elem)]
+                             (matchv ::M/objects [output]
+                               [["Expression" [?val ?type]]]
+                               (|do [=val-type (&type/clean =var ?type)]
+                                 (return (&/V "Expression" (&/T ?val exo-type))))))))
+                       (&/zip2 members-vars ?elems))]
     (return (&/|list (&/V "Expression" (&/T (&/V "tuple" =elems)
                                             exo-type))))))
 
 (defn analyse-variant [analyse exo-type ident ?value]
   (|let [[?module ?name] ident]
-    (|do [module (if (= "" ?module)
-                   &/get-module-name
-                   (return ?module))
-          :let [?tag (str module ";" ?name)]
-          =value ((analyse-1+ analyse) ?value)
-          =value-type (&&/expr-type =value)
-          :let [endo-type (&/V "lux;VariantT" (|list (&/T ?tag =value-type)))]
-          _ (&type/check exo-type endo-type)
-          ;; :let [_ (prn 'analyse-variant 'DONE)]
-          ]
-      (return (&/|list (&/V "Expression" (&/T (&/V "variant" (&/T ?tag =value))
-                                              exo-type)))))))
+    (do (prn 'analyse-variant (str ?module ";" ?name) (&/show-ast ?value))
+      (|do [:let [_ (prn 'analyse-variant/exo-type (&type/show-type exo-type))]
+            module (if (= "" ?module)
+                     &/get-module-name
+                     (return ?module))
+            :let [?tag (str module ";" ?name)]
+            exo-type* (matchv ::M/objects [exo-type]
+                        [["lux;VarT" ?id]]
+                        (|do [? (&type/bound? ?id)]
+                          (if ?
+                            (|do [exo-type (&type/deref ?id)]
+                              (&type/actual-type exo-type))
+                            (|do [_ (&type/set-var ?id &type/Type)]
+                              (&type/actual-type &type/Type))))
+
+                        [_]
+                        (&type/actual-type exo-type))
+            :let [_ (prn 'exo-type* (&type/show-type exo-type*))]]
+        (matchv ::M/objects [exo-type*]
+          [["lux;VariantT" ?cases]]
+          (if-let [vtype (&/|get ?tag ?cases)]
+            (|do [:let [_ (prn 'VARIANT_BODY ?tag (&/show-ast ?value) (&type/show-type vtype))]
+                  =value (&&/analyse-1 analyse vtype ?value)
+                  :let [_ (prn 'GOT_VALUE =value)]]
+              (return (&/|list (&/V "Expression" (&/T (&/V "variant" (&/T ?tag =value))
+                                                      exo-type)))))
+            (fail (str "[Analyser Error] There is no case " ?tag " for variant type " (&type/show-type exo-type*))))
+
+          [_]
+          (fail (str "[Analyser Error] Can't create a variant if the expected type is " (&type/show-type exo-type*))))))))
 
 (defn analyse-record [analyse exo-type ?elems]
   (|do [=elems (&/map% (fn [kv]
@@ -162,39 +185,41 @@
 
 (defn analyse-lambda [analyse exo-type ?self ?arg ?body]
   ;; (prn 'analyse-lambda ?self ?arg ?body)
-  (|do [=lambda-type* &type/fresh-lambda]
+  (|do [=lambda-type* &type/fresh-lambda
+        _ (&type/check exo-type =lambda-type*)]
     (matchv ::M/objects [=lambda-type*]
       [["lux;LambdaT" [=arg =return]]]
       (|do [[=scope =captured =body] (&&lambda/with-lambda ?self =lambda-type*
                                        ?arg =arg
                                        (&&/analyse-1 analyse =return ?body))
             =lambda-type** (&type/clean =return =lambda-type*)
-            =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)]
-                             (|do [_ (&type/reset id bound)
-                                   lambda-type (&type/clean =arg =lambda-type**)]
-                               (return (&/V "lux;AllT" (&/T (&/|list) "" var-name lambda-type))))))]
+            =lambda-type (matchv ::M/objects [=arg]
+                           [["lux;VarT" ?id]]
+                           (&/try-all% (&/|list (|do [bound (&type/deref ?id)]
+                                                  (&type/clean =arg =lambda-type**))
+                                                (let [var-name (str (gensym ""))]
+                                                  (|do [_ (&type/set-var ?id (&/V "lux;BoundT" var-name))
+                                                        lambda-type (&type/clean =arg =lambda-type**)]
+                                                    (return (&/V "lux;AllT" (&/T (&/|list) "" var-name lambda-type)))))))
+
+                           [_]
+                           (fail ""))]
         (return (&/|list (&/V "Expression" (&/T (&/V "lambda" (&/T =scope =captured =body)) =lambda-type))))))))
 
 (defn analyse-def [analyse exo-type ?name ?value]
-  ;; (prn 'analyse-def ?name ?value)
-  (|do [_ (&type/check &type/Nothing exo-type)
-        module-name &/get-module-name]
-    (&/if% (&&def/defined? module-name ?name)
-           (fail (str "[Analyser Error] Can't redefine " ?name))
-           (|do [=value (&/with-scope ?name
-                          (&&/with-var
-                            #(&&/analyse-1 analyse % ?value)))
-                 =value-type (&&/expr-type =value)
-                 :let [_ (prn 'analyse-def ?name (&type/show-type =value-type))]
-                 _ (&&def/define module-name ?name =value-type)]
-             (return (&/|list (&/V "Statement" (&/V "def" (&/T ?name =value)))))))))
+  (prn 'analyse-def ?name (&/show-ast ?value))
+  (|do [_ (&type/check exo-type &type/Nothing)
+        module-name &/get-module-name
+        ? (&&def/defined? module-name ?name)]
+    (if ?
+      (fail (str "[Analyser Error] Can't redefine " ?name))
+      (|do [=value (&/with-scope ?name
+                     (&&/with-var
+                       #(&&/analyse-1 analyse % ?value)))
+            =value-type (&&/expr-type =value)
+            :let [_ (prn 'analyse-def ?name (&type/show-type =value-type))]
+            _ (&&def/define module-name ?name =value-type)]
+        (return (&/|list (&/V "Statement" (&/V "def" (&/T ?name =value)))))))))
 
 (defn analyse-declare-macro [exo-type ident]
   (|let [[?module ?name] ident]
@@ -211,23 +236,24 @@
 (defn analyse-check [analyse eval! exo-type ?type ?value]
   (println "analyse-check#0")
   (|do [=type (&&/analyse-1 analyse &type/Type ?type)
-         :let [_ (println "analyse-check#1")]
-         ==type (eval! =type)
-         _ (&type/check exo-type ==type)
-         :let [_ (println "analyse-check#4" (&type/show-type ==type))]
-         =value (&&/analyse-1 analyse ==type ?value)
-         :let [_ (println "analyse-check#5")]]
+        ;; =type ((analyse-1+ analyse) ?type)
+        :let [_ (println "analyse-check#1")]
+        ==type (eval! =type)
+        _ (&type/check exo-type ==type)
+        :let [_ (println "analyse-check#4" (&type/show-type ==type))]
+        =value (&&/analyse-1 analyse exo-type ?value)
+        :let [_ (println "analyse-check#5")]]
     (matchv ::M/objects [=value]
       [["Expression" [?expr ?expr-type]]]
       (|do [:let [_ (println "analyse-check#6" (&type/show-type ?expr-type))]
-             _ (&type/check ==type ?expr-type)
-             :let [_ (println "analyse-check#7")]]
+            _ (&type/check ==type ?expr-type)
+            :let [_ (println "analyse-check#7")]]
         (return (&/|list (&/V "Expression" (&/T ?expr ==type))))))))
 
 (defn analyse-coerce [analyse eval! exo-type ?type ?value]
   (|do [=type (&&/analyse-1 analyse &type/Type ?type)
-         ==type (eval! =type)
-         =value (&&/analyse-1 analyse ==type ?value)]
+        ==type (eval! =type)
+        =value (&&/analyse-1 analyse ==type ?value)]
     (matchv ::M/objects [=value]
       [["Expression" [?expr ?expr-type]]]
       (return (&/|list (&/V "Expression" (&/T ?expr ==type)))))))
diff --git a/src/lux/base.clj b/src/lux/base.clj
index a8649816a..91519eb0c 100644
--- a/src/lux/base.clj
+++ b/src/lux/base.clj
@@ -125,6 +125,7 @@
 ;; [Resources/Monads]
 (defn fail [message]
   (fn [_]
+    (prn 'FAIL message)
     (V "lux;Left" message)))
 
 (defn return [value]
@@ -144,8 +145,7 @@
         [["lux;Right" [?state ?datum]]]
         (let [next-fn (step ?datum)]
           (when (not (fn? next-fn))
-            (prn 'bind (aget next-fn 0)
-                 (aget next-fn 1)))
+            (prn 'bind (aget next-fn 0) (aget next-fn 1)))
           (next-fn ?state))
         
         [["lux;Left" _]]
@@ -676,7 +676,7 @@
   (monad state))
 
 (defn show-ast [ast]
-  (prn 'show-ast (aget ast 0))
+  ;; (prn 'show-ast (aget ast 0))
   ;; (prn 'show-ast (aget ast 1 1 0))
   ;; (cond (= "lux;Meta" (aget ast 1 1 0))
   ;;       (prn 'EXTRA 'show-ast (aget ast 1 1 1 1 0))
@@ -706,7 +706,9 @@
     (str "#" ?module ";" ?tag)
 
     [["lux;Meta" [_ ["lux;Symbol" [?module ?ident]]]]]
-    (str ?module ";" ?ident)
+    (if (= "" ?module)
+      ?ident
+      (str ?module ";" ?ident))
 
     [["lux;Meta" [_ ["lux;Tuple" ?elems]]]]
     (str "[" (->> ?elems (|map show-ast) (|interpose " ") (fold str "")) "]")
diff --git a/src/lux/compiler/host.clj b/src/lux/compiler/host.clj
index f289ed6ba..184c6a4f4 100644
--- a/src/lux/compiler/host.clj
+++ b/src/lux/compiler/host.clj
@@ -43,19 +43,19 @@
       [["lux;NothingT" nil]]
       (.visitInsn *writer* Opcodes/ACONST_NULL)
 
-      [["lux;DataT" ["char" _]]]
+      [["lux;DataT" "char"]]
       (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host/->class char-class) "valueOf" (str "(C)" (&host/->type-signature char-class)))
 
-      [["lux;DataT" ["int" _]]]
+      [["lux;DataT" "int"]]
       (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host/->class integer-class) "valueOf" (str "(I)" (&host/->type-signature integer-class)))
 
-      [["lux;DataT" ["long" _]]]
+      [["lux;DataT" "long"]]
       (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host/->class long-class) "valueOf" (str "(J)" (&host/->type-signature long-class)))
 
-      [["lux;DataT" ["boolean" _]]]
+      [["lux;DataT" "boolean"]]
       (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host/->class boolean-class) "valueOf" (str "(Z)" (&host/->type-signature boolean-class)))
 
-      [["lux;DataT" [_ _]]]
+      [["lux;DataT" _]]
       nil)
     *writer*))
 
diff --git a/src/lux/host.clj b/src/lux/host.clj
index b10b23995..4d1fef04a 100644
--- a/src/lux/host.clj
+++ b/src/lux/host.clj
@@ -20,13 +20,8 @@
                                             (.getSimpleName class)))]
     (if (= "void" base)
       (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)))))
-                          base*
-                          (range (/ (count arr-level) 2.0))))
-          (return base*)))
+      (return (&/V "lux;DataT" (str (reduce str "" (repeat (int (/ (count arr-level) 2)) "["))
+                                    base)))
       )))
 
 (defn ^:private method->type [method]
@@ -87,10 +82,7 @@
     [["lux;NothingT" _]]
     "V"
     
-    [["lux;DataT" ["array" ["lux;Cons" [?elem ["lux;Nil" _]]]]]]
-    (str "[" (->java-sig ?elem))
-
-    [["lux;DataT" [?name ?params]]]
+    [["lux;DataT" ?name]]
     (->type-signature ?name)
 
     [["lux;LambdaT" [_ _]]]
diff --git a/src/lux/type.clj b/src/lux/type.clj
index 1fbaa78c0..0cd839cf2 100644
--- a/src/lux/type.clj
+++ b/src/lux/type.clj
@@ -1,41 +1,50 @@
 (ns lux.type
-  (:refer-clojure :exclude [deref apply merge])
+  (:refer-clojure :exclude [deref apply merge bound?])
   (:require [clojure.core.match :as M :refer [match matchv]]
             clojure.core.match.array
             [lux.base :as & :refer [|do return* return fail fail* assert! |let]]))
 
-;; [Util]
-(def ^:private success (return nil))
-
-(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))))
+(declare show-type)
 
-    [_]
-    (fail "[Type Error] Can't lookup non-vars.")))
-
-(defn deref [id]
+;; [Util]
+(defn bound? [id]
   (fn [state]
     (if-let [type* (->> state (&/get$ "lux;types") (&/get$ "lux;mappings") (&/|get id))]
       (matchv ::M/objects [type*]
-        [["lux;Some" type]]
-        (return* state type)
+        [["lux;Some" _]]
+        (return* state true)
         
         [["lux;None" _]]
-        (fail* (str "Unbound type-var: " id)))
+        (return* state false))
       (fail* (str "Unknown type-var: " id)))))
 
-(defn reset [id type]
+(defn deref [id]
   (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) %)
-                                                         ts))
-                          state)
-               nil)
+    (let [mappings (->> state (&/get$ "lux;types") (&/get$ "lux;mappings"))]
+      (do (prn 'deref/mappings (&/->seq (&/|keys mappings)))
+        (if-let [type* (->> mappings (&/|get id))]
+          (do (prn 'deref/type* (aget type* 0))
+            (matchv ::M/objects [type*]
+              [["lux;Some" type]]
+              (return* state type)
+              
+              [["lux;None" _]]
+              (fail* (str "Unbound type-var: " id))))
+          (fail* (str "Unknown type-var: " id)))))))
+
+(defn set-var [id type]
+  (fn [state]
+    (if-let [tvar (->> state (&/get$ "lux;types") (&/get$ "lux;mappings") (&/|get id))]
+      (do ;; (prn 'set-var (aget tvar 0))
+          (matchv ::M/objects [tvar]
+            [["lux;Some" bound]]
+            (fail* (str "Can't rebind type var: " id " | Current type: " (show-type bound)))
+            
+            [["lux;None" _]]
+            (return* (&/update$ "lux;types" (fn [ts] (&/update$ "lux;mappings" #(&/|put id (&/V "lux;Some" type) %)
+                                                               ts))
+                                state)
+                     nil)))
       (fail* (str "Unknown type-var: " id)))))
 
 ;; [Exports]
@@ -50,7 +59,7 @@
 
 (def fresh-lambda
   (|do [=arg fresh-var
-         =return fresh-var]
+        =return fresh-var]
     (return (&/V "lux;LambdaT" (&/T =arg =return)))))
 
 (defn clean [tvar type]
@@ -59,19 +68,18 @@
     (matchv ::M/objects [type]
       [["lux;VarT" ?id]]
       (if (= ?tid ?id)
-        (&/try-all% (&/|list (|do [=type (deref ?id)]
-                               (clean tvar =type))
-                             (return type)))
+        (|do [=type (deref ?id)]
+          (clean tvar =type))
         (return type))
       
       [["lux;LambdaT" [?arg ?return]]]
       (|do [=arg (clean tvar ?arg)
-             =return (clean tvar ?return)]
+            =return (clean tvar ?return)]
         (return (&/V "lux;LambdaT" (&/T =arg =return))))
 
       [["lux;AppT" [?lambda ?param]]]
       (|do [=lambda (clean tvar ?lambda)
-             =param (clean tvar ?param)]
+            =param (clean tvar ?param)]
         (return (&/V "lux;AppT" (&/T =lambda =param))))
 
       [["lux;TupleT" ?members]]
@@ -80,23 +88,23 @@
       
       [["lux;VariantT" ?members]]
       (|do [=members (&/map% (fn [[k v]]
-                                (|do [=v (clean tvar v)]
-                                  (return (&/T k =v))))
-                              ?members)]
+                               (|do [=v (clean tvar v)]
+                                 (return (&/T k =v))))
+                             ?members)]
         (return (&/V "lux;VariantT" =members)))
 
       [["lux;RecordT" ?members]]
       (|do [=members (&/map% (fn [[k v]]
-                                (|do [=v (clean tvar v)]
-                                  (return (&/T k =v))))
-                              ?members)]
+                               (|do [=v (clean tvar v)]
+                                 (return (&/T k =v))))
+                             ?members)]
         (return (&/V "lux;RecordT" =members)))
 
       [["lux;AllT" [?env ?name ?arg ?body]]]
       (|do [=env (&/map% (fn [[k v]]
-                            (|do [=v (clean tvar v)]
-                              (return (&/T k =v))))
-                          ?env)]
+                           (|do [=v (clean tvar v)]
+                             (return (&/T k =v))))
+                         ?env)]
         (return (&/V "lux;AllT" (&/T =env ?name ?arg ?body))))
 
       [_]
@@ -112,8 +120,8 @@
     [["lux;NothingT" _]]
     "Nothing"
 
-    [["lux;DataT" [name params]]]
-    (str "(^ " name " [" (->> params (&/|map show-type) (&/|interpose " ") (&/fold str "")) "])")
+    [["lux;DataT" name]]
+    (str "(^ " name ")")
     
     [["lux;TupleT" elems]]
     (if (&/|empty? elems)
@@ -166,10 +174,8 @@
     [["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;DataT" xname] ["lux;DataT" yname]]
+    (= xname yname)
 
     [["lux;TupleT" xelems] ["lux;TupleT" yelems]]
     (&/fold (fn [old xy] (and old (type= (aget xy 0) (aget xy 1))))
@@ -261,9 +267,6 @@
     [["lux;TupleT" ?members]]
     (&/V "lux;TupleT" (&/|map (partial beta-reduce env) ?members))
 
-    [["lux;DataT" [?name ?params]]]
-    (&/V "lux;DataT" (&/T ?name (&/|map (partial beta-reduce env) ?params)))
-
     [["lux;AppT" [?type-fn ?type-arg]]]
     (&/V "lux;AppT" (&/T (beta-reduce env ?type-fn) (beta-reduce env ?type-arg)))
 
@@ -316,28 +319,40 @@
   ;; (prn 'check* (show-type expected) (show-type actual))
   (matchv ::M/objects [expected actual]
     [["lux;AnyT" _] _]
-    success
+    (return (&/T fixpoints nil))
 
     [_ ["lux;NothingT" _]]
-    success
-
+    (return (&/T fixpoints nil))
+
+    [["lux;VarT" ?eid] ["lux;VarT" ?aid]]
+    (if (= ?eid ?aid)
+      (return (&/T fixpoints nil))
+      (&/try-all% (&/|list (|do [ebound (deref ?eid)]
+                             (check* fixpoints ebound actual))
+                           (|do [abound (deref ?aid)]
+                             (check* fixpoints expected abound))
+                           (|do [_ (set-var ?eid actual)]
+                             (return (&/T fixpoints nil))))))
+    
     [["lux;VarT" ?id] _]
-    (&/try-all% (&/|list (|do [bound (deref ?id)]
-                           (check* fixpoints bound actual))
-                         (reset ?id actual)))
+    (&/try-all% (&/|list (|do [_ (set-var ?id actual)]
+                           (return (&/T fixpoints nil)))
+                         (|do [bound (deref ?id)]
+                           (check* fixpoints bound actual))))
     
     [_ ["lux;VarT" ?id]]
-    (&/try-all% (&/|list (|do [bound (deref ?id)]
-                           (check* fixpoints expected bound))
-                         (reset ?id expected)))
+    (&/try-all% (&/|list (|do [_ (set-var ?id expected)]
+                           (return (&/T fixpoints nil)))
+                         (|do [bound (deref ?id)]
+                           (check* fixpoints expected bound))))
 
     [["lux;AppT" [F A]] _]
     (|do [expected* (apply-type F A)
-           :let [fp-pair (&/T expected actual)]]
+          :let [fp-pair (&/T expected actual)]]
       (matchv ::M/objects [(fp-get fp-pair fixpoints)]
         [["lux;Some" ?]]
         (if ?
-          success
+          (return (&/T fixpoints nil))
           (fail (check-error expected actual)))
 
         [["lux;None" _]]
@@ -349,68 +364,72 @@
 
     [["lux;AllT" _] _]
     (|do [$var fresh-var
-           expected* (apply-type expected $var)]
+          expected* (apply-type expected $var)]
       (check* fixpoints expected* actual))
 
     [_ ["lux;AllT" _]]
     (|do [$var fresh-var
-           actual* (apply-type actual $var)]
+          actual* (apply-type actual $var)]
       (check* 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
-          (|do [_ (&/map% (fn [ea]
-                             (|let [[e a] ea]
-                               (check* fixpoints e a)))
-                           (&/zip2 e!params a!params))]
-            success))
+    [["lux;DataT" e!name] ["lux;DataT" a!name]]
+    (if (= e!name a!name)
+      (return (&/T fixpoints nil))
+      (fail (str "[Type Error] Names don't match: " e!name " & " a!name)))
 
     [["lux;LambdaT" [eI eO]] ["lux;LambdaT" [aI aO]]]
-    (|do [_ (check* fixpoints aI eI)]
-      (check* fixpoints eO aO))
+    (|do [[fixpoints* _] (check* fixpoints aI eI)]
+      (check* fixpoints* eO aO))
 
     [["lux;TupleT" e!members] ["lux;TupleT" a!members]]
-    (if (= (&/|length e!members) (&/|length a!members))
-      (|do [_ (&/map% (fn [ea]
-                         (|let [[e a] ea]
-                           (do ;; (prn "lux;TupleT" 'ITER (show-type e) (show-type a))
-                               (check* 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.")))
+    (do (do (prn 'e!members (&/|length e!members))
+          (prn 'a!members (&/|length a!members)))
+      (if (= (&/|length e!members) (&/|length a!members))
+        (|do [fixpoints* (&/fold% (fn [fixp ea]
+                                    (|let [[e a] ea]
+                                      (do ;; (prn "lux;TupleT" 'ITER (show-type e) (show-type a))
+                                          (|do [[fixp* _] (check* fixp e a)]
+                                            (return fixp*)))))
+                                  fixpoints
+                                  (&/zip2 e!members a!members))
+              ;; :let [_ (prn "lux;TupleT" 'DONE)]
+              ]
+          (return (&/T fixpoints* nil)))
+        (do ;; (prn "lux;TupleT" (&/|length e!members) (&/|length a!members))
+            ;; (prn "lux;TupleT"
+            ;;      (&/fold str "" (&/|interpose " " (&/|map show-type e!members)))
+            ;;      (&/fold str "" (&/|interpose " " (&/|map show-type a!members))))
+            ;; (prn "lux;TupleT#fail" (fail "[Type Error] Tuples don't match in size."))
+            (fail "[Type Error] Tuples don't match in size."))))
     
     [["lux;VariantT" e!cases] ["lux;VariantT" a!cases]]
-    (|do [_ (&/map% (fn [kv]
-                       (|let [[k av] kv]
-                         (if-let [ev (&/|get k e!cases)]
-                           (check* fixpoints ev av)
-                           (fail (str "[Type Error] The expected variant cannot handle case: #" k)))))
-                     a!cases)]
-      success)
+    (if (= (&/|length e!cases) (&/|length a!cases))
+      (|do [fixpoints* (&/fold% (fn [fixp slot]
+                                  (prn "lux;VariantT" slot)
+                                  (if-let [e!type (&/|get slot e!cases)]
+                                    (if-let [a!type (&/|get slot a!cases)]
+                                      (|do [[fixp* _] (check* fixp e!type a!type)]
+                                        (return fixp*))
+                                      (fail (check-error expected actual)))
+                                    (fail (check-error expected actual))))
+                                fixpoints
+                                (&/|keys e!cases))]
+        (return (&/T fixpoints* nil)))
+      (fail "[Type Error] Variants don't match in size."))
 
     [["lux;RecordT" e!fields] ["lux;RecordT" a!fields]]
     (if (= (&/|length e!fields) (&/|length a!fields))
-      (|do [_ (&/map% (fn [slot]
-                         (if-let [e!type (&/|get e!fields slot)]
-                           (if-let [a!type (&/|get a!fields slot)]
-                             (check* fixpoints e!type a!type)
-                             (fail (check-error expected actual)))
-                           (fail (check-error expected actual))))
-                       (&/|keys e!fields))]
-        success)
+      (|do [fixpoints* (&/fold% (fn [fixp slot]
+                                  (prn "lux;RecordT" slot)
+                                  (if-let [e!type (&/|get slot e!fields)]
+                                    (if-let [a!type (&/|get slot a!fields)]
+                                      (|do [[fixp* _] (check* fixp e!type a!type)]
+                                        (return fixp*))
+                                      (fail (check-error expected actual)))
+                                    (fail (check-error expected actual))))
+                                fixpoints
+                                (&/|keys e!fields))]
+        (return (&/T fixpoints* nil)))
       (fail "[Type Error] Records don't match in size."))
 
     [_ _]
@@ -426,7 +445,9 @@
     ;; ...
     ))
 
-(def check (partial check* init-fixpoints))
+(defn check [expected actual]
+  (|do [_ (check* init-fixpoints expected actual)]
+    (return nil)))
 
 (defn apply-lambda [func param]
   (matchv ::M/objects [func]
@@ -436,20 +457,30 @@
 
     [["lux;AllT" [local-env local-name local-arg local-def]]]
     (|do [$var fresh-var
-           func* (apply-type func $var)]
+          func* (apply-type func $var)]
       (apply-lambda func* param))
 
     [_]
     (fail (str "[Type System] Can't apply type " (show-type func) " to type " (show-type param)))
     ))
 
+(defn actual-type [type]
+  (matchv ::M/objects [type]
+    [["lux;AppT" [?all ?param]]]
+    (|do [type* (apply-type ?all ?param)]
+      (actual-type type*))
+
+    [_]
+    (return type)
+    ))
+
 (def Any (&/V "lux;AnyT" nil))
 (def Nothing (&/V "lux;NothingT" nil))
-(def Bool (&/V "lux;DataT" (&/T "java.lang.Boolean" (&/|list))))
-(def Int (&/V "lux;DataT" (&/T "java.lang.Long" (&/|list))))
-(def Real (&/V "lux;DataT" (&/T "java.lang.Double" (&/|list))))
-(def Char (&/V "lux;DataT" (&/T "java.lang.Character" (&/|list))))
-(def Text (&/V "lux;DataT" (&/T "java.lang.String" (&/|list))))
+(def Bool (&/V "lux;DataT" "java.lang.Boolean"))
+(def Int (&/V "lux;DataT" "java.lang.Long"))
+(def Real (&/V "lux;DataT" "java.lang.Double"))
+(def Char (&/V "lux;DataT" "java.lang.Character"))
+(def Text (&/V "lux;DataT" "java.lang.String"))
 (def Unit (&/V "lux;TupleT" (&/|list)))
 
 (def List
@@ -460,16 +491,15 @@
                                                                                                                     (&/V "lux;BoundT" "a")))))))))))
 
 (def Type
-  (let [Type (&/V "lux;AppT" (&/T (&/V "lux;BoundT" "Type") (&/V "lux;BoundT" "")))
+  (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;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;DataT" Text)
+                                                                           (&/T "lux;TupleT" (&/V "lux;AppT" (&/T List Type)))
                                                                            (&/T "lux;VariantT" TypeEnv)
                                                                            (&/T "lux;RecordT" TypeEnv)
                                                                            (&/T "lux;LambdaT" TypePair)
@@ -479,94 +509,3 @@
                                                                            (&/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;DataT" [xname xparams]] ["lux;DataT" [yname yparams]]]
-      (if (and (= xname yname)
-               (= (&/|length xparams) (&/|length yparams)))
-        (fail (str "[Type System Error] Can't merge types: " (show-type x) " and " (show-type y)))
-        (|do [xyparams (&/map% (fn [xy]
-                                 (|let [[xp yp] xy]
-                                   (merge xp yp)))
-                               (&/zip2 xparams yparams))]
-          (return (&/V "lux;DataT" (&/T xname xyparams)))))
-
-      [["lux;TupleT" xmembers] ["lux;TupleT" ymembers]]
-      (if (= (&/|length xmembers) (&/|length ymembers))
-        (fail (str "[Type System Error] Can't merge types: " (show-type x) " and " (show-type y)))
-        (|do [xymembers (&/map% (fn [xy]
-                                  (|let [[xp yp] xy]
-                                    (merge xp yp)))
-                                (&/zip2 xmembers ymembers))]
-          (return (&/V "lux;TupleT" xymembers))))
-
-      [["lux;VariantT" x!cases] ["lux;VariantT" y!cases]]
-      (|do [cases (&/fold% (fn [cases kv]
-                             (matchv ::M/objects [kv]
-                               [[k v]]
-                               (if-let [cv (&/|get k cases)]
-                                 (|do [v* (merge cv v)]
-                                   (return (&/|put k v* 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))
-        (|do [fields (&/fold% (fn [fields kv]
-                                (matchv ::M/objects [kv]
-                                  [[k v]]
-                                  (if-let [cv (&/|get k fields)]
-                                    (|do [v* (merge cv v)]
-                                      (return (&/|put k v* 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))))
-
-      [["lux;LambdaT" [xinput xoutput]] ["lux;LambdaT" [yinput youtput]]]
-      (|do [xyinput (check xinput yinput)
-            xyoutput (check xoutput youtput)]
-        (return (&/V "lux;LambdaT" (&/T xyinput xyoutput))))
-      
-      [_ _]
-      (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 [((check Type RealT)
-                        (&/init-state nil))]
-    [["lux;Left" ?msg]]
-    (assert false ?msg)
-
-    [_]
-    (println "YEAH!"))
-
-  (matchv ::M/objects [((check List (&/V "lux;AppT" (&/T List Real)))
-                        (&/init-state nil))]
-    [["lux;Left" ?msg]]
-    (assert false ?msg)
-
-    [_]
-    (println "YEAH!"))
-  )