From ee4ec02054d2ec9c07cb2d0e0350f0d0cfd253a9 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Fri, 1 Aug 2014 16:11:36 -0400 Subject: When unifying constructor-level unification variables, also unify their kinds --- src/elaborate.sml | 42 +++++++++++++++++++++++------------------- 1 file changed, 23 insertions(+), 19 deletions(-) (limited to 'src/elaborate.sml') 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 -- cgit v1.2.3