- 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...)

3 files changed, 110 insertions, 114 deletions

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))))))