diff options
| author |  Adam Chlipala <adam@chlipala.net> | 2011-10-15 10:19:50 -0400 |
|---|---|---|
| committer | Adam Chlipala <adam@chlipala.net> | 2011-10-15 10:19:50 -0400 |
| commit | 95682837c58809ed98071acb6a1c2730b2ee1862 (patch) | |
| tree | 5bd132fb29536e887593ea8d3f7baae3319e6e5b /src/elab_env.sml | |
| parent | 40047b604b23d8342f9f3d499bacff2d78b88749 (diff) | |
Improved unification of record literals in type class resolution
Diffstat (limited to 'src/elab_env.sml')
| -rw-r--r-- | src/elab_env.sml | 20 |
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)) |