summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2014-12-23 11:23:27 -0500
committerGravatar Adam Chlipala <adam@chlipala.net>2014-12-23 11:23:27 -0500
commit95b4aa54de703e59c4733ba828180a2a684c0274 (patch)
tree4fd812a645329fe83ffaefc826f29927fb5d204f
parent65e08aafe417c881b89e5c689048fd627a72129b (diff)
Another try at a proper fix for constraint matching in subsignature checking
-rw-r--r--src/elaborate.sml63
1 files changed, 41 insertions, 22 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 749bd2f1..f5edbe3e 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -2015,6 +2015,41 @@ fun chaseUnifs c =
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 @@ and subSgn' counterparts env strLoc sgn1 (sgn2 as (_, loc2)) =
| (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 @@ and subSgn' counterparts env strLoc sgn1 (sgn2 as (_, loc2)) =
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