changeset 1575:287604b4a08d

Improved unification of record literals in type class resolution
author Adam Chlipala <adam@chlipala.net>
date Sat, 15 Oct 2011 10:19:50 -0400
parents 644558d9c756
children f6c74b4bc4e6
files src/elab_env.sml tests/tcrec.ur
diffstat 2 files changed, 21 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/src/elab_env.sml	Sat Oct 15 10:05:13 2011 -0400
+++ b/src/elab_env.sml	Sat Oct 15 10:19:50 2011 -0400
@@ -545,8 +545,14 @@
 
       | (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 @@
 
               | (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))
 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tests/tcrec.ur	Sat Oct 15 10:19:50 2011 -0400
@@ -0,0 +1,5 @@
+type r1 = {A : string, B : string}
+type r2 = {B : string, A : string}
+
+val show_r1 : show r1 = mkShow (fn r => r.A ^ "+" ^ r.B)
+val show_r2 : show r2 = _