- Solved the bug wherein type-inferencing was causing computational complexity to explode and cause the compiler to become very slow (solved it by removing type-inference from tuples).

- Also removed type-inference from functions/lambdas.
- Added a small optimization to improve the efficiency of type-checking by not doing a thorough type-check when a global or local binding has a type variant with the same cases as Type, and it's exo-type is also like this (hopefully, it will never happen that someone will exploit this to make the compiler do something weird...)

4 files changed, 298 insertions, 322 deletions

diff --git a/source/lux.lux b/source/lux.lux
index 84eaab689..a08c88db7 100644
--- a/source/lux.lux
+++ b/source/lux.lux
@@ -74,215 +74,195 @@
                                                                                                                                    #Nil])])])])])])])])])])]))])
                         #NothingT]))))
 
-## (def' Type
-##   (case' (#AppT [(#BoundT "Type") (#BoundT "")])
-##          Type
-##          (case' (#AppT [List (#TupleT (#Cons [Text (#Cons [Type #Nil])]))])
-##                 TypeEnv
-##                 (#AppT [(#AllT [#Nil "Type" ""
-##                                 (#VariantT (#Cons [["lux;AnyT" (#TupleT #Nil)]
-##                                                    (#Cons [["lux;NothingT" (#TupleT #Nil)]
-##                                                            (#Cons [["lux;DataT" Text]
-##                                                                    (#Cons [["lux;TupleT" (#AppT [List (#AppT [(#BoundT "Type") (#BoundT "")])])]
-##                                                                            (#Cons [["lux;VariantT" TypeEnv]
-##                                                                                    (#Cons [["lux;RecordT" TypeEnv]
-##                                                                                            (#Cons [["lux;LambdaT" (#TupleT (#Cons [Type (#Cons [Type #Nil])]))]
-##                                                                                                    (#Cons [["lux;BoundT" Text]
-##                                                                                                            (#Cons [["lux;VarT" Int]
-##                                                                                                                    (#Cons [["lux;AllT" (#TupleT (#Cons [TypeEnv (#Cons [Text (#Cons [Text (#Cons [Type #Nil])])])]))]
-##                                                                                                                            (#Cons [["lux;AppT" (#TupleT (#Cons [Type (#Cons [Type #Nil])]))]
-##                                                                                                                                    #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 (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 #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" ""
-##                                 (#AppT [(#AppT [Meta Cursor])
-##                                         (#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 (Maybe a)
+##   (| #None
+##      (#Some a)))
+(def' Maybe
+  (check' Type
+          (#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
+  (check' Type
+          (#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
+  (check' Type
+          (#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
+  (check' Type
+          (#TupleT (#Cons [Text (#Cons [Int (#Cons [Int #Nil])])]))))
+
+## (deftype (Meta m v)
+##   (| (#Meta (, m v))))
+(def' Meta
+  (check' Type
+          (#AllT [#Nil "Meta" "m"
+                  (#AllT [#Nil "" "v"
+                          (#VariantT (#Cons [["lux;Meta" (#TupleT (#Cons [(#BoundT "m")
+                                                                          (#Cons [(#BoundT "v")
+                                                                                  #Nil])]))]
+                                             #Nil]))])])))
 
-## ## ## (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 Macro
-## ## ##   (-> (List Syntax) Compiler_State
-## ## ##       (Either Text [Compiler_State (List Syntax)])))
-## ## (def' Macro
-## ##   (case' (#AppT [List Syntax])
-## ##          SyntaxList
-## ##          (#LambdaT [SyntaxList
-## ##                     (#LambdaT [Compiler_State
-## ##                                (#AppT [(#AppT [Either Text])
-## ##                                        (#TupleT (#Cons [Compiler_State
-## ##                                                         (#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'
-## ##   (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
-## ## ## ##       (-> 21268
-## ## ## ##           (All  21267
-## ## ## ##                 (-> 21267
-## ## ## ##                     (| (#lux;Right (, 21267
-## ## ## ##                                       (| (#lux;Cons (, (((All Meta m (All  v (| (#lux;Meta (, m v)))))
-## ## ## ##                                                          (, (^ java.lang.String []) (^ java.lang.Long []) (^ java.lang.Long [])))
-## ## ## ##                                                         ⌈17⌋)
-## ## ## ##                                                        (| (#lux;Nil (, )))))))))))))
+## (def' Reader
+##   (List (Meta Cursor Text)))
+(def' Reader
+  (check' Type
+          (#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
+  (check' Type
+          (#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 #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
+  (check' Type
+          (case' (#AppT [(#BoundT "Syntax") (#BoundT "")])
+                 Syntax
+                 (case' (#AppT [List Syntax])
+                        SyntaxList
+                        (#AppT [(#AllT [#Nil "Syntax" ""
+                                        (#AppT [(#AppT [Meta Cursor])
+                                                (#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
+  (check' Type
+          (#AllT [#Nil "_" "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
+  (check' Type
+          (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'
+##   (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')
 
 ## ## ## (def' lambda
 ## ## ##   (check' Macro
diff --git a/src/lux.clj b/src/lux.clj
index e035e92c8..103c15565 100644
--- a/src/lux.clj
+++ b/src/lux.clj
@@ -16,7 +16,6 @@
 
   ;; TODO: Change &type/check to it returns a tuple with the new expected & actual types
   ;; TODO: Stop passing-along the exo-types and instead pass-along endo-types where possible
-  ;; TODO: Optimize analyser to avoid redundant checks when dealing with type-checking (making sure check* is being handed a type)
   
   (time (&compiler/compile-all (&/|list "lux")))
   (System/gc)
diff --git a/src/lux/analyser/lux.clj b/src/lux/analyser/lux.clj
index 8e3afb476..1abc0bcea 100644
--- a/src/lux/analyser/lux.clj
+++ b/src/lux/analyser/lux.clj
@@ -26,56 +26,50 @@
 
 ;; [Exports]
 (defn analyse-tuple [analyse exo-type ?elems]
+  ;; (prn "^^ analyse-tuple ^^")
   ;; (prn 'analyse-tuple (str "[" (->> ?elems (&/|map &/show-ast) (&/|interpose " ") (&/fold str "")) "]")
   ;;      (&type/show-type exo-type))
-  (&type/with-vars (&/|length ?elems)
-    (fn [=vars]
-      (|do [_ (&type/check exo-type (&/V "lux;TupleT" =vars))
-            =elems (&/map% (fn [ve]
-                             (|let [[=var elem] ve]
-                               (|do [output (&&/analyse-1 analyse =var elem)]
-                                 (matchv ::M/objects [output]
-                                   [["Expression" [?val ?type]]]
-                                   (|do [=type (&type/clean =var ?type)]
-                                     (return (&/V "Expression" (&/T ?val =type))))))))
-                           (&/zip2 =vars ?elems))]
-        (return (&/|list (&/V "Expression" (&/T (&/V "tuple" =elems)
-                                                exo-type))))))))
+  (|do [t-members (matchv ::M/objects [exo-type]
+                    [["lux;TupleT" ?members]]
+                    (return ?members)
+
+                    [_]
+                    (fail "[Analyser Error] Tuple requires tuple-type."))
+        =elems (&/map% (fn [ve]
+                         (|let [[elem-t elem] ve]
+                           (&&/analyse-1 analyse elem-t elem)))
+                       (&/zip2 t-members ?elems))]
+    (return (&/|list (&/V "Expression" (&/T (&/V "tuple" =elems)
+                                            exo-type))))))
 
 (defn analyse-variant [analyse exo-type ident ?value]
-  (|let [[?module ?name] ident]
-    (do ;; (prn 'analyse-variant (str ?module ";" ?name) (&/show-ast ?value))
-      (|do [;; :let [_ (prn 'analyse-variant/exo-type (&type/show-type exo-type))]
-            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))))
+  ;; (prn "^^ analyse-variant ^^")
+  (|do [;; :let [_ (prn 'analyse-variant/exo-type (&type/show-type exo-type))]
+        ?tag (&&/resolved-ident ident)
+        exo-type* (matchv ::M/objects [exo-type]
+                    [["lux;VarT" ?id]]
+                    (&/try-all% (&/|list (|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 'analyse-variant/exo-type* (&type/show-type exo-type*))]
-            ]
-        (matchv ::M/objects [exo-type*]
-          [["lux;VariantT" ?cases]]
-          (if-let [vtype (&/|get ?tag ?cases)]
-            (|do [;; :let [_ (prn 'VARIANT_BODY ?tag (&/show-ast ?value) (&type/show-type vtype))]
-                  =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*))))
+                    [_]
+                    (&type/actual-type exo-type))
+        ;; :let [_ (prn 'analyse-variant/exo-type* (&type/show-type exo-type*))]
+        ]
+    (matchv ::M/objects [exo-type*]
+      [["lux;VariantT" ?cases]]
+      (if-let [vtype (&/|get ?tag ?cases)]
+        (|do [;; :let [_ (prn 'VARIANT_BODY ?tag (&/show-ast ?value) (&type/show-type vtype))]
+              =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*))))))))
+      [_]
+      (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]
@@ -102,6 +96,18 @@
                  &/|keys &/->seq (interpose " ") (reduce str ""))
        "}}"))
 
+(defn ^:private type-test [exo-type binding]
+  (|do [btype (&&/expr-type binding)
+        o?? (&type/is-Type? exo-type)]
+    (if o??
+      (|do [i?? (&type/is-Type? btype)]
+        (if i??
+          (do (println "FOUND TWO TYPES!")
+            (return (&/|list binding)))
+          (fail "[Type Error] Types don't match.")))
+      (|do [_ (&type/check exo-type btype)]
+        (return (&/|list binding))))))
+
 (defn analyse-symbol [analyse exo-type ident]
   (|do [module-name &/get-module-name]
     (fn [state]
@@ -115,9 +121,10 @@
         (matchv ::M/objects [outer]
           [["lux;Nil" _]]
           (if-let [global (->> state (&/get$ "lux;global-env") &/from-some (&/get$ "lux;locals") (&/get$ "lux;mappings") (&/|get global-ident))]
-            (&/run-state (|do [=global-type (&&/expr-type global)
-                               _ (&type/check exo-type =global-type)]
-                           (return (&/|list global)))
+            (&/run-state (type-test exo-type global)
+                         ;; (|do [btype (&&/expr-type global)
+                         ;;       _ (&type/check exo-type btype)]
+                         ;;   (return (&/|list global)))
                          state)
             (do (prn (str "((" (->> stack (&/|map show-frame) &/->seq (interpose " ") (reduce str "")) "))"))
               (fail* (str "[Analyser Error] Unrecognized identifier: " local-ident))))
@@ -135,9 +142,10 @@
                                                   (->> top-outer (&/get$ "lux;closure") (&/get$ "lux;mappings") (&/|get local-ident)))
                                               (&/|list))
                                          (&/zip2 (&/|reverse inner) scopes))]
-            (&/run-state (|do [=local-type (&&/expr-type =local)
-                               _ (&type/check exo-type =local-type)]
-                           (return (&/|list =local)))
+            (&/run-state (type-test exo-type =local)
+                         ;; (|do [btype (&&/expr-type =local)
+                         ;;       _ (&type/check exo-type btype)]
+                         ;;   (return (&/|list =local)))
                          (&/set$ "lux;local-envs" (&/|++ inner* outer) state)))
           )))
     ))
@@ -201,44 +209,15 @@
 
 (defn analyse-lambda* [analyse exo-type ?self ?arg ?body]
   ;; (prn 'analyse-lambda ?self ?arg ?body)
-  (|do [lambda-expr (&type/with-vars 2
-                 (fn [=vars2]
-                   (matchv ::M/objects [=vars2]
-                     [["lux;Cons" [=arg ["lux;Cons" [=return ["lux;Nil" _]]]]]]
-                     (|do [:let [_ (prn 'analyse-lambda/_-1 (&type/show-type =arg) (&type/show-type =return))]
-                           :let [=lambda-type* (&/V "lux;LambdaT" (&/T =arg =return))]
-                           :let [_ (prn 'analyse-lambda/_0)]
-                           _ (&type/check exo-type =lambda-type*)
-                           :let [_ (prn 'analyse-lambda/_0.5 (&type/show-type exo-type))]
-                           :let [_ (prn 'analyse-lambda/_1 (&type/show-type =lambda-type*))]
-                           ;; _ (|do [aid (&type/var-id =arg)
-                           ;;         atype (&type/deref aid)
-                           ;;         rid (&type/var-id =return)
-                           ;;         rtype (&type/deref rid)
-                           ;;         :let [_ (prn 'analyse-lambda/_1.5 (&type/show-type atype) (&type/show-type rtype))]]
-                           ;;     (return nil))
-                           [=scope =captured =body] (&&lambda/with-lambda ?self =lambda-type*
-                                                      ?arg =arg
-                                                      (&&/analyse-1 analyse =return ?body))
-                           =lambda-type** (&type/clean =return =lambda-type*)
-                           :let [_ (prn 'analyse-lambda/_2)]
-                           =lambda-type (matchv ::M/objects [=arg]
-                                          [["lux;VarT" ?id]]
-                                          (|do [? (&type/bound? ?id)]
-                                            (if ?
-                                              (&type/clean =arg =lambda-type**)
-                                              (let [var-name (str (gensym ""))]
-                                                (|do [_ (&type/set-var ?id (&/V "lux;BoundT" var-name))
-                                                      =lambda-type*** (&type/clean =arg =lambda-type**)]
-                                                  (return (&/V "lux;AllT" (&/T (&/|list) "" var-name =lambda-type***)))))))
-
-                                          [_]
-                                          (fail ""))
-                           :let [_ (prn 'analyse-lambda/_3 (&type/show-type =lambda-type))]]
-                       (return (&/V "Expression" (&/T (&/V "lambda" (&/T =scope =captured =body)) =lambda-type))))
-                     )))
-        :let [_ (prn 'analyse-lambda/_4)]]
-    (return lambda-expr)))
+  (matchv ::M/objects [exo-type]
+    [["lux;LambdaT" [?arg-t ?return-t]]]
+    (|do [[=scope =captured =body] (&&lambda/with-lambda ?self exo-type
+                                     ?arg ?arg-t
+                                     (&&/analyse-1 analyse ?return-t ?body))]
+      (return (&/V "Expression" (&/T (&/V "lambda" (&/T =scope =captured =body)) exo-type))))
+    
+    [_]
+    (fail "[Analyser Error] Functions require function types.")))
 
 (defn analyse-lambda** [analyse exo-type ?self ?arg ?body]
   (prn 'analyse-lambda**/&& (aget exo-type 0))
@@ -248,10 +227,12 @@
       (fn [$var]
         (|do [exo-type* (&type/apply-type exo-type $var)
               output (analyse-lambda** analyse exo-type* ?self ?arg ?body)]
-          (matchv ::M/objects [output]
-            [["Expression" [?item ?type]]]
-            (|do [=type (&type/clean $var ?type)]
-              (return (&/V "Expression" (&/T ?item =type))))))))
+          (matchv ::M/objects [$var]
+            [["lux;VarT" ?id]]
+            (|do [? (&type/bound? ?id)]
+              (if ?
+                (fail "[Analyser Error] Can't use type-var in any type-specific way inside polymorphic functions.")
+                (return output)))))))
     
     [_]
     (analyse-lambda* analyse exo-type ?self ?arg ?body)))
@@ -267,15 +248,16 @@
         ? (&&def/defined? module-name ?name)]
     (if ?
       (fail (str "[Analyser Error] Can't redefine " ?name))
-      (|do [:let [_ (prn 'analyse-def/_0)]
+      (|do [;; :let [_ (prn 'analyse-def/_0)]
             =value (&/with-scope ?name
                      (analyse-1+ analyse ?value))
-            :let [_ (prn 'analyse-def/_1)]
+            ;; :let [_ (prn 'analyse-def/_1)]
             =value-type (&&/expr-type =value)
-            :let [_ (prn 'analyse-def/_2)]
-            ;; :let [_ (prn 'analyse-def/TYPE ?name (&type/show-type =value-type))]
+            ;; :let [_ (prn 'analyse-def/_2)]
+            :let [_ (prn 'analyse-def/TYPE ?name (&type/show-type =value-type))]
             _ (&&def/define module-name ?name =value-type)
-            :let [_ (prn 'analyse-def/_3)]]
+            ;; :let [_ (prn 'analyse-def/_3)]
+            ]
         (return (&/|list (&/V "Statement" (&/V "def" (&/T ?name =value)))))))))
 
 (defn analyse-declare-macro [exo-type ident]
diff --git a/src/lux/type.clj b/src/lux/type.clj
index b17079bcc..ed5e2be24 100644
--- a/src/lux/type.clj
+++ b/src/lux/type.clj
@@ -98,8 +98,9 @@
   (fn [state]
     (prn 'delete-var id)
     (if-let [tvar (->> state (&/get$ "lux;types") (&/get$ "lux;mappings") (&/|get id))]
-      (return* (&/update$ "lux;types" (fn [ts] (&/update$ "lux;mappings" #(&/|remove id %)
-                                                         ts))
+      (return* (&/update$ "lux;types" #(->> %
+                                            ;; (&/update$ "lux;counter" dec)
+                                            (&/update$ "lux;mappings" (fn [ms] (&/|remove id ms))))
                           state)
                nil)
       (fail* (str "[Type Error] Unknown type-var: " id)))))
@@ -165,6 +166,7 @@
     ))
 
 (defn clean [tvar type]
+  ;; (prn "^^ clean ^^")
   (matchv ::M/objects [tvar]
     [["lux;VarT" ?id]]
     (clean* ?id type)
@@ -228,6 +230,7 @@
     ))
 
 (defn type= [x y]
+  ;; (prn "^^ type= ^^")
   (let [output (matchv ::M/objects [x y]
                  [["lux;AnyT" _] ["lux;AnyT" _]]
                  true
@@ -293,7 +296,7 @@
                         ))
 
                  [_ _]
-                 (do (prn 'type= (show-type x) (show-type y))
+                 (do ;; (prn 'type= (show-type x) (show-type y))
                    false)
                  )]
     ;; (prn 'type= output (show-type x) (show-type y))
@@ -384,6 +387,7 @@
 (def init-fixpoints (&/|list))
 
 (defn ^:private check* [fixpoints expected actual]
+  ;; (prn "^^ check* ^^")
   ;; (prn 'check* (aget expected 0) (aget actual 0))
   ;; (prn 'check* (show-type expected) (show-type actual))
   (matchv ::M/objects [expected actual]
@@ -417,7 +421,7 @@
 
     [["lux;AppT" [F A]] _]
     (let [fp-pair (&/T expected actual)
-          _ (prn 'LEFT_APP (&/|length fixpoints))
+          ;; _ (prn 'LEFT_APP (&/|length fixpoints))
           _ (when (> (&/|length fixpoints) 10)
               (println 'FIXPOINTS (->> (&/|keys fixpoints)
                                        (&/|map (fn [pair]
@@ -473,16 +477,6 @@
         (|do [actual* (apply-type actual $arg)]
           (check* fixpoints expected actual*))))
 
-    ;; [["lux;AllT" _] _]
-    ;; (|do [$arg create-var
-    ;;       expected* (apply-type expected $arg)]
-    ;;   (check* fixpoints expected* actual))
-
-    ;; [_ ["lux;AllT" _]]
-    ;; (|do [$arg create-var
-    ;;       actual* (apply-type actual $arg)]
-    ;;   (check* fixpoints expected actual*))
-
     [["lux;DataT" e!name] ["lux;DataT" a!name]]
     (if (= e!name a!name)
       (return (&/T fixpoints nil))
@@ -516,7 +510,7 @@
     [["lux;VariantT" e!cases] ["lux;VariantT" a!cases]]
     (if (= (&/|length e!cases) (&/|length a!cases))
       (|do [fixpoints* (&/fold% (fn [fixp slot]
-                                  (prn 'VARIANT_CASE slot)
+                                  ;; (prn 'VARIANT_CASE slot)
                                   (if-let [e!type (&/|get slot e!cases)]
                                     (if-let [a!type (&/|get slot a!cases)]
                                       (|do [[fixp* _] (check* fixp e!type a!type)]
@@ -531,7 +525,7 @@
     [["lux;RecordT" e!fields] ["lux;RecordT" a!fields]]
     (if (= (&/|length e!fields) (&/|length a!fields))
       (|do [fixpoints* (&/fold% (fn [fixp slot]
-                                  (prn 'RECORD_FIELD slot)
+                                  ;; (prn 'RECORD_FIELD slot)
                                   (if-let [e!type (&/|get slot e!fields)]
                                     (if-let [a!type (&/|get slot a!fields)]
                                       (|do [[fixp* _] (check* fixp e!type a!type)]
@@ -548,6 +542,7 @@
     ))
 
 (defn check [expected actual]
+  ;; (prn "^^ check ^^")
   (|do [_ (check* init-fixpoints expected actual)]
     (return nil)))
 
@@ -587,3 +582,23 @@
 
     [_]
     (fail (str "[Type Error] Type is not a variant: " (show-type type)))))
+
+(let [type-cases #{"lux;AnyT"   , "lux;NothingT", "lux;DataT"
+                   "lux;TupleT" , "lux;VariantT", "lux;RecordT"
+                   "lux;LambdaT", "lux;BoundT"  , "lux;VarT"
+                   "lux;AllT"   , "lux;AppT"}]
+  (defn is-Type? [type]
+    (matchv ::M/objects [type]
+      [["lux;VarT" ?id]]
+      (&/try-all% (&/|list (|do [type* (deref ?id)]
+                             (is-Type? type*))
+                           (return false)))
+
+      [_]
+      (|do [type* (actual-type type)]
+        (matchv ::M/objects [type*]
+          [["lux;VariantT" ?cases]]
+          (return (->> ?cases &/|keys &/->seq set (= type-cases)))
+
+          [_]
+          (return false))))))