aboutsummaryrefslogtreecommitdiffhomepage
path: root/src/elaborate.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2014-12-05 19:41:27 -0500
committerGravatar Adam Chlipala <adam@chlipala.net>2014-12-05 19:41:27 -0500
commitb6df808b8ff4795f4523c39860070d6153cfad5d (patch)
treeccb61a8d0924daad1ac2f13bd19af21d80581c2b /src/elaborate.sml
parentb50cd7f9ddf5f7d8428ba79a0e336556389ac1c0 (diff)
Move code from last changeset, to improve performance
Diffstat (limited to 'src/elaborate.sml')
-rw-r--r--src/elaborate.sml19
1 files changed, 19 insertions, 0 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index c55dec01..749bd2f1 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -3020,6 +3020,25 @@ 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),
("sgn2", p_sgn env sgn2),
("sgis1", p_sgn env (L'.SgnConst sgis1, loc2)),