Mercurial > urweb

changeset 2086:3d22f761a4b7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
In checking signature subsumption, be sure to try constraints last.
author Adam Chlipala <adam@chlipala.net>
date Thu, 04 Dec 2014 20:22:39 -0500
parents fd6d362666c0
children 834b438d57f3
files src/elab_env.sml
diffstat 1 files changed, 18 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/src/elab_env.sml	Thu Dec 04 19:54:04 2014 -0500
+++ b/src/elab_env.sml	Thu Dec 04 20:22:39 2014 -0500
@@ -1114,7 +1114,24 @@
     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