- Fixed a bug in the way type-adjustment happens during pattern-matching, in which the handing of universal quantification and type-vars was done improperly and caused the wrong type-vars to show up in the wrong places.

- Fixed a bug in the type-checking of function application, in which, if the result of an apply was a universally-quantified value, the type wasn't actually universally-quantified, even though the BoundTs had been added to it.
- Fixed a bug in the way the "loop" optimized-AST was compiled, which sometimes caused miscalculation, due to premature rebinding of variables.
- Now also cleaning ExQ.

4 files changed, 210 insertions, 71 deletions

diff --git a/src/lux/analyser/case.clj b/src/lux/analyser/case.clj
index 1c315e405..13e982fef 100644
--- a/src/lux/analyser/case.clj
+++ b/src/lux/analyser/case.clj
@@ -64,71 +64,188 @@
   (|let [[_env _idx _var] frame]
     (&/T [_env (+ 2 _idx) _var])))
 
-(defn adjust-type* [up type]
-  "(-> (List (, (Maybe (List Type)) Int Type)) Type (Lux Type))"
+(defn clean! [level ?tid bound-idx type]
   (|case type
-    (&/$UnivQ _aenv _abody)
-    (&type/with-var
-      (fn [$var]
-        (|do [=type (&type/apply-type type $var)
-              ==type (adjust-type* (&/$Cons (&/T [_aenv 1 $var]) (&/|map update-up-frame up)) =type)]
-          (&type/clean $var ==type))))
-
-    (&/$ExQ _aenv _abody)
-    (|do [$var &type/existential
-          =type (&type/apply-type type $var)]
-      (adjust-type* up =type))
+    (&/$VarT ?id)
+    (if (= ?tid ?id)
+      (let [new-bound (&/$BoundT (+ (* 2 level) bound-idx))]
+        (do ;; (prn 'CLEANED level ?tid bound-idx (&type/show-type new-bound))
+          new-bound))
+      type)
+
+    (&/$HostT ?name ?params)
+    (&/$HostT ?name (&/|map (partial clean! level ?tid bound-idx)
+                            ?params))
+    
+    (&/$LambdaT ?arg ?return)
+    (&/$LambdaT (clean! level ?tid bound-idx ?arg)
+                (clean! level ?tid bound-idx ?return))
+
+    (&/$AppT ?lambda ?param)
+    (&/$AppT (clean! level ?tid bound-idx ?lambda)
+             (clean! level ?tid bound-idx ?param))
 
     (&/$ProdT ?left ?right)
-    (|do [=type (&/fold% (fn [_abody ena]
-                           (|let [[_aenv _aidx (&/$VarT _avar)] ena]
-                             (|do [_ (&type/set-var _avar (&/$BoundT _aidx))]
-                               (&type/clean* _avar _abody))))
-                         type
-                         up)
-          :let [distributor (fn [v]
-                              (&/fold (fn [_abody ena]
-                                        (|let [[_aenv _aidx _avar] ena]
-                                          (&/$UnivQ _aenv _abody)))
-                                      v
-                                      up))
-                adjusted-type (&type/Tuple$ (&/|map distributor (&type/flatten-prod =type)))]]
-      (return adjusted-type))
-
+    (&/$ProdT (clean! level ?tid bound-idx ?left)
+              (clean! level ?tid bound-idx ?right))
+    
     (&/$SumT ?left ?right)
-    (|do [=type (&/fold% (fn [_abody ena]
-                           (|let [[_aenv _aidx (&/$VarT _avar)] ena]
-                             (|do [_ (&type/set-var _avar (&/$BoundT _aidx))]
-                               (&type/clean* _avar _abody))))
-                         type
-                         up)
-          :let [distributor (fn [v]
-                              (&/fold (fn [_abody ena]
-                                        (|let [[_aenv _aidx _avar] ena]
-                                          (&/$UnivQ _aenv _abody)))
-                                      v
-                                      up))
-                adjusted-type (&type/Variant$ (&/|map distributor (&type/flatten-sum =type)))]]
-      (return adjusted-type))
-
-    (&/$AppT ?tfun ?targ)
-    (|do [=type (&type/apply-type ?tfun ?targ)]
-      (adjust-type* up =type))
+    (&/$SumT (clean! level ?tid bound-idx ?left)
+             (clean! level ?tid bound-idx ?right))
 
-    (&/$VarT ?id)
-    (|do [type* (&/try-all% (&/|list (&type/deref ?id)
-                                     (fail (str "##2##: " ?id))))]
-      (adjust-type* up type*))
+    (&/$UnivQ ?env ?body)
+    (&/$UnivQ (&/|map (partial clean! level ?tid bound-idx) ?env)
+              (clean! (inc level) ?tid bound-idx ?body))
+
+    (&/$ExQ ?env ?body)
+    (&/$ExQ (&/|map (partial clean! level ?tid bound-idx) ?env)
+            (clean! (inc level) ?tid bound-idx ?body))
+
+    _
+    type
+    ))
+
+(defn beta-reduce! [level env type]
+  (do ;; (prn 0 'beta-reduce! level (&type/show-type type) (&/|length env))
+    (|case type
+      (&/$HostT ?name ?params)
+      (&/$HostT ?name (&/|map (partial beta-reduce! level env) ?params))
+
+      (&/$SumT ?left ?right)
+      (&/$SumT (beta-reduce! level env ?left)
+               (beta-reduce! level env ?right))
+
+      (&/$ProdT ?left ?right)
+      (&/$ProdT (beta-reduce! level env ?left)
+                (beta-reduce! level env ?right))
+
+      (&/$AppT ?type-fn ?type-arg)
+      (do ;; (prn 'beta-reduce! level 'APP (show-type ?type-fn) (show-type ?type-arg))
+          (&/$AppT (beta-reduce! level env ?type-fn)
+                   (beta-reduce! level env ?type-arg)))
+      
+      (&/$UnivQ ?local-env ?local-def)
+      (&/$UnivQ ?local-env (beta-reduce! (inc level) env ?local-def))
+
+      (&/$ExQ ?local-env ?local-def)
+      (&/$ExQ ?local-env (beta-reduce! (inc level) env ?local-def))
+
+      (&/$LambdaT ?input ?output)
+      (&/$LambdaT (beta-reduce! level env ?input)
+                  (beta-reduce! level env ?output))
+
+      (&/$BoundT ?idx)
+      (do ;; (prn 1 'beta-reduce! level [?idx (- ?idx (* 2 level))] (&/|length env))
+        (|case (&/|at (- ?idx (* 2 level)) env)
+          (&/$Some bound)
+          (do ;; (prn 'beta-reduce! level 'BOUND ?idx (&type/show-type bound))
+            (beta-reduce! level env bound))
+
+          _
+          type))
+
+      _
+      type
+      )))
+
+(defn apply-type! [type-fn param]
+  (|case type-fn
+    (&/$UnivQ local-env local-def)
+    (return (beta-reduce! 0 (->> local-env
+                                 (&/$Cons param)
+                                 (&/$Cons type-fn))
+                          local-def))
+
+    (&/$ExQ local-env local-def)
+    (return (beta-reduce! 0 (->> local-env
+                                 (&/$Cons param)
+                                 (&/$Cons type-fn))
+                          local-def))
+
+    (&/$AppT F A)
+    (|do [type-fn* (apply-type! F A)]
+      (apply-type! type-fn* param))
 
     (&/$NamedT ?name ?type)
-    (adjust-type* up ?type)
+    (apply-type! ?type param)
 
-    (&/$UnitT)
-    (return type)
+    (&/$ExT id)
+    (return (&/$AppT type-fn param))
 
+    (&/$VarT id)
+    (|do [=type-fun (deref id)]
+      (apply-type! =type-fun param))
+    
     _
-    (fail (str "[Pattern-matching Error] Can't adjust type: " (&type/show-type type)))
-    ))
+    (fail (str "[Type System] Not a type function:\n" (&type/show-type type-fn) "\n"))))
+
+(defn adjust-type* [up type]
+  "(-> (List (, (Maybe (List Type)) Int Type)) Type (Lux Type))"
+  (do ;; (prn 'adjust-type* 0 (&type/show-type type))
+    (|case type
+      (&/$UnivQ _aenv _abody)
+      (&type/with-var
+        (fn [$var]
+          (|do [=type (apply-type! type $var)
+                ==type (adjust-type* (&/$Cons (&/T [_aenv 1 $var]) (&/|map update-up-frame up)) =type)]
+            (&type/clean $var ==type))))
+
+      (&/$ExQ _aenv _abody)
+      (|do [$var &type/existential
+            =type (apply-type! type $var)]
+        (adjust-type* up =type))
+
+      (&/$ProdT ?left ?right)
+      (|do [:let [=type (&/fold (fn [_abody ena]
+                                  (|let [[_aenv _aidx (&/$VarT _avar)] ena]
+                                    (clean! 0 _avar _aidx _abody)))
+                                type
+                                up)]
+            ;; :let [_ (prn 'adjust-type* 1 (&type/show-type =type))]
+            :let [distributor (fn [v]
+                                (&/fold (fn [_abody ena]
+                                          (|let [[_aenv _aidx _avar] ena]
+                                            (&/$UnivQ _aenv _abody)))
+                                        v
+                                        up))
+                  adjusted-type (&type/Tuple$ (&/|map distributor (&type/flatten-prod =type)))]
+            ;; :let [_ (prn 'adjust-type* 2 (&type/show-type adjusted-type))]
+            ]
+        (return adjusted-type))
+
+      (&/$SumT ?left ?right)
+      (|do [:let [=type (&/fold (fn [_abody ena]
+                                  (|let [[_aenv _aidx (&/$VarT _avar)] ena]
+                                    (clean! 0 _avar _aidx _abody)))
+                                type
+                                up)]
+            :let [distributor (fn [v]
+                                (&/fold (fn [_abody ena]
+                                          (|let [[_aenv _aidx _avar] ena]
+                                            (&/$UnivQ _aenv _abody)))
+                                        v
+                                        up))
+                  adjusted-type (&type/Variant$ (&/|map distributor (&type/flatten-sum =type)))]]
+        (return adjusted-type))
+
+      (&/$AppT ?tfun ?targ)
+      (|do [=type (apply-type! ?tfun ?targ)]
+        (adjust-type* up =type))
+
+      (&/$VarT ?id)
+      (|do [type* (&/try-all% (&/|list (&type/deref ?id)
+                                       (fail (str "##2##: " ?id))))]
+        (adjust-type* up type*))
+
+      (&/$NamedT ?name ?type)
+      (adjust-type* up ?type)
+
+      (&/$UnitT)
+      (return type)
+
+      _
+      (fail (str "[Pattern-matching Error] Can't adjust type: " (&type/show-type type)))
+      )))
 
 (defn adjust-type [type]
   "(-> Type (Lux Type))"
diff --git a/src/lux/analyser/lux.clj b/src/lux/analyser/lux.clj
index d51ac2168..6ecd45974 100644
--- a/src/lux/analyser/lux.clj
+++ b/src/lux/analyser/lux.clj
@@ -20,6 +20,8 @@
                           [meta :as &&meta])))
 
 ;; [Utils]
+;; TODO: Walk the type to set up the bound-type, instead of doing a
+;; rough calculation like this one.
 (defn ^:private count-univq [type]
   "(-> Type Int)"
   (|case type
@@ -29,6 +31,8 @@
     _
     0))
 
+;; TODO: This technique won't work if the body of the type contains
+;; nested quantifications that are cannot be directly counted.
 (defn ^:private next-bound-type [type]
   "(-> Type Type)"
   (&/$BoundT (->> (count-univq type) (* 2) (+ 1))))
@@ -333,8 +337,10 @@
                   (|do [? (&type/bound? ?id)
                         type** (if ?
                                  (&type/clean $var =output-t)
-                                 (|do [_ (&type/set-var ?id (next-bound-type =output-t))]
-                                   (&type/clean $var =output-t)))
+                                 (|do [_ (&type/set-var ?id (next-bound-type =output-t))
+                                       cleaned-output* (&type/clean $var =output-t)
+                                       :let [cleaned-output (&/$UnivQ &/$Nil cleaned-output*)]]
+                                   (return cleaned-output)))
                         _ (&type/clean $var exo-type)]
                     (return (&/T [type** ==args])))
                   ))))
@@ -486,7 +492,7 @@
     _
     (&/with-attempt
       (|do [exo-type* (&type/actual-type exo-type)]
-        (|case exo-type
+        (|case exo-type*
           (&/$UnivQ _)
           (|do [$var &type/existential
                 :let [(&/$ExT $var-id) $var]
@@ -564,21 +570,22 @@
 
 (defn analyse-import [analyse compile-module path ex-alias]
   (|do [_ &/ensure-statement
-        module-name &/get-module-name
-        _ (if (= module-name path)
+        current-module &/get-module-name
+        _ (if (= current-module path)
             (&/fail-with-loc (str "[Analyser Error] Module can't import itself: " path))
             (return nil))]
     (&/save-module
      (|do [already-compiled? (&&module/exists? path)
            active? (&/active-module? path)
-           _ (&/assert! (not active?) (str "[Analyser Error] Can't import a module that is mid-compilation: " path " @ " module-name))
+           _ (&/assert! (not active?)
+                        (str "[Analyser Error] Can't import a module that is mid-compilation: " path " @ " current-module))
            _ (&&module/add-import path)
-           _ (if (not already-compiled?)
-               (compile-module path)
-               (return nil))
+           ?module-hash (if (not already-compiled?)
+                          (compile-module path)
+                          (&&module/module-hash path))
            _ (if (= "" ex-alias)
                (return nil)
-               (&&module/alias module-name ex-alias path))]
+               (&&module/alias current-module ex-alias path))]
        (return &/$Nil)))))
 
 (defn ^:private coerce [new-type analysis]
diff --git a/src/lux/compiler/lux.clj b/src/lux/compiler/lux.clj
index d5481dbd8..a9cd3756f 100644
--- a/src/lux/compiler/lux.clj
+++ b/src/lux/compiler/lux.clj
@@ -151,6 +151,20 @@
 
 (defn compile-loop [compile $begin ?args]
   (|do [^MethodVisitor *writer* &/get-writer
+        :let [idxs+args (&/zip2 (&/|range* 1 (&/|length ?args))
+                                ?args)]
+        _ (&/map% (fn [idx+?arg]
+                    (|do [:let [[idx ?arg] idx+?arg
+                                already-set? (|case ?arg
+                                               [_ (&o/$var (&/$Local l-idx))]
+                                               (= idx l-idx)
+
+                                               _
+                                               false)]]
+                      (if already-set?
+                        (return nil)
+                        (compile ?arg))))
+                  idxs+args)
         _ (&/map% (fn [idx+?arg]
                     (|do [:let [[idx ?arg] idx+?arg
                                 already-set? (|case ?arg
@@ -159,14 +173,10 @@
 
                                                _
                                                false)]
-                          _ (if already-set?
-                              (return nil)
-                              (compile ?arg))
                           :let [_ (when (not already-set?)
                                     (.visitVarInsn *writer* Opcodes/ASTORE idx))]]
                       (return nil)))
-                  (&/zip2 (&/|range* 1 (&/|length ?args))
-                          ?args))
+                  (&/|reverse idxs+args))
         :let [_ (.visitJumpInsn *writer* Opcodes/GOTO $begin)]]
     (return nil)))
 
diff --git a/src/lux/type.clj b/src/lux/type.clj
index 898088ff8..f0ec289c2 100644
--- a/src/lux/type.clj
+++ b/src/lux/type.clj
@@ -323,9 +323,14 @@
 
     (&/$UnivQ ?env ?body)
     (|do [=env (&/map% (partial clean* ?tid) ?env)
-          body* (clean* ?tid ?body)]
+          body* (clean* ?tid ?body)] ;; TODO: DON'T CLEAN THE BODY
       (return (&/$UnivQ =env body*)))
 
+    (&/$ExQ ?env ?body)
+    (|do [=env (&/map% (partial clean* ?tid) ?env)
+          body* (clean* ?tid ?body)] ;; TODO: DON'T CLEAN THE BODY
+      (return (&/$ExQ =env body*)))
+
     _
     (return type)
     ))