- Improved handling of type variables.

3 files changed, 64 insertions, 19 deletions

diff --git a/new-luxc/source/luxc/lang/analysis/case.lux b/new-luxc/source/luxc/lang/analysis/case.lux
index 5f8ed344f..b0098f7c2 100644
--- a/new-luxc/source/luxc/lang/analysis/case.lux
+++ b/new-luxc/source/luxc/lang/analysis/case.lux
@@ -26,6 +26,7 @@
 (exception: #export Sum-Type-Has-No-Case)
 (exception: #export Unrecognized-Pattern-Syntax)
 (exception: #export Cannot-Simplify-Type-For-Pattern-Matching)
+(exception: #export Cannot-Apply-Type)
 
 (def: (pattern-error type pattern)
   (-> Type Code Text)
@@ -40,19 +41,19 @@
 ## type-variables or quantifications.
 ## This function makes it easier for "case" analysis to properly
 ## type-check the input with respect to the patterns.
-(def: (simplify-case-type type)
+(def: (simplify-case-type caseT)
   (-> Type (Meta Type))
-  (case type
+  (case caseT
     (#;Var id)
     (do meta;Monad<Meta>
       [? (&;with-type-env
            (tc;concrete? id))]
       (if ?
         (do @
-          [type' (&;with-type-env
-                   (tc;read id))]
-          (simplify-case-type type'))
-        (&;throw Cannot-Simplify-Type-For-Pattern-Matching (%type type))))
+          [caseT' (&;with-type-env
+                    (tc;read id))]
+          (simplify-case-type caseT'))
+        (&;throw Cannot-Simplify-Type-For-Pattern-Matching (%type caseT))))
 
     (#;Named name unnamedT)
     (simplify-case-type unnamedT)
@@ -61,18 +62,30 @@
     (do meta;Monad<Meta>
       [[ex-id exT] (&;with-type-env
                      tc;existential)]
-      (simplify-case-type (maybe;assume (type;apply (list exT) type))))
+      (simplify-case-type (maybe;assume (type;apply (list exT) caseT))))
 
     (#;Apply inputT funcT)
-    (case (type;apply (list inputT) funcT)
-      (#;Some outputT)
-      (:: meta;Monad<Meta> wrap outputT)
+    (case funcT
+      (#;Var funcT-id)
+      (do meta;Monad<Meta>
+        [funcT' (&;with-type-env
+                  (do tc;Monad<Check>
+                    [? (tc;concrete? funcT-id)]
+                    (if ?
+                      (tc;read funcT-id)
+                      (tc;throw Cannot-Apply-Type (%type caseT)))))]
+        (simplify-case-type (#;Apply inputT funcT')))
+
+      _
+      (case (type;apply (list inputT) funcT)
+        (#;Some outputT)
+        (:: meta;Monad<Meta> wrap outputT)
 
-      #;None
-      (&;fail (format "Cannot apply type " (%type funcT) " to  type " (%type inputT))))
+        #;None
+        (&;throw Cannot-Apply-Type (%type caseT))))
 
     _
-    (:: meta;Monad<Meta> wrap type)))
+    (:: meta;Monad<Meta> wrap caseT)))
 
 ## This function handles several concerns at once, but it must be that
 ## way because those concerns are interleaved when doing
diff --git a/new-luxc/source/luxc/lang/analysis/procedure/common.lux b/new-luxc/source/luxc/lang/analysis/procedure/common.lux
index c8e3e3b38..778e57b94 100644
--- a/new-luxc/source/luxc/lang/analysis/procedure/common.lux
+++ b/new-luxc/source/luxc/lang/analysis/procedure/common.lux
@@ -151,6 +151,42 @@
   [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/type.lux b/new-luxc/source/luxc/lang/analysis/type.lux
index 0a8abd76b..89b25334f 100644
--- a/new-luxc/source/luxc/lang/analysis/type.lux
+++ b/new-luxc/source/luxc/lang/analysis/type.lux
@@ -14,9 +14,7 @@
   (do meta;Monad<Meta>
     [actualT (eval Type type)
      #let [actualT (:! Type actualT)]
-     expectedT meta;expected-type
-     _ (&;with-type-env
-         (tc;check expectedT actualT))]
+     _ (&;infer actualT)]
     (&;with-expected-type actualT
       (analyse value))))
 
@@ -24,8 +22,6 @@
   (-> &;Analyser &;Eval Code Code (Meta Analysis))
   (do meta;Monad<Meta>
     [actualT (eval Type type)
-     expectedT meta;expected-type
-     _ (&;with-type-env
-         (tc;check expectedT (:! Type actualT)))]
+     _ (&;infer (:! Type actualT))]
     (&;with-expected-type Top
       (analyse value))))