diff options
| author |  Adam Chlipala <adam@chlipala.net> | 2014-08-01 16:11:36 -0400 |
|---|---|---|
| committer | Adam Chlipala <adam@chlipala.net> | 2014-08-01 16:11:36 -0400 |
| commit | ee4ec02054d2ec9c07cb2d0e0350f0d0cfd253a9 (patch) | |
| tree | 7281677ddfd7ec7ed6a2d15dbcb3623dd7c548c9 /src/elaborate.sml | |
| parent | b6d4f55981faff6ca7fa8b890c22ff4f33302ef2 (diff) | |
When unifying constructor-level unification variables, also unify their kinds
Diffstat (limited to 'src/elaborate.sml')
| -rw-r--r-- | src/elaborate.sml | 42 |
1 files changed, 23 insertions, 19 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml index 03e9d6e8..c55dec01 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -1226,26 +1226,29 @@ else err (fn _ => TooLifty (loc1, loc2)) - | (L'.CUnif (0, _, _, _, 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 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)), _) => - 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 |