unisonweb/unison
1
0
Fork 0
mirror of https://github.com/unisonweb/unison.git synced 2024-11-14 16:28:34 +03:00
Code Issues Projects Releases Wiki Activity

formatting

Browse Source
This commit is contained in:
Paul Chiusano 2015-03-09 14:51:05 -04:00
parent c615e237ad
commit aa7c513c18
1 changed files with 10 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
node/src/Unison/Type/Context.hs
View File

@ -343,16 +343,16 @@ synthesize ctx e = scope ("infer: " ++ show e) $ go e where
let e = fresh ctx
ctxTl = context [E.Marker e, E.Existential e]
step term ctx = check ctx term (T.Existential e)
in Foldable.foldrM step (ctx `append` ctxTl) v >>= \ctx' ->
pure $
let
(ctx1, ctx2) = breakAt (E.Marker e) ctx'
-- unsolved existentials get generalized to universals
vt = apply ctx2 (T.Unit T.Vector `T.App` T.Existential e)
existentials' = unsolved ctx2
vt2 = foldr gen vt existentials'
gen e vt = T.forall1 $ \v -> subst vt e v
in (vt2, ctx1)
in Foldable.foldrM step (ctx `append` ctxTl) v >>=
\ctx' -> pure $
let
(ctx1, ctx2) = breakAt (E.Marker e) ctx'
-- unsolved existentials get generalized to universals
vt = apply ctx2 (T.Unit T.Vector `T.App` T.Existential e)
existentials' = unsolved ctx2
vt2 = foldr gen vt existentials'
gen e vt = T.forall1 $ \v -> subst vt e v
in (vt2, ctx1)
go fn@(Term.Lam _) = -- ->I=> (Full Damas Milner rule)
let (arg, i, o) = fresh3 ctx
ctxTl = context [E.Marker i, E.Existential i, E.Existential o,