# HG changeset patch # User Adam Chlipala # Date 1318688390 14400 # Node ID 287604b4a08dcac3ba525c467337b069cf5ba096 # Parent 644558d9c756c2b54a6db6a7878fc215e15e6fb0 Improved unification of record literals in type class resolution diff -r 644558d9c756 -r 287604b4a08d src/elab_env.sml --- 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)) diff -r 644558d9c756 -r 287604b4a08d tests/tcrec.ur --- /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 = _