Mercurial > urweb
diff src/elaborate.sml @ 2049:459ccbf8cd08
When unifying constructor-level unification variables, also unify their kinds
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Fri, 01 Aug 2014 16:11:36 -0400 |
| parents | 42ae25a354f8 |
| children | 834b438d57f3 |
line wrap: on
line diff
--- a/src/elaborate.sml Fri Aug 01 15:44:17 2014 -0400 +++ b/src/elaborate.sml Fri Aug 01 16:11:36 2014 -0400 @@ -1226,26 +1226,29 @@ else err (fn _ => TooLifty (loc1, loc2)) - | (L'.CUnif (0, _, _, _, r as ref (L'.Unknown f)), _) => - if occursCon r c2All then - maybeIsRecord c2 - else if f c2All then - r := L'.Known c2All - else - err CScope - | (_, L'.CUnif (0, _, _, _, r as ref (L'.Unknown f))) => - if occursCon r c1All then - maybeIsRecord c1 - else if f c1All then - r := L'.Known c1All - else - err CScope - - | (L'.CUnif (nl, _, _, _, r as ref (L'.Unknown f)), _) => + | (L'.CUnif (0, _, k1, _, r as ref (L'.Unknown f)), _) => + (unifyKinds env k1 (kindof env c2All); + if occursCon r c2All then + maybeIsRecord c2 + else if f c2All then + r := L'.Known c2All + else + err CScope) + | (_, L'.CUnif (0, _, k2, _, r as ref (L'.Unknown f))) => + (unifyKinds env (kindof env c1All) k2; + if occursCon r c1All then + maybeIsRecord c1 + else if f c1All then + r := L'.Known c1All + else + err CScope) + + | (L'.CUnif (nl, _, k1, _, r as ref (L'.Unknown f)), _) => if occursCon r c2All then maybeIsRecord c2 else - (let + (unifyKinds env k1 (kindof env c2All); + let val sq = squish nl c2All in if f sq then @@ -1254,11 +1257,12 @@ err CScope end handle CantSquish => err (fn _ => TooDeep)) - | (_, L'.CUnif (nl, _, _, _, r as ref (L'.Unknown f))) => + | (_, L'.CUnif (nl, _, k2, _, r as ref (L'.Unknown f))) => if occursCon r c1All then maybeIsRecord c1 else - (let + (unifyKinds env (kindof env c1All) k2; + let val sq = squish nl c1All in if f sq then