diff options
author | 2014-12-11 02:05:41 -0500 | |
---|---|---|
committer | 2014-12-11 02:05:41 -0500 | |
commit | 7a2739b18042953cdfc608a5d9c96237c97cebba (patch) | |
tree | f9598f40d97e26581e6f9f4cb910f5e335f7b0e1 /src/elaborate.sml | |
parent | 219524359a25417b9e140130ab77a9a330c41012 (diff) | |
parent | d47f51e33733c851a53feb308ddaee3924910371 (diff) |
Merge.
Diffstat (limited to 'src/elaborate.sml')
-rw-r--r-- | src/elaborate.sml | 19 |
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)), |