summaryrefslogtreecommitdiff
path: root/src/elaborate.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2010-10-10 15:37:14 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2010-10-10 15:37:14 -0400
commit3944b599134b89f12f24ae3f52d21f954463c765 (patch)
tree59ec01525ded42885a850c9e83ba458c79843ce5 /src/elaborate.sml
parent948aa854af8ca5560a1eea5221c4a1f3a6901970 (diff)
Tweaking unification fix to apply to demo/more
Diffstat (limited to 'src/elaborate.sml')
-rw-r--r--src/elaborate.sml34
1 files changed, 33 insertions, 1 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 37ca4b25..12047b9f 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -655,6 +655,24 @@
val delayedExhaustives = ref ([] : (E.env * L'.con * L'.pat list * ErrorMsg.span) list)
+ exception CantSquish
+
+ fun squish by =
+ U.Con.mapB {kind = fn _ => fn k => k,
+ con = fn bound => fn c =>
+ case c of
+ L'.CRel xn =>
+ if xn < bound then
+ c
+ else if bound <= xn andalso xn < bound + by then
+ raise CantSquish
+ else
+ L'.CRel (xn - by)
+ | L'.CUnif _ => raise CantSquish
+ | _ => c,
+ bind = fn (bound, U.Con.RelC _) => bound + 1
+ | (bound, _) => bound} 0
+
fun unifyRecordCons env (loc, c1, c2) =
let
fun rkindof c =
@@ -1056,6 +1074,19 @@
else
r := SOME c1All
+ | (L'.CUnif (nl, _, _, _, r), _) =>
+ if occursCon r c2All then
+ err COccursCheckFailed
+ else
+ (r := SOME (squish nl c2All)
+ handle CantSquish => err CIncompatible)
+ | (_, L'.CUnif (nl, _, _, _, r)) =>
+ if occursCon r c1All then
+ err COccursCheckFailed
+ else
+ (r := SOME (squish nl c1All)
+ handle CantSquish => err CIncompatible)
+
| (L'.CUnit, L'.CUnit) => ()
| (L'.TFun (d1, r1), L'.TFun (d2, r2)) =>
@@ -1290,7 +1321,8 @@ fun elabPat (pAll as (p, loc), (env, bound)) =
val k = (L'.KType, loc)
val unifs = map (fn _ => cunif (loc, k)) xs
val nxs = length unifs - 1
- val t = ListUtil.foldli (fn (i, u, t) => subConInCon env (nxs - i, u) t) t unifs
+ val t = ListUtil.foldli (fn (i, u, t) => subConInCon env (nxs - i,
+ E.mliftConInCon (nxs - i) u) t) t unifs
val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs
in
ignore (checkPatCon env p' pt t);