summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2014-08-01 16:11:36 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2014-08-01 16:11:36 -0400
commitee4ec02054d2ec9c07cb2d0e0350f0d0cfd253a9 (patch)
tree7281677ddfd7ec7ed6a2d15dbcb3623dd7c548c9 /src
parentb6d4f55981faff6ca7fa8b890c22ff4f33302ef2 (diff)
When unifying constructor-level unification variables, also unify their kinds
Diffstat (limited to 'src')
-rw-r--r--src/elaborate.sml42
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