- Yet more refactoring.

9 files changed, 115 insertions, 155 deletions

diff --git a/new-luxc/source/luxc/lang/analysis/case.lux b/new-luxc/source/luxc/lang/analysis/case.lux
index 5bf2e8ed1..ee4d4fcfa 100644
--- a/new-luxc/source/luxc/lang/analysis/case.lux
+++ b/new-luxc/source/luxc/lang/analysis/case.lux
@@ -47,13 +47,13 @@
   (case caseT
     (#;Var id)
     (do meta;Monad<Meta>
-      [? (&;with-type-env
-           (tc;concrete? id))]
-      (if ?
-        (do @
-          [caseT' (&;with-type-env
-                    (tc;read id))]
-          (simplify-case-type caseT'))
+      [?caseT' (&;with-type-env
+                 (tc;read id))]
+      (case ?caseT'
+        (#;Some caseT')
+        (simplify-case-type caseT')
+
+        _
         (&;throw Cannot-Simplify-Type-For-Pattern-Matching (%type caseT))))
 
     (#;Named name unnamedT)
@@ -71,9 +71,12 @@
       (do meta;Monad<Meta>
         [funcT' (&;with-type-env
                   (do tc;Monad<Check>
-                    [? (tc;concrete? funcT-id)]
-                    (if ?
-                      (tc;read funcT-id)
+                    [?funct' (tc;read funcT-id)]
+                    (case ?funct'
+                      (#;Some funct')
+                      (wrap funct')
+
+                      _
                       (tc;throw Cannot-Simplify-Type-For-Pattern-Matching (%type caseT)))))]
         (simplify-case-type (#;Apply inputT funcT')))
 
diff --git a/new-luxc/source/luxc/lang/analysis/common.lux b/new-luxc/source/luxc/lang/analysis/common.lux
index b14524559..968ebd2ea 100644
--- a/new-luxc/source/luxc/lang/analysis/common.lux
+++ b/new-luxc/source/luxc/lang/analysis/common.lux
@@ -11,14 +11,12 @@
         (lang analysis)))
 
 (def: #export (with-unknown-type action)
-  (All [a] (-> (Meta Analysis) (Meta [Type Analysis])))
+  (All [a] (-> (Meta a) (Meta [Type a])))
   (do meta;Monad<Meta>
-    [[var-id var-type] (&;with-type-env tc;var)
-     analysis (&;with-expected-type var-type
-                action)
-     analysis-type (&;with-type-env
-                     (tc;clean var-id var-type))]
-    (wrap [analysis-type analysis])))
+    [[_ varT] (&;with-type-env tc;var)
+     analysis (&;with-expected-type varT
+                action)]
+    (wrap [varT analysis])))
 
 (exception: #export Variant-Tag-Out-Of-Bounds)
 
diff --git a/new-luxc/source/luxc/lang/analysis/function.lux b/new-luxc/source/luxc/lang/analysis/function.lux
index 2a9826683..6a4a33e48 100644
--- a/new-luxc/source/luxc/lang/analysis/function.lux
+++ b/new-luxc/source/luxc/lang/analysis/function.lux
@@ -50,29 +50,21 @@
           
           (#;Var id)
           (do @
-            [? (&;with-type-env
-                 (tc;concrete? id))]
-            (if ?
-              (do @
-                [expectedT' (&;with-type-env
-                              (tc;read id))]
-                (recur expectedT'))
+            [?expectedT' (&;with-type-env
+                           (tc;read id))]
+            (case ?expectedT'
+              (#;Some expectedT')
+              (recur expectedT')
+
+              _
               ## Inference
               (do @
                 [[input-id inputT] (&;with-type-env tc;var)
                  [output-id outputT] (&;with-type-env tc;var)
                  #let [funT (#;Function inputT outputT)]
                  funA (recur funT)
-                 funT' (&;with-type-env
-                         (tc;clean output-id funT))
-                 concrete-input? (&;with-type-env
-                                   (tc;concrete? input-id))
-                 funT'' (if concrete-input?
-                          (&;with-type-env
-                            (tc;clean input-id funT'))
-                          (wrap (type;univ-q +1 (&inference;replace-var input-id +1 funT'))))
                  _ (&;with-type-env
-                     (tc;check expectedT funT''))]
+                     (tc;check expectedT funT))]
                 (wrap funA))
               ))
 
diff --git a/new-luxc/source/luxc/lang/analysis/inference.lux b/new-luxc/source/luxc/lang/analysis/inference.lux
index 5152de0b6..8b04ac2b7 100644
--- a/new-luxc/source/luxc/lang/analysis/inference.lux
+++ b/new-luxc/source/luxc/lang/analysis/inference.lux
@@ -14,50 +14,22 @@
               (analysis ["&;" common]))))
 
 (exception: #export Cannot-Infer)
+(def: (cannot-infer type args)
+  (-> Type (List Code) Text)
+  (format "     Type: " (%type type) "\n"
+          "Arguments:"
+          (|> args
+              list;enumerate
+              (list/map (function [[idx argC]]
+                          (format "\n  " (%n idx) " " (%code argC))))
+              (text;join-with ""))))
+
 (exception: #export Cannot-Infer-Argument)
 (exception: #export Smaller-Variant-Than-Expected)
 (exception: #export Invalid-Type-Application)
 (exception: #export Not-A-Record-Type)
 (exception: #export Not-A-Variant-Type)
 
-## When doing inference, type-variables often need to be created in
-## order to figure out which types are present in the expression being
-## inferred.
-## If a type-variable never gets bound/resolved to a type, then that
-## means the expression can be generalized through universal
-## quantification.
-## When that happens, the type-variable must be replaced by an
-## argument to the universally-quantified type.
-(def: #export (replace-var var-id bound-idx type)
-  (-> Nat Nat Type Type)
-  (case type
-    (#;Primitive name params)
-    (#;Primitive name (list/map (replace-var var-id bound-idx) params))
-
-    (^template [<tag>]
-      (<tag> left right)
-      (<tag> (replace-var var-id bound-idx left)
-             (replace-var var-id bound-idx right)))
-    ([#;Sum]
-     [#;Product]
-     [#;Function]
-     [#;Apply])
-    
-    (#;Var id)
-    (if (n.= var-id id)
-      (#;Bound bound-idx)
-      type)
-
-    (^template [<tag>]
-      (<tag> env quantified)
-      (<tag> (list/map (replace-var var-id bound-idx) env)
-             (replace-var var-id (n.+ +2 bound-idx) quantified)))
-    ([#;UnivQ]
-     [#;ExQ])
-    
-    _
-    type))
-
 (def: (replace-bound bound-idx replacementT type)
   (-> Nat Type Type Type)
   (case type
@@ -110,18 +82,8 @@
 
       (#;UnivQ _)
       (do meta;Monad<Meta>
-        [[var-id varT] (&;with-type-env tc;var)
-         [outputT argsA] (general analyse (maybe;assume (type;apply (list varT) inferT)) args)]
-        (do @
-          [? (&;with-type-env
-               (tc;concrete? var-id))
-           ## Quantify over the type if genericity/parametricity
-           ## is discovered.
-           outputT' (if ?
-                      (&;with-type-env
-                        (tc;clean var-id outputT))
-                      (wrap (type;univ-q +1 (replace-var var-id +1 outputT))))]
-          (wrap [outputT' argsA])))
+        [[var-id varT] (&;with-type-env tc;var)]
+        (general analyse (maybe;assume (type;apply (list varT) inferT)) args))
 
       (#;ExQ _)
       (do meta;Monad<Meta>
@@ -155,14 +117,18 @@
                   (analyse argC)))]
         (wrap [outputT' (list& argA args'A)]))
 
+      (#;Var infer-id)
+      (do meta;Monad<Meta>
+        [?inferT' (&;with-type-env (tc;read infer-id))]
+        (case ?inferT'
+          (#;Some inferT')
+          (general analyse inferT' args)
+
+          _
+          (&;throw Cannot-Infer (cannot-infer inferT args))))
+
       _
-      (&;throw Cannot-Infer (format "     Type: " (%type inferT) "\n"
-                                    "Arguments:"
-                                    (|> args
-                                        list;enumerate
-                                        (list/map (function [[idx argC]]
-                                                    (format "\n  " (%n idx) " " (%code argC))))
-                                        (text;join-with "")))))
+      (&;throw Cannot-Infer (cannot-infer inferT args)))
     ))
 
 ## Turns a record type into the kind of function type suitable for inference.
diff --git a/new-luxc/source/luxc/lang/analysis/procedure/common.lux b/new-luxc/source/luxc/lang/analysis/procedure/common.lux
index fff5de504..3965e78ba 100644
--- a/new-luxc/source/luxc/lang/analysis/procedure/common.lux
+++ b/new-luxc/source/luxc/lang/analysis/procedure/common.lux
@@ -141,42 +141,6 @@
   [lux//check typeA;analyse-check]
   [lux//coerce typeA;analyse-coerce])
 
-(def: (clean-type inputT)
-  (-> Type (tc;Check Type))
-  (case inputT
-    (#;Primitive name paramsT+)
-    (do tc;Monad<Check>
-      [paramsT+' (monad;map @ clean-type paramsT+)]
-      (wrap (#;Primitive name paramsT+')))
-
-    (^or #;Void #;Unit (#;Bound _) (#;Ex _) (#;Named _))
-    (:: tc;Monad<Check> wrap inputT)
-
-    (^template [<tag>]
-      (<tag> leftT rightT)
-      (do tc;Monad<Check>
-        [leftT' (clean-type leftT)
-         rightT' (clean-type rightT)]
-        (wrap (<tag> leftT' rightT'))))
-    ([#;Sum] [#;Product] [#;Function] [#;Apply])
-
-    (#;Var id)
-    (do tc;Monad<Check>
-      [? (tc;concrete? id)]
-      (if ?
-        (do @
-          [actualT (tc;read id)]
-          (clean-type actualT))
-        (wrap inputT)))
-
-    (^template [<tag>]
-      (<tag> envT+ unquantifiedT)
-      (do tc;Monad<Check>
-        [envT+' (monad;map @ clean-type envT+)]
-        (wrap (<tag> envT+' unquantifiedT))))
-    ([#;UnivQ] [#;ExQ])
-    ))
-
 (def: (lux//check//type proc)
   (-> Text Proc)
   (function [analyse eval args]
diff --git a/new-luxc/source/luxc/lang/analysis/procedure/host.jvm.lux b/new-luxc/source/luxc/lang/analysis/procedure/host.jvm.lux
index 39ca0eb43..cd5fdc7bb 100644
--- a/new-luxc/source/luxc/lang/analysis/procedure/host.jvm.lux
+++ b/new-luxc/source/luxc/lang/analysis/procedure/host.jvm.lux
@@ -305,9 +305,9 @@
          _ (&;infer varT)
          arrayA (&;with-expected-type (type (Array varT))
                   (analyse arrayC))
-         elemT (&;with-type-env
-                 (tc;read var-id))
-         [elemT elem-class] (box-array-element-type elemT)
+         ?elemT (&;with-type-env
+                  (tc;read var-id))
+         [elemT elem-class] (box-array-element-type (maybe;default varT ?elemT))
          idxA (&;with-expected-type Nat
                 (analyse idxC))]
         (wrap (la;procedure proc (list (code;text elem-class) idxA arrayA))))
@@ -325,9 +325,9 @@
          _ (&;infer (type (Array varT)))
          arrayA (&;with-expected-type (type (Array varT))
                   (analyse arrayC))
-         elemT (&;with-type-env
-                 (tc;read var-id))
-         [valueT elem-class] (box-array-element-type elemT)
+         ?elemT (&;with-type-env
+                  (tc;read var-id))
+         [valueT elem-class] (box-array-element-type (maybe;default varT ?elemT))
          idxA (&;with-expected-type Nat
                 (analyse idxC))
          valueA (&;with-expected-type valueT
diff --git a/new-luxc/source/luxc/lang/analysis/structure.lux b/new-luxc/source/luxc/lang/analysis/structure.lux
index e1f4de1d7..1f1ef15d7 100644
--- a/new-luxc/source/luxc/lang/analysis/structure.lux
+++ b/new-luxc/source/luxc/lang/analysis/structure.lux
@@ -1,17 +1,13 @@
 (;module:
   lux
   (lux (control [monad #+ do]
-                ["ex" exception #+ exception:]
-                pipe)
-       [function]
-       (concurrency ["A" atom])
+                ["ex" exception #+ exception:])
        (data [ident]
              [number]
              [product]
              [maybe]
              (coll [list "list/" Functor<List>]
                    [dict #+ Dict])
-             [text]
              text/format)
        [meta]
        (meta [code]
@@ -63,20 +59,21 @@
 
         (#;Var id)
         (do @
-          [concrete? (&;with-type-env
-                       (tc;concrete? id))]
-          (if concrete?
-            (do @
-              [expectedT' (&;with-type-env
-                            (tc;read id))]
-              (&;with-expected-type expectedT'
-                (analyse-sum analyse tag valueC)))
+          [?expectedT' (&;with-type-env
+                         (tc;read id))]
+          (case ?expectedT'
+            (#;Some expectedT')
+            (&;with-expected-type expectedT'
+              (analyse-sum analyse tag valueC))
+
+            _
             ## Cannot do inference when the tag is numeric.
             ## This is because there is no way of knowing how many
             ## cases the inferred sum type would have.
             (&;throw Cannot-Infer-Numeric-Tag (format "  Tag: " (%n tag) "\n"
                                                       "Value: " (%code  valueC) "\n"
-                                                      " Type: " (%type expectedT)))))
+                                                      " Type: " (%type expectedT)))
+            ))
 
         (^template [<tag> <instancer>]
           (<tag> _)
@@ -166,14 +163,14 @@
 
         (#;Var id)
         (do @
-          [concrete? (&;with-type-env
-                       (tc;concrete? id))]
-          (if concrete?
-            (do @
-              [expectedT' (&;with-type-env
-                            (tc;read id))]
-              (&;with-expected-type expectedT'
-                (analyse-product analyse membersC)))
+          [?expectedT' (&;with-type-env
+                         (tc;read id))]
+          (case ?expectedT'
+            (#;Some expectedT')
+            (&;with-expected-type expectedT'
+              (analyse-product analyse membersC))
+
+            _
             ## Must do inference...
             (do @
               [membersTA (monad;map @ (|>. analyse &common;with-unknown-type)
diff --git a/new-luxc/source/luxc/lang/translation.lux b/new-luxc/source/luxc/lang/translation.lux
index cf3137aff..6726470cc 100644
--- a/new-luxc/source/luxc/lang/translation.lux
+++ b/new-luxc/source/luxc/lang/translation.lux
@@ -8,6 +8,7 @@
              text/format
              (coll [dict]))
        [meta]
+       (meta (type ["tc" check]))
        [host]
        [io]
        (world [file #+ File]))
@@ -35,6 +36,43 @@
 (exception: #export Macro-Expansion-Failed)
 (exception: #export Unrecognized-Statement)
 
+(def: (clean inputT)
+  (-> Type (tc;Check Type))
+  (case inputT
+    (#;Primitive name paramsT+)
+    (do tc;Monad<Check>
+      [paramsT+' (monad;map @ clean paramsT+)]
+      (wrap (#;Primitive name paramsT+')))
+
+    (^or #;Void #;Unit (#;Bound _) (#;Ex _) (#;Named _))
+    (:: tc;Monad<Check> wrap inputT)
+
+    (^template [<tag>]
+      (<tag> leftT rightT)
+      (do tc;Monad<Check>
+        [leftT' (clean leftT)
+         rightT' (clean rightT)]
+        (wrap (<tag> leftT' rightT'))))
+    ([#;Sum] [#;Product] [#;Function] [#;Apply])
+
+    (#;Var id)
+    (do tc;Monad<Check>
+      [?actualT (tc;read id)]
+      (case ?actualT
+        (#;Some actualT)
+        (clean actualT)
+
+        _
+        (wrap inputT)))
+
+    (^template [<tag>]
+      (<tag> envT+ unquantifiedT)
+      (do tc;Monad<Check>
+        [envT+' (monad;map @ clean envT+)]
+        (wrap (<tag> envT+' unquantifiedT))))
+    ([#;UnivQ] [#;ExQ])
+    ))
+
 (def: (translate code)
   (-> Code (Meta Unit))
   (case code
@@ -55,6 +93,8 @@
                                    (wrap [Type valueA]))
                                  (commonA;with-unknown-type
                                    (analyse valueC))))
+           valueT (&;with-type-env
+                    (clean valueT))
            valueI (expressionT;translate (expressionS;synthesize valueA))
            _ (&;with-scope
                (statementT;translate-def def-name valueT valueI metaI (:! Code metaV)))]
diff --git a/new-luxc/source/luxc/lang/translation/statement.jvm.lux b/new-luxc/source/luxc/lang/translation/statement.jvm.lux
index 2a2173fa9..1cef99c76 100644
--- a/new-luxc/source/luxc/lang/translation/statement.jvm.lux
+++ b/new-luxc/source/luxc/lang/translation/statement.jvm.lux
@@ -76,7 +76,7 @@
            tags
            (&module;declare-tags tags (meta;export? metaV) (:! Type valueV)))
          (wrap []))
-     #let [_ (log! (format "DEF " current-module ";" def-name))]]
+     #let [_ (log! (format "DEF " (%ident [current-module def-name])))]]
     (commonT;record-artifact bytecode-name bytecode)))
 
 (def: #export (translate-program program-args programI)