# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1419351807 18000
# Node ID d4eb9b6729f8a8841bb5bf87a77c14334b3c961d
# Parent  35c1341b01799e7dfc94fdc78aa9c6879f5198f7
Another try at a proper fix for constraint matching in subsignature checking

diff -r 35c1341b0179 -r d4eb9b6729f8 src/elaborate.sml
--- a/src/elaborate.sml	Sun Dec 21 13:20:11 2014 -0500
+++ b/src/elaborate.sml	Tue Dec 23 11:23:27 2014 -0500
@@ -2015,6 +2015,41 @@
         L'.CUnif (_, _, _, _, ref (L'.Known c)) => chaseUnifs c
       | _ => c
 
+val consEqSimple =
+    let
+        fun ces env (c1 : L'.con, c2 : L'.con) =
+            let
+                val c1 = hnormCon env c1
+                val c2 = hnormCon env c2
+            in
+                case (#1 c1, #1 c2) of
+                    (L'.CRel n1, L'.CRel n2) => n1 = n2
+                  | (L'.CNamed n1, L'.CNamed n2) =>
+                    n1 = n2 orelse
+                    (case #3 (E.lookupCNamed env n1) of
+                         SOME (L'.CNamed n2', _) => n2' = n1
+                       | _ => false)
+                  | (L'.CModProj n1, L'.CModProj n2) => n1 = n2
+                  | (L'.CApp (f1, x1), L'.CApp (f2, x2)) => ces env (f1, f2) andalso ces env (x1, x2)
+                  | (L'.CAbs (x1, k1, c1), L'.CAbs (_, _, c2)) => ces (E.pushCRel env x1 k1) (c1, c2)
+                  | (L'.CName x1, L'.CName x2) => x1 = x2
+                  | (L'.CRecord (_, xts1), L'.CRecord (_, xts2)) =>
+                    ListPair.all (fn ((x1, t1), (x2, t2)) =>
+                                     ces env (x1, x2) andalso ces env (t2, t2)) (xts1, xts2)
+                  | (L'.CConcat (x1, y1), L'.CConcat (x2, y2)) =>
+                    ces env (x1, x2) andalso ces env (y1, y2)
+                  | (L'.CMap _, L'.CMap _) => true
+                  | (L'.CUnit, L'.CUnit) => true
+                  | (L'.CTuple cs1, L'.CTuple cs2) => ListPair.all (ces env) (cs1, cs2)
+                  | (L'.CProj (c1, n1), L'.CProj (c2, n2)) => ces env (c1, c2) andalso n1 = n2
+                  | (L'.CUnif (_, _, _, _, r1), L'.CUnif (_, _, _, _, r2)) => r1 = r2
+                  | _ => false
+            end
+    in
+        ces
+    end
+    
+
 fun elabExp (env, denv) (eAll as (e, loc)) =
     let
         (*val () = eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)]*)
@@ -3020,26 +3055,7 @@
 
       | (L'.SgnConst sgis1, L'.SgnConst sgis2) =>
         let
-            (* This reshuffling was added to avoid some unfortunate unification behavior.
-             * In particular, in sub-signature checking, constraints might be unified,
-             * even when we don't expect them to be unifiable, deciding on bad values
-             * for unification variables and dooming later unification.
-             * By putting all the constraints _last_, we allow all the other unifications
-             * to happen first, hoping that no unification variables survive to confuse
-             * constraint unification. *)
-
-            val sgis2 =
-                let
-                    val (constraints, others) = List.partition
-                                                   (fn (L'.SgiConstraint _, _) => true
-                                                   | _ => false) sgis2
-                in
-                    case constraints of
-                        [] => sgis2
-                      | _ => others @ constraints
-                end
-
-            (*val () = prefaces "subSgn" [("sgn1", p_sgn env sgn1),
+           (*val () = prefaces "subSgn" [("sgn1", p_sgn env sgn1),
                                         ("sgn2", p_sgn env sgn2),
                                         ("sgis1", p_sgn env (L'.SgnConst sgis1, loc2)),
                                         ("sgis2", p_sgn env (L'.SgnConst sgis2, loc2))]*)
@@ -3370,8 +3386,11 @@
                         seek (fn (env, sgi1All as (sgi1, loc)) =>
                                  case sgi1 of
                                      L'.SgiConstraint (c1, d1) =>
-                                     if consEq env loc (c1, c2)
-					andalso consEq env loc (d1, d2) then
+                                     (* It's important to do only simple equality checking here,
+                                      * with no unification, because constraints are unnamed.
+                                      * It's too easy to pick the wrong pair to unify! *)
+                                     if consEqSimple env (c1, c2)
+					andalso consEqSimple env (d1, d2) then
                                          SOME env
                                      else
                                          NONE