Avoid unification on ambiguous return types

Usually we want to unify on return types, but in the case of
constraint unification (especially during rewriting) we can find
ourselves in the situation where unifying too eagerly on a return
type like bool('p & 'q) can cause us to instantiate 'p and 'q in the
wrong order (as & should really respect commutativity and
associativity during typechecking to avoid being overly brittle).

Originally I simply avoided adding cases for unify on NC_and/NC_or
and similar to avoid these cases, but this lead to the undesirable
situation where identical types wouldn't unify with each other for
an empty set of goals, which should be a trivial property of the
unification functions.

The solution is therefore to identify type variables in ambiguous
positions, and remove them from the list of goals during
unification. All type variables still have to be resolved by the
time we finish checking each application, but this has the added
bonus of making order much less important when it comes to
instantiating type variables.

Currently I am overly conservative about what qualifies as
ambigious, but this set should be expanded

1 files changed, 5 insertions, 5 deletions

diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail
index 505ca7b6..98318dd4 100755
--- a/aarch64/prelude.sail
+++ b/aarch64/prelude.sail
@@ -127,7 +127,7 @@ val and_vec = {lem: "and_vec", c: "and_bits", coq: "and_vec"} : forall 'n. (bits
 
 function and_vec (xs, ys) = builtin_and_vec(xs, ys)
 
-overload operator & = {and_bool, and_vec}
+overload operator & = {and_vec}
 
 val builtin_or_vec = {ocaml: "or_vec", c: "or_bits"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
@@ -264,19 +264,19 @@ val Sqrt = {ocaml: "sqrt_real", lem: "realSqrt", c: "sqrt_real", coq: "sqrt"} :
 
 val gteq_real = {ocaml: "gteq_real", lem: "gteq", c: "gteq_real", coq: "gteq_real"} : (real, real) -> bool
 
-overload operator >= = {gteq_atom, gteq_int, gteq_real}
+overload operator >= = {gteq_real}
 
 val lteq_real = {ocaml: "lteq_real", lem: "lteq", c: "lteq_real", coq: "lteq_real"} : (real, real) -> bool
 
-overload operator <= = {lteq_atom, lteq_int, lteq_real}
+overload operator <= = {lteq_real}
 
 val gt_real = {ocaml: "gt_real", lem: "gt", c: "gt_real", coq: "gt_real"} : (real, real) -> bool
 
-overload operator > = {gt_atom, gt_int, gt_real}
+overload operator > = {gt_real}
 
 val lt_real = {ocaml: "lt_real", lem: "lt", c: "lt_real", coq: "lt_real"} : (real, real) -> bool
 
-overload operator < = {lt_atom, lt_int, lt_real}
+overload operator < = {lt_real}
 
 val RoundDown = {ocaml: "round_down", lem: "realFloor", c: "round_down", coq: "Zfloor"} : real -> int