summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2011-10-15 10:19:50 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2011-10-15 10:19:50 -0400
commit95682837c58809ed98071acb6a1c2730b2ee1862 (patch)
tree5bd132fb29536e887593ea8d3f7baae3319e6e5b /src
parent40047b604b23d8342f9f3d499bacff2d78b88749 (diff)
Improved unification of record literals in type class resolution
Diffstat (limited to 'src')
-rw-r--r--src/elab_env.sml20
1 files changed, 16 insertions, 4 deletions
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 23f3df01..e53c1538 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -545,8 +545,14 @@ fun eqCons (c1, c2) =
| (CRecord (k1, xcs1), CRecord (k2, xcs2)) =>
(unifyKinds (k1, k2);
- ListPair.appEq (fn ((x1, c1), (x2, c2)) => (eqCons (x1, x2); eqCons (c1, c2))) (xcs1, xcs2)
- handle ListPair.UnequalLengths => raise Unify)
+ if length xcs1 <> length xcs2 then
+ raise Unify
+ else
+ List.app (fn (x1, c1) =>
+ if List.exists (fn (x2, c2) => (eqCons (x1, x2); eqCons (c1, c2); true) handle Unify => false) xcs2 then
+ ()
+ else
+ raise Unify) xcs1)
| (CConcat (f1, x1), CConcat (f2, x2)) => (eqCons (f1, f2); eqCons (x1, x2))
| (CMap (d1, r1), CMap (d2, r2)) => (unifyKinds (d1, d2); unifyKinds (r1, r2))
@@ -606,8 +612,14 @@ fun unifyCons (hnorm : con -> con) rs =
| (CRecord (k1, xcs1), CRecord (k2, xcs2)) =>
(unifyKinds (k1, k2);
- ListPair.appEq (fn ((x1, c1), (x2, c2)) => (unify d (x1, x2); unify d (c1, c2))) (xcs1, xcs2)
- handle ListPair.UnequalLengths => raise Unify)
+ if length xcs1 <> length xcs2 then
+ raise Unify
+ else
+ app (fn (x1, c1) =>
+ if List.exists (fn (x2, c2) => (unify d (x1, x2); unify d (c1, c2); true) handle Unify => false) xcs2 then
+ ()
+ else
+ raise Unify) xcs1)
| (CConcat (f1, x1), CConcat (f2, x2)) => (unify d (f1, f2); unify d (x1, x2))
| (CMap (d1, r1), CMap (d2, r2)) => (unifyKinds (d1, d2); unifyKinds (r1, r2))