diff options
| author |  Adam Chlipala <adam@chlipala.net> | 2011-12-18 11:29:13 -0500 |
|---|---|---|
| committer | Adam Chlipala <adam@chlipala.net> | 2011-12-18 11:29:13 -0500 |
| commit | 4eb93836d04d18f43d8c4360f290a7977d96c468 (patch) | |
| tree | ef38476a5b0199272d5dc20a65a306b4c7b2a112 /src/elab_util.sml | |
| parent | 37cf82d0761088c469205b90e35569674707202f (diff) | |
Add a new scoping check for unification variables, to fix a type inference bug
Diffstat (limited to 'src/elab_util.sml')
| -rw-r--r-- | src/elab_util.sml | 19 |
1 files changed, 16 insertions, 3 deletions
diff --git a/src/elab_util.sml b/src/elab_util.sml index bf0185b1..df78616a 100644 --- a/src/elab_util.sml +++ b/src/elab_util.sml @@ -75,10 +75,10 @@ fun mapfoldB {kind, bind} = | KError => S.return2 kAll - | KUnif (_, _, ref (SOME k)) => mfk' ctx k + | KUnif (_, _, ref (KKnown k)) => mfk' ctx k | KUnif _ => S.return2 kAll - | KTupleUnif (_, _, ref (SOME k)) => mfk' ctx k + | KTupleUnif (_, _, ref (KKnown k)) => mfk' ctx k | KTupleUnif (loc, nks, r) => S.map2 (ListUtil.mapfold (fn (n, k) => S.map2 (mfk ctx k, @@ -217,7 +217,7 @@ fun mapfoldB {kind = fk, con = fc, bind} = (CProj (c', n), loc)) | CError => S.return2 cAll - | CUnif (nl, _, _, _, ref (SOME c)) => mfc' ctx (!mliftConInCon nl c) + | CUnif (nl, _, _, _, ref (Known c)) => mfc' ctx (!mliftConInCon nl c) | CUnif _ => S.return2 cAll | CKAbs (x, c) => @@ -256,6 +256,19 @@ fun map {kind, con} s = S.Return () => raise Fail "ElabUtil.Con.map: Impossible" | S.Continue (s, ()) => s +fun appB {kind, con, bind} ctx c = + case mapfoldB {kind = fn ctx => fn k => fn () => (kind ctx k; S.Continue (k, ())), + con = fn ctx => fn c => fn () => (con ctx c; S.Continue (c, ())), + bind = bind} ctx c () of + S.Continue _ => () + | S.Return _ => raise Fail "ElabUtil.Con.appB: Impossible" + +fun app {kind, con} s = + case mapfold {kind = fn k => fn () => (kind k; S.Continue (k, ())), + con = fn c => fn () => (con c; S.Continue (c, ()))} s () of + S.Return () => raise Fail "ElabUtil.Con.app: Impossible" + | S.Continue _ => () + fun existsB {kind, con, bind} ctx c = case mapfoldB {kind = fn ctx => fn k => fn () => if kind (ctx, k) then |