aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEduardo Julian2018-01-04 23:59:40 -0400
committerEduardo Julian2018-01-04 23:59:40 -0400
commit303c462daf461c20f41edba3d0921062c8535fda (patch)
treeeb7d4edb5dfbd5af8789a128a4e3deb7eec985b6
parent5c18722100637a61a6e52b4471a2068f37a3dcff (diff)
- Fixed inference involving existentials.
Diffstat (limited to '')
-rw-r--r--new-luxc/source/luxc/lang/analysis/inference.lux27
-rw-r--r--stdlib/source/lux/math/constructive.lux7
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))))