- Fixed inference involving existentials.

2 files changed, 28 insertions, 6 deletions

diff --git a/new-luxc/source/luxc/lang/analysis/inference.lux b/new-luxc/source/luxc/lang/analysis/inference.lux
index 881eee4a6..3919ff78d 100644
--- a/new-luxc/source/luxc/lang/analysis/inference.lux
+++ b/new-luxc/source/luxc/lang/analysis/inference.lux
@@ -60,6 +60,17 @@
     _
     type))
 
+(def: new-named-type
+  (Meta Type)
+  (do macro.Monad<Meta>
+    [[_module _line _column] macro.cursor
+     [ex-id exT] (&.with-type-env tc.existential)]
+    (wrap (#.Primitive (format "{New Type @ " (%t _module)
+                               "," (%n _line)
+                               "," (%n _column)
+                               "} " (%n ex-id))
+                       (list)))))
+
 ## Type-inference works by applying some (potentially quantified) type
 ## to a sequence of values.
 ## Function types are used for this, although inference is not always
@@ -87,9 +98,19 @@
 
       (#.ExQ _)
       (do macro.Monad<Meta>
-        [[ex-id exT] (&.with-type-env
-                       tc.existential)]
-        (general analyse (maybe.assume (type.apply (list exT) inferT)) args))
+        [[var-id varT] (&.with-type-env tc.var)
+         output (general analyse
+                         (maybe.assume (type.apply (list varT) inferT))
+                         args)
+         bound? (&.with-type-env
+                  (tc.bound? var-id))
+         _ (if bound?
+             (wrap [])
+             (do @
+               [newT new-named-type]
+               (&.with-type-env
+                 (tc.check varT newT))))]
+        (wrap output))
 
       (#.Apply inputT transT)
       (case (type.apply (list inputT) transT)
diff --git a/stdlib/source/lux/math/constructive.lux b/stdlib/source/lux/math/constructive.lux
index 3f12d1a88..5ecd8d0e2 100644
--- a/stdlib/source/lux/math/constructive.lux
+++ b/stdlib/source/lux/math/constructive.lux
@@ -7,6 +7,7 @@
              ["e" error]
              text/format
              (coll [list "list/" Functor<List>]))
+       (lang [type])
        (type abstract)
        [macro]
        (macro [code]
@@ -39,9 +40,9 @@
                 poly.apply
                 (p.after (poly.this Witness))
                 (p.after poly.any)
-                poly.existential)
-      (#e.Success witness-id)
-      (wrap (.list (.` (#.Ex (~ (code.nat witness-id))))))
+                poly.any)
+      (#e.Success identityT)
+      (wrap (.list (type.to-code identityT)))
       
       (#e.Error error)
       (macro.fail error))))