- Identifiers with just a semi-colon in front now have "lux" as their module, instead of the local module. (e.g. ;map, #;Cons, ;All)

- The type-checker now takes into account 2 types: an exo-type (imposed by outside forces) and an endo-type (generated through inference)
- Fixed a few bugs in the analyser and the type-system.
- &type/solve* is now the actual type-checker and &type/solve invokes solve* with an empty fixpoint environment.
- The exo-type of Statements is Nothing.
- variants, tuples and def' are being analyzed properly now.

6 files changed, 189 insertions, 177 deletions

diff --git a/src/lux/analyser.clj b/src/lux/analyser.clj
index 9ed75b83d..80f2cd252 100644
--- a/src/lux/analyser.clj
+++ b/src/lux/analyser.clj
@@ -2,7 +2,7 @@
   (:require (clojure [template :refer [do-template]])
             [clojure.core.match :as M :refer [matchv]]
             clojure.core.match.array
-            (lux [base :as & :refer [exec return fail]]
+            (lux [base :as & :refer [exec return fail |list]]
                  [reader :as &reader]
                  [parser :as &parser]
                  [type :as &type]
@@ -15,19 +15,22 @@
 ;; [Utils]
 (defn ^:private parse-handler [[catch+ finally+] token]
   (matchv ::M/objects [token]
-    [["lux;Meta" [meta ["Form" ["Cons" [["lux;Meta" [_ ["Symbol" [_ "jvm-catch"]]]]
-                                        ["Cons" [["lux;Meta" [_ ["Symbol" [_ ?ex-class]]]]
-                                                 ["Cons" [["lux;Meta" [_ ["Symbol" [_ ?ex-arg]]]]
-                                                          ["Cons" [?catch-body
-                                                                   ["Nil" _]]]]]]]]]]]]]
-    [(concat catch+ (list [?ex-class ?ex-arg ?catch-body])) finally+]
-
-    [["lux;Meta" [meta ["Form" ["Cons" [["lux;Meta" [_ ["Symbol" [_ "jvm-finally"]]]]
-                                        ["Cons" [?finally-body
-                                                 ["Nil" _]]]]]]]]]
-    [catch+ ?finally-body]))
-
-(defn ^:private analyse-basic-ast [analyse eval! token]
+    [["lux;Meta" [meta ["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Symbol" [_ "jvm-catch"]]]]
+                                                ["lux;Cons" [["lux;Meta" [_ ["lux;Symbol" [_ ?ex-class]]]]
+                                                             ["lux;Cons" [["lux;Meta" [_ ["lux;Symbol" [_ ?ex-arg]]]]
+                                                                          ["lux;Cons" [?catch-body
+                                                                                       ["lux;Nil" _]]]]]]]]]]]]]
+    (&/T (&/|++ catch+ (|list (&/T ?ex-class ?ex-arg ?catch-body))) finally+)
+
+    [["lux;Meta" [meta ["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Symbol" [_ "jvm-finally"]]]]
+                                                ["lux;Cons" [?finally-body
+                                                             ["lux;Nil" _]]]]]]]]]
+    (&/T catch+ ?finally-body)))
+
+(defn ^:private _meta [token]
+  (&/V "lux;Meta" (&/T (&/T "" -1 -1) token)))
+
+(defn ^:private analyse-basic-ast [analyse eval! exo-type token]
   ;; (prn 'analyse-basic-ast (aget token 0))
   ;; (when (= "lux;Tag" (aget token 0))
   ;;   (prn 'analyse-basic-ast/tag (aget token 1)))
@@ -35,37 +38,34 @@
   (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" (&/V "lux;Nil" nil)))))))
+    (return (&/|list (&/V "Expression" (&/T (&/V "bool" ?value) (&/V "lux;DataT" (&/T "java.lang.Boolean" (|list)))))))
 
     [["lux;Meta" [meta ["lux;Int" ?value]]]]
-    (return (&/|list (&/V "Expression" (&/T (&/V "int" ?value)  (&/V "lux;DataT" (&/T "java.lang.Long" (&/V "lux;Nil" nil)))))))
+    (return (&/|list (&/V "Expression" (&/T (&/V "int" ?value)  (&/V "lux;DataT" (&/T "java.lang.Long" (|list)))))))
 
     [["lux;Meta" [meta ["lux;Real" ?value]]]]
-    (return (&/|list (&/V "Expression" (&/T (&/V "real" ?value) (&/V "lux;DataT" (&/T "java.lang.Double" (&/V "lux;Nil" nil)))))))
+    (return (&/|list (&/V "Expression" (&/T (&/V "real" ?value) (&/V "lux;DataT" (&/T "java.lang.Double" (|list)))))))
 
     [["lux;Meta" [meta ["lux;Char" ?value]]]]
-    (return (&/|list (&/V "Expression" (&/T (&/V "char" ?value) (&/V "lux;DataT" (&/T "java.lang.Character" (&/V "lux;Nil" nil)))))))
+    (return (&/|list (&/V "Expression" (&/T (&/V "char" ?value) (&/V "lux;DataT" (&/T "java.lang.Character" (|list)))))))
 
     [["lux;Meta" [meta ["lux;Text" ?value]]]]
-    (return (&/|list (&/V "Expression" (&/T (&/V "text" ?value) (&/V "lux;DataT" (&/T "java.lang.String" (&/V "lux;Nil" nil)))))))
+    (return (&/|list (&/V "Expression" (&/T (&/V "text" ?value) (&/V "lux;DataT" (&/T "java.lang.String" (|list)))))))
 
     [["lux;Meta" [meta ["lux;Tuple" ?elems]]]]
-    (&&lux/analyse-tuple analyse ?elems)
+    (&&lux/analyse-tuple analyse exo-type ?elems)
 
     [["lux;Meta" [meta ["lux;Record" ?elems]]]]
     (&&lux/analyse-record analyse ?elems)
 
-    [["lux;Meta" [meta ["lux;Tag" [?module ?name]]]]]
-    (let [tuple-type (&/V "lux;TupleT" (&/V "lux;Nil" nil))
-          ?tag (str ?module ";" ?name)]
-      (return (&/|list (&/V "Expression" (&/T (&/V "variant" (&/T ?tag (&/V "Expression" (&/T (&/V "tuple" (&/|list)) tuple-type))))
-                                              (&/V "lux;VariantT" (&/V "lux;Cons" (&/T (&/T ?tag tuple-type) (&/V "lux;Nil" nil)))))))))
-
+    [["lux;Meta" [meta ["lux;Tag" ?ident]]]]
+    (&&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" (&/V "lux;Nil" nil)))))))
+    (return (&/|list (&/V "Expression" (&/T (&/V "jvm-null" nil) (&/V "lux;DataT" (&/T "null" (|list)))))))
     
     [["lux;Meta" [meta ["lux;Symbol" ?ident]]]]
-    (&&lux/analyse-ident analyse ?ident)
+    (&&lux/analyse-symbol analyse exo-type ?ident)
 
     [["lux;Meta" [meta ["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Symbol" [_ "case'"]]]]
                                                 ["lux;Cons" [?variant ?branches]]]]]]]]
@@ -76,7 +76,7 @@
                                                              ["lux;Cons" [["lux;Meta" [_ ["lux;Symbol" [_ ?arg]]]]
                                                                           ["lux;Cons" [?body
                                                                                        ["lux;Nil" _]]]]]]]]]]]]]
-    (&&lux/analyse-lambda analyse ?self ?arg ?body)
+    (&&lux/analyse-lambda analyse exo-type ?self ?arg ?body)
 
     [["lux;Meta" [meta ["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Symbol" [_ "def'"]]]]
                                                 ["lux;Cons" [["lux;Meta" [_ ["lux;Symbol" [_ ?name]]]]
@@ -84,7 +84,7 @@
                                                                           ["lux;Nil" _]]]]]]]]]]]
     (do ;; (when (= "if" ?name)
         ;;   (prn "if" (&/show-ast ?value)))
-        (&&lux/analyse-def analyse ?name ?value))
+        (&&lux/analyse-def analyse exo-type ?name ?value))
 
     [["lux;Meta" [meta ["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Symbol" [_ "declare-macro'"]]]]
                                                 ["lux;Cons" [["lux;Meta" [_ ["lux;Symbol" ?ident]]]
@@ -100,7 +100,7 @@
                                                 ["lux;Cons" [?type
                                                              ["lux;Cons" [?value
                                                                           ["lux;Nil" _]]]]]]]]]]]
-    (&&lux/analyse-check analyse eval! ?type ?value)
+    (&&lux/analyse-check analyse eval! exo-type ?type ?value)
 
     [["lux;Meta" [meta ["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Symbol" [_ "coerce'"]]]]
                                                 ["lux;Cons" [?type
@@ -421,34 +421,28 @@
     [_]
     (fail (str "[Analyser Error] Unmatched token: " (&/show-ast token)))))
 
-(defn ^:private analyse-ast [eval!]
-  (fn [token]
-    ;; (prn 'analyse-ast token)
-    (matchv ::M/objects [token]
-      [["lux;Meta" [meta ["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Tag" [?module ?name]]]] ?values]]]]]]
-      (exec [;; :let [_ (prn 'PRE-ASSERT)]
-             :let [?tag (str ?module ";" ?name)]
-             :let [_ (assert (= 1 (&/|length ?values)) (str "[Analyser Error] Can only tag 1 value: " (pr-str token)))]
-             ;; :let [_ (prn 'POST-ASSERT)]
-             =value (&&/analyse-1 (analyse-ast eval!) (&/|head ?values))
-             =value-type (&&/expr-type =value)]
-        (return (&/|list (&/V "Expression" (&/T (&/V "variant" (&/T ?tag =value)) (&/V "lux;VariantT" (&/V "lux;Cons" (&/T (&/T ?tag =value-type) (&/V "lux;Nil" nil)))))))))
-      
-      [["lux;Meta" [meta ["lux;Form" ["lux;Cons" [?fn ?args]]]]]]
-      (fn [state]
-        ;; (prn '(&/show-ast ?fn) (&/show-ast ?fn))
-        (matchv ::M/objects [((&&/analyse-1 (analyse-ast eval!) ?fn) state)]
-          [["lux;Right" [state* =fn]]]
-          ((&&lux/analyse-apply (analyse-ast eval!) =fn ?args) state*)
-
-          [_]
-          (do ;; (prn 'analyse-ast/token (aget token 0) (&/show-state state))
-              ((analyse-basic-ast (analyse-ast eval!) eval! token) state))))
-      
-      [_]
-      (analyse-basic-ast (analyse-ast eval!) eval! token))))
+(defn ^:private analyse-ast [eval! exo-type token]
+  ;; (prn 'analyse-ast token)
+  (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.")
+      (&&lux/analyse-variant (partial analyse-ast eval!) exo-type ?ident (&/|head ?values)))
+    
+    [["lux;Meta" [meta ["lux;Form" ["lux;Cons" [?fn ?args]]]]]]
+    (fn [state]
+      ;; (prn '(&/show-ast ?fn) (&/show-ast ?fn))
+      (matchv ::M/objects [((&&/analyse-1 (partial analyse-ast eval!) exo-type ?fn) state)]
+        [["lux;Right" [state* =fn]]]
+        ((&&lux/analyse-apply (partial analyse-ast eval!) exo-type =fn ?args) state*)
+
+        [_]
+        (do ;; (prn 'analyse-ast/token (aget token 0) (&/show-state state))
+            ((analyse-basic-ast (partial analyse-ast eval!) eval! exo-type token) state))))
+    
+    [_]
+    (analyse-basic-ast (partial analyse-ast eval!) eval! exo-type token)))
 
 ;; [Resources]
 (defn analyse [eval!]
   (exec [asts &parser/parse]
-    (&/flat-map% (analyse-ast eval!) asts)))
+    (&/flat-map% (partial analyse-ast eval! &type/Nothing) asts)))
diff --git a/src/lux/analyser/base.clj b/src/lux/analyser/base.clj
index 827d0336e..62ccedb51 100644
--- a/src/lux/analyser/base.clj
+++ b/src/lux/analyser/base.clj
@@ -16,8 +16,8 @@
     [["Statement" _]]
     (fail (str "[Analyser Error] Can't retrieve the type of a statement: " (pr-str syntax+)))))
 
-(defn analyse-1 [analyse elem]
-  (exec [output (analyse elem)]
+(defn analyse-1 [analyse exo-type elem]
+  (exec [output (analyse exo-type elem)]
     (do ;; (prn 'analyse-1 (aget output 0))
       (matchv ::M/objects [output]
         [["lux;Cons" [x ["lux;Nil" _]]]]
diff --git a/src/lux/analyser/lux.clj b/src/lux/analyser/lux.clj
index aa205bf06..e38d10117 100644
--- a/src/lux/analyser/lux.clj
+++ b/src/lux/analyser/lux.clj
@@ -2,7 +2,7 @@
   (:require (clojure [template :refer [do-template]])
             [clojure.core.match :as M :refer [matchv]]
             clojure.core.match.array
-            (lux [base :as & :refer [exec return return* fail fail* |let]]
+            (lux [base :as & :refer [exec return return* fail fail* |let |list]]
                  [parser :as &parser]
                  [type :as &type]
                  [macro :as &macro]
@@ -13,15 +13,35 @@
                           [env :as &&env]
                           [def :as &&def])))
 
-;; [Resources]
-(defn analyse-tuple [analyse ?elems]
-  (exec [=elems (&/flat-map% analyse ?elems)
+(defn ^:private analyse-1+ [analyse]
+  (fn [?token]
+    (&&/with-var #(&&/analyse-1 analyse % ?token))))
+
+;; [Exports]
+(defn analyse-tuple [analyse exo-type ?elems]
+  (exec [=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/solve exo-type endo-type)
+         ;; :let [_ (prn 'analyse-tuple 'DONE)]
          ]
-    (return (&/|list (&/V "Expression" (&/T (&/V "tuple" =elems) (&/V "lux;TupleT" =elems-types)))))))
+    (return (&/|list (&/V "Expression" (&/T (&/V "tuple" =elems)
+                                            exo-type))))))
 
-(defn analyse-record [analyse ?elems]
+(defn analyse-variant [analyse exo-type ident ?value]
+  (|let [[?module ?name] ident
+         ?tag (str ?module ";" ?name)]
+    (exec [=value ((analyse-1+ analyse) ?value)
+           =value-type (&&/expr-type =value)
+           :let [endo-type (&/V "lux;VariantT" (|list (&/T ?tag =value-type)))]
+           _ (&type/solve exo-type endo-type)
+           ;; :let [_ (prn 'analyse-variant 'DONE)]
+           ]
+      (return (&/|list (&/V "Expression" (&/T (&/V "variant" (&/T ?tag =value))
+                                              exo-type)))))))
+
+(defn analyse-record [analyse exo-type ?elems]
   (exec [=elems (&/map% (fn [kv]
                           (matchv ::M/objects [kv]
                             [[k v]]
@@ -38,19 +58,10 @@
          ]
     (return (&/|list (&/V "Expression" (&/T (&/V "lux;record" =elems) (&/V "lux;RecordT" =elems-types)))))))
 
-(defn ^:private resolve-global [ident state]
-  (|let [[?module ?name] ident
-         ident* (str ?module ";" ?name)]
-    (if-let [global (->> state (&/get$ "lux;global-env") &/from-some (&/get$ "lux;locals") (&/get$ "lux;mappings") (&/|get ident*))]
-      (return* state (&/|list global))
-      (fail* (str "[Analyser Error] Unresolved identifier: " ident*)))))
-
-(defn analyse-ident [analyse ident]
+(defn analyse-symbol [analyse exo-type ident]
   (|let [[?module ?name] ident]
     (do ;; (prn 'analyse-ident ?module ?name)
-      (exec [module-name &/get-module-name]
-        (if (not= module-name ?module)
-          (partial resolve-global ident)
+        (exec [module-name &/get-module-name]
           (fn [state]
             ;; (when (and (= "lux" ?module)
             ;;            (= "output" ?name))
@@ -59,44 +70,40 @@
             ;; (prn '(&/get$ "local-envs" state) (&/get$ "local-envs" state))
             ;; (prn '(&/->seq (&/get$ "local-envs" state)) (&/->seq (&/get$ "local-envs" state)))
             ;; (println (&/show-state state))
-            (let [stack (&/get$ "lux;local-envs" state)]
-              (matchv ::M/objects [stack]
+            (|let [stack (&/get$ "lux;local-envs" state)
+                   no-binding? #(and (->> % (&/get$ "lux;locals")  (&/get$ "lux;mappings") (&/|contains? ?name) not)
+                                     (->> % (&/get$ "lux;closure") (&/get$ "lux;mappings") (&/|contains? ?name) not))
+                   [inner outer] (&/|split-with no-binding? stack)]
+              (matchv ::M/objects [outer]
                 [["lux;Nil" _]]
-                (resolve-global ident state)
-                
-                [["lux;Cons" [top stack*]]]
-                (if-let [=bound (or (->> stack &/|head (&/get$ "lux;locals")  (&/get$ "lux;mappings") (&/|get ?name))
-                                    (->> stack &/|head (&/get$ "lux;closure") (&/get$ "lux;mappings") (&/|get ?name)))]
-                  (return* state (&/|list =bound))
-                  (|let [no-binding? #(and (->> % (&/get$ "lux;locals")  (&/get$ "lux;mappings") (&/|contains? ?name) not)
-                                           (->> % (&/get$ "lux;closure") (&/get$ "lux;mappings") (&/|contains? ?name) not))
-                         [inner outer] (&/|split-with no-binding? stack*)]
-                    (matchv ::M/objects [outer]
-                      [["lux;Nil" _]]
-                      (resolve-global ident state)
-
-                      [["lux;Cons" [top-outer _]]]
-                      (|let [in-stack (&/|cons top inner)
-                             scopes (&/|tail (&/folds #(&/|cons (&/get$ "lux;name" %2) %1)
-                                                      (&/|map #(&/get$ "lux;name" %) outer)
-                                                      (&/|reverse in-stack)))
-                             ;; _ (prn 'in-stack module-name ident (&/->seq (&/|map #(&/get$ "name" %) in-stack)) scopes)
-                             [=local inner*] (&/fold (fn [register+new-inner frame+in-scope]
-                                                       (|let [[register new-inner] register+new-inner
-                                                              [frame in-scope] frame+in-scope
-                                                              [register* frame*] (&&lambda/close-over (&/|cons module-name (&/|reverse in-scope)) ?name register frame)]
-                                                         (&/T register* (&/|cons frame* new-inner))))
-                                                     (&/T (or (->> top-outer (&/get$ "lux;locals")  (&/get$ "lux;mappings") (&/|get ?name))
-                                                              (->> top-outer (&/get$ "lux;closure") (&/get$ "lux;mappings") (&/|get ?name)))
-                                                          (&/|list))
-                                                     (&/zip2 (&/|reverse in-stack) scopes))]
-                        (return* (&/set$ "lux;local-envs" (&/|++ inner* outer) state) (&/|list =local)))
-                      )))
-                ))
-            ))
-        ))))
-
-(defn ^:private analyse-apply* [analyse =fn ?args]
+                (|let [[?module ?name] ident
+                       ident* (str ?module ";" ?name)]
+                  (if-let [global (->> state (&/get$ "lux;global-env") &/from-some (&/get$ "lux;locals") (&/get$ "lux;mappings") (&/|get ident*))]
+                    (&/run-state (exec [=global-type (&&/expr-type global)
+                                        _ (&type/solve exo-type =global-type)]
+                                   (return (&/|list global)))
+                                 state)
+                    (fail* (str "[Analyser Error] Unresolved identifier: " ident*))))
+
+                [["lux;Cons" [top-outer _]]]
+                (|let [scopes (&/|tail (&/folds #(&/|cons (&/get$ "lux;name" %2) %1)
+                                                (&/|map #(&/get$ "lux;name" %) outer)
+                                                (&/|reverse inner)))
+                       ;; _ (prn 'inner module-name ident (&/->seq (&/|map #(&/get$ "name" %) inner)) scopes)
+                       [=local inner*] (&/fold (fn [register+new-inner frame+in-scope]
+                                                 (|let [[register new-inner] register+new-inner
+                                                        [frame in-scope] frame+in-scope
+                                                        [register* frame*] (&&lambda/close-over (&/|cons module-name (&/|reverse in-scope)) ?name register frame)]
+                                                   (&/T register* (&/|cons frame* new-inner))))
+                                               (&/T (or (->> top-outer (&/get$ "lux;locals")  (&/get$ "lux;mappings") (&/|get ?name))
+                                                        (->> top-outer (&/get$ "lux;closure") (&/get$ "lux;mappings") (&/|get ?name)))
+                                                    (&/|list))
+                                               (&/zip2 (&/|reverse inner) scopes))]
+                  (return* (&/set$ "lux;local-envs" (&/|++ inner* outer) state) (&/|list =local)))
+                )))
+          ))))
+
+(defn ^:private analyse-apply* [analyse exo-type =fn ?args]
   (exec [=args (&/flat-map% analyse ?args)
          =fn-type (&&/expr-type =fn)
          [=apply _] (&/fold% (fn [[=fn =fn-type] =input]
@@ -113,7 +120,7 @@
                              =args)]
     (return (&/|list =apply))))
 
-(defn analyse-apply [analyse =fn ?args]
+(defn analyse-apply [analyse exo-type =fn ?args]
   ;; (prn 'analyse-apply1 (aget =fn 0))
   (exec [loader &/loader]
     (matchv ::M/objects [=fn]
@@ -136,7 +143,7 @@
       (fail "[Analyser Error] Can't call a statement!"))
     ))
 
-(defn analyse-case [analyse ?value ?branches]
+(defn analyse-case [analyse exo-type ?value ?branches]
   ;; (prn 'analyse-case (aget ?branches 0) (aget ?branches 1 1 0)
   ;;      (&/->seq ?branches))
   ;; (prn 'analyse-case (&/show-ast ?value))
@@ -160,12 +167,13 @@
          ;; :let [_ (prn '=bodies =bodies)]
          ;; :let [_ (prn 'analyse-case/=bodies =bodies)]
          =body-types (&/map% &&/expr-type =bodies)
+         :let [_ (prn 'analyse-case (->> =body-types (&/|map &type/show-type) (&/|interpose " ") (&/fold str "")))]
          =case-type (&/fold% &type/merge (&/V "lux;NothingT" nil) =body-types)
          :let [=branches (&/zip2 (&/|map &/|first branches) =bodies)]]
     (return (&/|list (&/V "Expression" (&/T (&/V "case" (&/T =value base-register max-locals =branches))
                                             =case-type))))))
 
-(defn analyse-lambda [analyse ?self ?arg ?body]
+(defn analyse-lambda [analyse exo-type ?self ?arg ?body]
   ;; (prn 'analyse-lambda ?self ?arg ?body)
   (exec [=lambda-type* &type/fresh-lambda]
     (matchv ::M/objects [=lambda-type*]
@@ -192,18 +200,21 @@
              ]
         (return (&/|list (&/V "Expression" (&/T (&/V "lambda" (&/T =scope =captured ?arg =body)) =lambda-type))))))))
 
-(defn analyse-def [analyse ?name ?value]
+(defn analyse-def [analyse exo-type ?name ?value]
   ;; (prn 'analyse-def ?name ?value)
-  (exec [module-name &/get-module-name]
+  (exec [_ (&type/solve &type/Nothing exo-type)
+         module-name &/get-module-name]
     (&/if% (&&def/defined? module-name ?name)
            (fail (str "[Analyser Error] Can't redefine " ?name))
            (exec [=value (&/with-scope ?name
-                           (&&/analyse-1 analyse ?value))
+                           (&&/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 [ident]
+(defn analyse-declare-macro [exo-type ident]
   (|let [[?module ?name] ident]
     (exec [module-name &/get-module-name]
       (if (= ?module module-name)
@@ -211,23 +222,18 @@
           (return (&/|list)))
         (fail "Can't declare macros from foreign modules.")))))
 
-(defn analyse-import [analyse ?path]
+(defn analyse-import [analyse exo-type ?path]
   (assert false)
   (return (&/|list)))
 
-(defn analyse-check [analyse eval! ?type ?value]
+(defn analyse-check [analyse eval! exo-type ?type ?value]
   (println "analyse-check#0")
-  (exec [=type (&&/analyse-1 analyse ?type)
+  (exec [=type (&&/analyse-1 analyse &type/Type ?type)
          :let [_ (println "analyse-check#1")]
-         =type-type (&&/expr-type =type)
-         :let [_ (println "analyse-check#2")
-               _ (println 1 (&type/show-type &type/Type))
-               _ (println 2 (&type/show-type =type-type))]
-         _ (&type/solve &type/init-fixpoints &type/Type =type-type)
-         :let [_ (println "analyse-check#3")]
          ==type (eval! =type)
+         _ (&type/solve &type/init-fixpoints exo-type ==type)
          :let [_ (println "analyse-check#4" (&type/show-type ==type))]
-         =value (&&/analyse-1 analyse ?value)
+         =value (&&/analyse-1 analyse ==type ?value)
          :let [_ (println "analyse-check#5")]]
     (matchv ::M/objects [=value]
       [["Expression" [?expr ?expr-type]]]
@@ -236,7 +242,7 @@
              :let [_ (println "analyse-check#7")]]
         (return (&/|list (&/V "Expression" (&/T ?expr ==type))))))))
 
-(defn analyse-coerce [analyse eval! ?type ?value]
+(defn analyse-coerce [analyse eval! exo-type ?type ?value]
   (exec [=type (&&/analyse-1 analyse ?type)
          =type-type (&&/expr-type =type)
          _ (&type/solve &type/init-fixpoints &type/Type =type-type)
diff --git a/src/lux/base.clj b/src/lux/base.clj
index 29ecfd123..cd5801660 100644
--- a/src/lux/base.clj
+++ b/src/lux/base.clj
@@ -312,12 +312,15 @@
 
 (do-template [<name> <joiner>]
   (defn <name> [f xs]
+    ;; (prn '<name> 0 (aget xs 0))
     (matchv ::M/objects [xs]
       [["lux;Nil" _]]
       (return xs)
 
       [["lux;Cons" [x xs*]]]
       (exec [y (f x)
+             ;; :let [_ (prn '<name> 1 (class y))
+             ;;       _ (prn '<name> 2 (aget y 0))]
              ys (<name> f xs*)]
         (return (<joiner> y ys)))))
 
@@ -658,7 +661,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))
diff --git a/src/lux/lexer.clj b/src/lux/lexer.clj
index 918ddc7d9..4dc46f41c 100644
--- a/src/lux/lexer.clj
+++ b/src/lux/lexer.clj
@@ -80,10 +80,9 @@
 
 (def ^:private lex-ident
   (&/try-all% (&/|list (exec [[_ [meta _]] (&reader/read-text ";")
-                              [_ [_ token]] (&reader/read-regex +ident-re+)
-                              module-name &/get-module-name]
-                         (return (&/V "lux;Meta" (&/T meta (&/T module-name token)))))
-                       (exec [[_ [metma token]] (&reader/read-regex +ident-re+)]
+                              [_ [_ token]] (&reader/read-regex +ident-re+)]
+                         (return (&/V "lux;Meta" (&/T meta (&/T "lux" token)))))
+                       (exec [[_ [meta token]] (&reader/read-regex +ident-re+)]
                          (&/try-all% (&/|list (exec [_ (&reader/read-text ";")
                                                      [_ [_ local-token]] (&reader/read-regex +ident-re+)]
                                                 (&/try-all% (&/|list (exec [unaliased (&def/unalias-module token)]
@@ -93,8 +92,7 @@
                                                                          (return (&/V "lux;Meta" (&/T meta (&/T token local-token))))
                                                                          (fail (str "[Lexer Error] Unknown module: " token))))
                                                                      )))
-                                              (exec [module-name &/get-module-name]
-                                                (return (&/V "lux;Meta" (&/T meta (&/T module-name token)))))
+                                              (return (&/V "lux;Meta" (&/T meta (&/T "" token))))
                                               )))
                        )))
 
diff --git a/src/lux/type.clj b/src/lux/type.clj
index 7d05d65b4..77025b62e 100644
--- a/src/lux/type.clj
+++ b/src/lux/type.clj
@@ -67,12 +67,12 @@
       [["lux;LambdaT" [?arg ?return]]]
       (exec [=arg (clean tvar ?arg)
              =return (clean tvar ?return)]
-        (return (&/V "lux;LambdaT" (to-array [=arg =return]))))
+        (return (&/V "lux;LambdaT" (&/T =arg =return))))
 
       [["lux;AppT" [?lambda ?param]]]
       (exec [=lambda (clean tvar ?lambda)
              =param (clean tvar ?param)]
-        (return (&/V "lux;AppT" (to-array [=lambda =param]))))
+        (return (&/V "lux;AppT" (&/T =lambda =param))))
 
       [["lux;TupleT" ?members]]
       (exec [=members (&/map% (partial clean tvar) ?members)]
@@ -81,23 +81,23 @@
       [["lux;VariantT" ?members]]
       (exec [=members (&/map% (fn [[k v]]
                                 (exec [=v (clean tvar v)]
-                                  (return (to-array [k =v]))))
+                                  (return (&/T k =v))))
                               ?members)]
         (return (&/V "lux;VariantT" =members)))
 
       [["lux;RecordT" ?members]]
       (exec [=members (&/map% (fn [[k v]]
                                 (exec [=v (clean tvar v)]
-                                  (return (to-array [k =v]))))
+                                  (return (&/T k =v))))
                               ?members)]
         (return (&/V "lux;RecordT" =members)))
 
       [["lux;AllT" [?env ?name ?arg ?body]]]
       (exec [=env (&/map% (fn [[k v]]
                             (exec [=v (clean tvar v)]
-                              (return (to-array [k =v]))))
+                              (return (&/T k =v))))
                           ?env)]
-        (return (&/V "lux;AllT" (to-array [=env ?name ?arg ?body]))))
+        (return (&/V "lux;AllT" (&/T =env ?name ?arg ?body))))
 
       [_]
       (return type)
@@ -113,7 +113,9 @@
     "Nothing"
 
     [["lux;DataT" [name params]]]
-    (str "(^ " name " [" (->> params (&/|map show-type) (&/|interpose " ") (&/fold str "")) "])")
+    (if (&/|empty? params)
+      "(,)"
+      (str "(^ " name " [" (->> params (&/|map show-type) (&/|interpose " ") (&/fold str "")) "])"))
 
     [["lux;TupleT" elems]]
     (str "(, " (->> elems (&/|map show-type) (&/|interpose " ") (&/fold str "")) ")")
@@ -217,8 +219,8 @@
          (type= xbody ybody))
 
     [_ _]
-    (do (prn 'type= (show-type x) (show-type y))
-      false)
+    (do ;; (prn 'type= (show-type x) (show-type y))
+        false)
     ))
 
 (defn ^:private fp-get [k xs]
@@ -275,7 +277,7 @@
     (if-let [bound (&/|get ?name env)]
       (do ;; (prn 'beta-reduce "lux;BoundT" ?name (->> (&/|keys env) (&/|interpose " ") (&/fold str ""))
           ;;      (show-type bound))
-        (beta-reduce env bound))
+          (beta-reduce env bound))
       type)
 
     [_]
@@ -294,7 +296,7 @@
 (def +dont-care+ (&/V "lux;AnyT" nil))
 
 (defn apply-type [type-fn param]
-  (prn 'apply-type (aget type-fn 0) (aget param 0))
+  ;; (prn 'apply-type (aget type-fn 0) (aget param 0))
   (matchv ::M/objects [type-fn]
     [["lux;AllT" [local-env local-name local-arg local-def]]]
     (return (beta-reduce (->> local-env
@@ -311,24 +313,24 @@
 
 (def init-fixpoints (&/|list))
 
-(defn solve [fixpoints expected actual]
-  (prn 'solve (aget expected 0) (aget actual 0))
-  ;; (prn 'solve (show-type expected) (show-type actual))
+(defn ^:private solve* [fixpoints expected actual]
+  (prn 'solve* (aget expected 0) (aget actual 0))
+  ;; (prn 'solve* (show-type expected) (show-type actual))
   (matchv ::M/objects [expected actual]
-    [["Any" _] _]
+    [["lux;AnyT" _] _]
     success
 
-    [_ ["Nothing" _]]
+    [_ ["lux;NothingT" _]]
     success
 
     [["lux;VarT" ?id] _]
     (&/try-all% (&/|list (exec [bound (deref ?id)]
-                           (solve fixpoints bound actual))
+                           (solve* fixpoints bound actual))
                          (reset ?id actual)))
     
     [_ ["lux;VarT" ?id]]
     (&/try-all% (&/|list (exec [bound (deref ?id)]
-                           (solve fixpoints expected bound))
+                           (solve* fixpoints expected bound))
                          (reset ?id expected)))
 
     [["lux;AppT" [F A]] _]
@@ -341,21 +343,21 @@
           (fail (solve-error expected actual)))
 
         [["lux;None" _]]
-        (solve (fp-put fp-pair true fixpoints) expected* actual)))
+        (solve* (fp-put fp-pair true fixpoints) expected* actual)))
 
     [_ ["lux;AppT" [F A]]]
     (exec [actual* (apply-type F A)]
-      (solve fixpoints expected actual*))
+      (solve* fixpoints expected actual*))
 
     [["lux;AllT" _] _]
     (exec [$var fresh-var
            expected* (apply-type expected $var)]
-      (solve fixpoints expected* actual))
+      (solve* fixpoints expected* actual))
 
     [_ ["lux;AllT" _]]
     (exec [$var fresh-var
            actual* (apply-type actual $var)]
-      (solve fixpoints expected actual*))
+      (solve* fixpoints expected actual*))
 
     [["lux;DataT" [e!name e!params]] ["lux;DataT" [a!name a!params]]]
     (cond (not= e!name a!name)
@@ -367,22 +369,23 @@
           :else
           (exec [_ (&/map% (fn [ea]
                              (|let [[e a] ea]
-                               (solve fixpoints e a)))
+                               (solve* fixpoints e a)))
                            (&/zip2 e!params a!params))]
             success))
 
     [["lux;LambdaT" [eI eO]] ["lux;LambdaT" [aI aO]]]
-    (exec [_ (solve fixpoints aI eI)]
-      (solve fixpoints eO aO))
+    (exec [_ (solve* fixpoints aI eI)]
+      (solve* fixpoints eO aO))
 
     [["lux;TupleT" e!members] ["lux;TupleT" a!members]]
     (if (= (&/|length e!members) (&/|length a!members))
       (exec [_ (&/map% (fn [ea]
                          (|let [[e a] ea]
-                           (do (prn "lux;TupleT" 'ITER (show-type e) (show-type a))
-                             (solve fixpoints e a))))
+                           (do ;; (prn "lux;TupleT" 'ITER (show-type e) (show-type a))
+                               (solve* fixpoints e a))))
                        (&/zip2 e!members a!members))
-             :let [_ (prn "lux;TupleT" 'DONE)]]
+             ;; :let [_ (prn "lux;TupleT" 'DONE)]
+             ]
         success)
       (do ;; (prn "lux;TupleT" (&/|length e!members) (&/|length a!members))
           ;; (prn "lux;TupleT"
@@ -395,7 +398,7 @@
     (exec [_ (&/map% (fn [kv]
                        (|let [[k av] kv]
                          (if-let [ev (&/|get k e!cases)]
-                           (solve fixpoints ev av)
+                           (solve* fixpoints ev av)
                            (fail (str "[Type Error] The expected variant cannot handle case: #" k)))))
                      a!cases)]
       success)
@@ -405,33 +408,41 @@
       (exec [_ (&/map% (fn [slot]
                          (if-let [e!type (&/|get e!fields slot)]
                            (if-let [a!type (&/|get a!fields slot)]
-                             (solve fixpoints e!type a!type)
+                             (solve* fixpoints e!type a!type)
                              (fail (solve-error expected actual)))
                            (fail (solve-error expected actual))))
                        (&/|keys e!fields))]
         success)
       (fail "[Type Error] Records don't match in size."))
 
-    [["lux;BoundT" name] _]
-    (do (prn "lux;BoundT" name)
-      (assert false))
+    ;; [["lux;BoundT" name] _]
+    ;; (do (prn "lux;BoundT" name)
+    ;;   (assert false))
     ;; ...
     
     ;; [_ ["lux;BoundT" name]]
     ;; ...
     ))
 
+(def solve (partial solve* init-fixpoints))
+
 (defn apply-lambda [func param]
   (matchv ::M/objects [func]
     [["lux;LambdaT" [input output]]]
-    (exec [_ (solve init-fixpoints input param)]
+    (exec [_ (solve* init-fixpoints input param)]
       (return output))
 
+    [["lux;AllT" [local-env local-name local-arg local-def]]]
+    (exec [$var fresh-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)))
     ))
 
 (def Any (&/V "lux;AnyT" nil))
+(def Nothing (&/V "lux;NothingT" nil))
 (def Int (&/V "lux;DataT" (&/T "java.lang.Long" (&/|list))))
 (def Text (&/V "lux;DataT" (&/T "java.lang.String" (&/|list))))
 
@@ -483,7 +494,7 @@
                               (matchv ::M/objects [kv]
                                 [[k v]]
                                 (if-let [cv (&/|get k cases)]
-                                  (exec [_ (solve init-fixpoints cv v)]
+                                  (exec [_ (solve* init-fixpoints cv v)]
                                     (return cases))
                                   (return (&/|put k v cases)))))
                             x!cases
@@ -496,7 +507,7 @@
                                  (matchv ::M/objects [kv]
                                    [[k v]]
                                    (if-let [cv (&/|get k fields)]
-                                     (exec [_ (solve init-fixpoints cv v)]
+                                     (exec [_ (solve* init-fixpoints cv v)]
                                        (return fields))
                                      (fail (str "[Type System Error] Incompatible records: " (show-type x) " and " (show-type y))))))
                                x!fields
@@ -513,7 +524,7 @@
                                                                                         (&/V "lux;VariantT" (&/|list (&/T "lux;Nil" (&/V "lux;TupleT" (&/|list)))))))))))
     )
   
-  (matchv ::M/objects [((solve init-fixpoints Type RealT)
+  (matchv ::M/objects [((solve Type RealT)
                         (&/init-state nil))]
     [["lux;Left" ?msg]]
     (assert false ?msg)
@@ -521,7 +532,7 @@
     [_]
     (println "YEAH!"))
 
-  (matchv ::M/objects [((solve init-fixpoints List (&/V "lux;AppT" (&/T List Real)))
+  (matchv ::M/objects [((solve List (&/V "lux;AppT" (&/T List Real)))
                         (&/init-state nil))]
     [["lux;Left" ?msg]]
     (assert false ?msg)