- Type checking of polymorphic functions now relies on ExT types to guarantee that type-variables don't unify to anything, instead of relying on VarT types.

- Fixed some bugs in the standard library due to improper behavior of the type-checker.
- The analysis and pattern-matching code for records now reuses that of tuples.

4 files changed, 105 insertions, 102 deletions

diff --git a/src/lux/analyser.clj b/src/lux/analyser.clj
index fbc360628..9a57191f5 100644
--- a/src/lux/analyser.clj
+++ b/src/lux/analyser.clj
@@ -532,6 +532,12 @@
                  (prn 'analyse-basic-ast/Error-1 e)
                  (prn 'analyse-basic-ast/Error-2 (&/show-ast token))
                  (prn 'analyse-basic-ast/Error-3 (&type/show-type exo-type))
+                 (|case ((&type/deref+ exo-type) state)
+                   (&/$Right [_state _exo-type])
+                   (prn 'analyse-basic-ast/Error-4 (&type/show-type _exo-type))
+
+                   _
+                   (prn 'analyse-basic-ast/Error-4 'YOLO))
                  (throw e))
                )
         (&/$Right state* output)
diff --git a/src/lux/analyser/case.clj b/src/lux/analyser/case.clj
index 3b12270c2..f2afdb0e9 100644
--- a/src/lux/analyser/case.clj
+++ b/src/lux/analyser/case.clj
@@ -49,14 +49,9 @@
       (resolve-type type*))
 
     (&/$UnivQ _)
-    ;; (&type/actual-type _abody)
     (|do [$var &type/existential
           =type (&type/apply-type type $var)]
       (&type/actual-type =type))
-    ;; (&type/with-var
-    ;;   (fn [$var]
-    ;;     (|do [=type (&type/apply-type type $var)]
-    ;;       (&type/actual-type =type))))
 
     _
     (&type/actual-type type)))
@@ -126,7 +121,7 @@
   (adjust-type* (&/|list) type))
 
 (defn ^:private analyse-pattern [value-type pattern kont]
-  (|let [[_ pattern*] pattern]
+  (|let [[meta pattern*] pattern]
     (|case pattern*
       (&/$SymbolS "" name)
       (|do [=kont (&env/with-local name value-type
@@ -183,23 +178,8 @@
               (fail (str "[Pattern-matching Error] Tuples require tuple-types: " (&type/show-type value-type*))))))
       
       (&/$RecordS pairs)
-      (|do [?members (&&record/order-record pairs)
-            value-type* (adjust-type value-type)]
-        (|case value-type*
-          (&/$TupleT ?member-types)
-          (if (not (.equals ^Object (&/|length ?member-types) (&/|length ?members)))
-            (fail (str "[Pattern-matching Error] Pattern-matching mismatch. Require record[" (&/|length ?member-types) "]. Given record[" (&/|length ?members) "]"))
-            (|do [[=tests =kont] (&/fold (fn [kont* vm]
-                                           (|let [[v m] vm]
-                                             (|do [[=test [=tests =kont]] (analyse-pattern v m kont*)]
-                                               (return (&/T (&/Cons$ =test =tests) =kont)))))
-                                         (|do [=kont kont]
-                                           (return (&/T (&/|list) =kont)))
-                                         (&/|reverse (&/zip2 ?member-types ?members)))]
-              (return (&/T (&/V $TupleTestAC =tests) =kont))))
-
-          _
-          (fail "[Pattern-matching Error] Record requires record-type.")))
+      (|do [?members (&&record/order-record pairs)]
+        (analyse-pattern value-type (&/T meta (&/V &/$TupleS ?members)) kont))
 
       (&/$TagS ?ident)
       (|do [;; :let [_ (println "#00" (&/ident->text ?ident))]
diff --git a/src/lux/analyser/lux.clj b/src/lux/analyser/lux.clj
index 3a9b822ca..f22cc6c9a 100644
--- a/src/lux/analyser/lux.clj
+++ b/src/lux/analyser/lux.clj
@@ -44,19 +44,39 @@
                 (analyse-tuple analyse exo-type** ?elems))))
 
           _
-          (fail (str "[Analyser Error] Tuples require tuple-types: " (&type/show-type exo-type*) (&type/show-type exo-type))))))))
+          (fail (str "[Analyser Error] Tuples require tuple-types: " (&type/show-type exo-type*) " " (&type/show-type exo-type) " " "[" (->> ?elems (&/|map &/show-ast) (&/|interpose " ") (&/fold str "")) "]"))
+          ;; (assert false (str "[Analyser Error] Tuples require tuple-types: " (&type/show-type exo-type*) " " (&type/show-type exo-type) " " "[" (->> ?elems (&/|map &/show-ast) (&/|interpose " ") (&/fold str "")) "]"))
+          )))))
 
-(defn ^:private analyse-variant-body [analyse exo-type ?values]
-  (|do [output (|case ?values
-                 (&/$Nil)
-                 (analyse-tuple analyse exo-type (&/|list))
-
-                 (&/$Cons ?value (&/$Nil))
-                 (analyse exo-type ?value)
+(defn with-attempt [m-value on-error]
+  (fn [state]
+    (|case (m-value state)
+      (&/$Left msg)
+      ((on-error msg) state)
+      
+      output
+      output)))
 
-                 _
-                 (analyse-tuple analyse exo-type ?values)
-                 )]
+(defn ^:private analyse-variant-body [analyse exo-type ?values]
+  (|do [output (with-attempt
+                 (|case ?values
+                   (&/$Nil)
+                   (analyse-tuple analyse exo-type (&/|list))
+
+                   (&/$Cons ?value (&/$Nil))
+                   (analyse exo-type ?value)
+
+                   _
+                   (analyse-tuple analyse exo-type ?values))
+                 (fn [err]
+                   (fail (str err "\n"
+                              'analyse-variant-body " " (&type/show-type exo-type)
+                              " " (->> ?values (&/|map &/show-ast) (&/|interpose " ") (&/fold str ""))))
+                   ;; (assert false
+                   ;;         (str err "\n"
+                   ;;              'analyse-variant-body " " (&type/show-type exo-type)
+                   ;;              " " (->> ?values (&/|map &/show-ast) (&/|interpose " ") (&/fold str ""))))
+                   ))]
     (|case output
       (&/$Cons x (&/$Nil))
       (return x)
@@ -78,7 +98,13 @@
       (&/$VariantT ?cases)
       (|case (&/|at idx ?cases)
         (&/$Some vtype)
-        (|do [=value (analyse-variant-body analyse vtype ?values)]
+        (|do [=value (with-attempt
+                       (analyse-variant-body analyse vtype ?values)
+                       (fn [err]
+                         (|do [_exo-type (&type/deref+ exo-type)]
+                           (fail (str err "\n"
+                                      'analyse-variant " " idx " " (&type/show-type exo-type) " " (&type/show-type _exo-type)
+                                      " " (->> ?values (&/|map &/show-ast) (&/|interpose " ") (&/fold str "")))))))]
           (return (&/|list (&/T (&/V &&/$variant (&/T idx =value))
                                 exo-type))))
 
@@ -95,41 +121,8 @@
       (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]
-  ;; (when @&type/!flag
-  ;;   (prn 'analyse-record (&type/show-type exo-type)
-  ;;        (&/->seq (&/|map (fn [pair]
-  ;;                           (|let [[k v] pair]
-  ;;                             (str (&/show-ast k) " " (&/show-ast v))))
-  ;;                         ?elems))))
-  (|do [exo-type* (|case exo-type
-                    (&/$VarT ?id)
-                    (|do [exo-type* (&type/deref ?id)]
-                      (&type/actual-type exo-type*))
-
-                    (&/$UnivQ _)
-                    (|do [$var &type/existential
-                          =type (&type/apply-type exo-type $var)]
-                      (&type/actual-type =type))
-                    ;; (&type/with-var
-                    ;;   (fn [$var]
-                    ;;     (|do [=type (&type/apply-type exo-type $var)]
-                    ;;       (&type/actual-type =type))))
-
-                    _
-                    (&type/actual-type exo-type))
-        types (|case exo-type*
-                (&/$TupleT ?table)
-                (return ?table)
-
-                _
-                (fail (str "[Analyser Error] The type of a record must be a record-type:\n" (&type/show-type exo-type*) "\n" (&type/show-type exo-type))))
-        _ (&/assert! (= (&/|length types) (&/|length ?elems))
-                     (str "[Analyser Error] Record length mismatch. Expected: " (&/|length types) "; actual: " (&/|length ?elems)))
-        members (&&record/order-record ?elems)
-        =members (&/map2% (fn [elem-t elem]
-                            (&&/analyse-1 analyse elem-t elem))
-                          types members)]
-    (return (&/|list (&/T (&/V &&/$tuple =members) exo-type)))))
+  (|do [members (&&record/order-record ?elems)]
+    (analyse-tuple analyse exo-type members)))
 
 (defn ^:private analyse-global [analyse exo-type module name]
   (|do [[[r-module r-name] $def] (&&module/find-def module name)
@@ -222,7 +215,10 @@
   ;; (prn 'analyse-apply* (aget fun-type 0))
   (|case ?args
     (&/$Nil)
-    (|do [_ (&type/check exo-type fun-type)]
+    (|do [;; :let [_ (prn 'analyse-apply*/_0 (&type/show-type exo-type) (&type/show-type fun-type))]
+          _ (&type/check exo-type fun-type)
+          ;; :let [_ (prn 'analyse-apply*/_1 'SUCCESS (str "(_ " (->> ?args (&/|map &/show-ast) (&/|interpose " ") (&/fold str "")) ")"))]
+          ]
       (return (&/T fun-type (&/|list))))
     
     (&/$Cons ?arg ?args*)
@@ -248,7 +244,12 @@
 
         (&/$LambdaT ?input-t ?output-t)
         (|do [[=output-t =args] (analyse-apply* analyse exo-type ?output-t ?args*)
-              =arg (&&/analyse-1 analyse ?input-t ?arg)]
+              =arg (with-attempt
+                     (&&/analyse-1 analyse ?input-t ?arg)
+                     (fn [err]
+                       (fail (str err "\n"
+                                  'analyse-apply* " " (&type/show-type exo-type) " " (&type/show-type ?fun-type*)
+                                  " " "(_ " (->> ?args (&/|map &/show-ast) (&/|interpose " ") (&/fold str "")) ")"))))]
           (return (&/T =output-t (&/Cons$ =arg =args))))
 
         ;; [[&/$VarT ?id-t]]
@@ -325,35 +326,39 @@
 (defn analyse-lambda** [analyse exo-type ?self ?arg ?body]
   (|case exo-type
     (&/$UnivQ _)
-    (&type/with-var
-      (fn [$var]
-        (|do [exo-type* (&type/apply-type exo-type $var)
-              [_expr _] (analyse-lambda** analyse exo-type* ?self ?arg ?body)]
-          (|case $var
-            (&/$VarT ?id)
-            (|do [? (&type/bound? ?id)]
-              (if ?
-                (|do [dtype (&type/deref ?id)
-                      ;; dtype* (&type/actual-type dtype)
-                      ]
-                  (|case dtype
-                    (&/$BoundT ?vname)
-                    (return (&/T _expr exo-type))
-                    
-                    (&/$ExT _)
-                    (return (&/T _expr exo-type))
-
-                    (&/$VarT ?_id)
-                    (|do [?? (&type/bound? ?_id)]
-                      ;; (return (&/T _expr exo-type))
-                      (if ??
-                        (fail (str "[Analyser Error] Can't use type-var in any type-specific way inside polymorphic functions: " ?id " " (&type/show-type dtype)))
-                        (return (&/T _expr exo-type)))
-                      )
-
-                    _
-                    (fail (str "[Analyser Error] Can't use type-var in any type-specific way inside polymorphic functions: " ?id " " (&type/show-type dtype)))))
-                (return (&/T _expr exo-type))))))))
+    (|do [$var &type/existential
+          exo-type* (&type/apply-type exo-type $var)
+          [_expr _] (analyse-lambda** analyse exo-type* ?self ?arg ?body)]
+      (return (&/T _expr exo-type)))
+    ;; (&type/with-var
+    ;;   (fn [$var]
+    ;;     (|do [exo-type* (&type/apply-type exo-type $var)
+    ;;           [_expr _] (analyse-lambda** analyse exo-type* ?self ?arg ?body)]
+    ;;       (|case $var
+    ;;         (&/$VarT ?id)
+    ;;         (|do [? (&type/bound? ?id)]
+    ;;           (if ?
+    ;;             (|do [dtype (&type/deref ?id)
+    ;;                   ;; dtype* (&type/actual-type dtype)
+    ;;                   ]
+    ;;               (|case dtype
+    ;;                 (&/$BoundT ?vname)
+    ;;                 (return (&/T _expr exo-type))
+    
+    ;;                 (&/$ExT _)
+    ;;                 (return (&/T _expr exo-type))
+
+    ;;                 (&/$VarT ?_id)
+    ;;                 (|do [?? (&type/bound? ?_id)]
+    ;;                   ;; (return (&/T _expr exo-type))
+    ;;                   (if ??
+    ;;                     (fail (str "[Analyser Error] Can't use type-var in any type-specific way inside polymorphic functions: " ?id " " (&type/show-type dtype)))
+    ;;                     (return (&/T _expr exo-type)))
+    ;;                   )
+
+    ;;                 _
+    ;;                 (fail (str "[Analyser Error] Can't use type-var in any type-specific way inside polymorphic functions: " ?id " " (&type/show-type dtype)))))
+    ;;             (return (&/T _expr exo-type))))))))
     
     _
     (|do [exo-type* (&type/actual-type exo-type)]
diff --git a/src/lux/type.clj b/src/lux/type.clj
index 5fbc33de2..889d4fc47 100644
--- a/src/lux/type.clj
+++ b/src/lux/type.clj
@@ -342,7 +342,9 @@
     (deref id)
 
     _
-    (fail (str "[Type Error] Type is not a variable: " (show-type type)))))
+    ;; (assert false (str "[Type Error] Type is not a variable: " (show-type type)))
+    (fail (str "[Type Error] Type is not a variable: " (show-type type)))
+    ))
 
 (defn set-var [id type]
   (fn [state]
@@ -370,6 +372,7 @@
                id))))
 
 (def existential
+  ;; (Lux Type)
   (|do [seed &/gen-id]
     (return (&/V &/$ExT seed))))
 
@@ -650,6 +653,9 @@
 
     (&/$NamedT ?name ?type)
     (apply-type ?type param)
+
+    (&/$ExT id)
+    (return (App$ type-fn param))
     
     _
     (fail (str "[Type System] Not a type function:\n" (show-type type-fn) "\n"))))
@@ -728,6 +734,11 @@
              (check* class-loader fixpoints expected bound))
            state)))
 
+      [(&/$AppT (&/$ExT eid) eA) (&/$AppT (&/$ExT aid) aA)]
+      (if (= eid aid)
+        (check* class-loader fixpoints eA aA)
+        (fail (check-error expected actual)))
+
       [(&/$AppT (&/$VarT ?eid) A1) (&/$AppT (&/$VarT ?aid) A2)]
       (fn [state]
         (|case ((|do [F1 (deref ?eid)]
@@ -757,6 +768,7 @@
                    [fixpoints** _] (check* class-loader fixpoints* A1 A2)]
                (return (&/T fixpoints** nil)))
              state))))
+      
       ;; (|do [_ (check* class-loader fixpoints (Var$ ?eid) (Var$ ?aid))
       ;;       _ (check* class-loader fixpoints A1 A2)]
       ;;   (return (&/T fixpoints nil)))