summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2014-12-04 20:22:39 -0500
committerGravatar Adam Chlipala <adam@chlipala.net>2014-12-04 20:22:39 -0500
commitb50cd7f9ddf5f7d8428ba79a0e336556389ac1c0 (patch)
treedfe6b1e1c5fe0196d35c033b135aa8e341e01c26
parent514bde72c4a3f291221bbb362b9496c020042925 (diff)
In checking signature subsumption, be sure to try constraints last.
-rw-r--r--src/elab_env.sml19
1 files changed, 18 insertions, 1 deletions
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 9fbe7bd7..711db166 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -1114,7 +1114,24 @@ and hnormSgn env (all as (sgn, loc)) =
case sgn of
SgnError => all
| SgnVar n => hnormSgn env (#2 (lookupSgnNamed env n))
- | SgnConst _ => all
+ | SgnConst sgis =>
+ 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 (constraint, others) = List.partition
+ (fn (SgiConstraint _, _) => true
+ | _ => false) sgis
+ in
+ case constraint of
+ [] => all
+ | _ => (SgnConst (others @ constraint), loc)
+ end
| SgnFun _ => all
| SgnProj (m, ms, x) =>
let