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, 34 insertions, 1 deletions

diff --git a/src/type_check.ml b/src/type_check.ml
index ad6b48b3..a5ffff43 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1678,6 +1678,39 @@ let instantiate_quant (v, arg) (QI_aux (aux, l) as qi) =
 let instantiate_quants quants unifier =
   List.map (instantiate_quant unifier) quants |> Util.option_these
 
+(* During typechecking, we can run into the following issue, where we
+   have a function like
+
+   val and_bool : forall ('p : Bool) ('q : Bool). (bool('p), bool('q)) -> bool('p & 'q)
+
+   and we want to check something like Q & P <= bool(X & Y)
+
+   where Q => bool(Y) & P => bool(X)
+
+   if we instantiate using the return type (which is usually good)
+   we'll run into the situtation where we have to check bool(Y)
+   subtype bool(X) because the quantifiers will get instantiated in
+   the wrong order, despite the expression being otherwise well-typed
+   the trick here is to recognise that we shouldn't unify on goals in
+   certain ambiguous positions in types. In this case with and_bool,
+   they'll be unambigiously unified with the argument types so it's
+   better to just not bother with the return type.
+*)
+let rec ambiguous_vars (Typ_aux (aux, _)) =
+  match aux with
+  | Typ_app (_, args) -> List.fold_left KidSet.union KidSet.empty (List.map ambiguous_arg_vars args)
+  | _ -> KidSet.empty
+  
+and ambiguous_arg_vars (A_aux (aux, _)) =
+  match aux with
+  | A_bool nc -> ambiguous_nc_vars nc
+  | _ -> KidSet.empty
+               
+and ambiguous_nc_vars (NC_aux (aux, _)) =
+  match aux with
+  | NC_and (nc1, nc2) -> KidSet.union (tyvars_of_constraint nc1) (tyvars_of_constraint nc2)
+  | _ -> KidSet.empty
+               
 (**************************************************************************)
 (* 3.5. Subtyping with existentials                                       *)
 (**************************************************************************)
@@ -3508,7 +3541,7 @@ and infer_funapp' l env f (typq, f_typ) xs expected_ret_typ =
     | Some expect ->
        let goals = quant_kopts (mk_typquant !quants) |> List.map kopt_kid |> KidSet.of_list in
        try
-         let unifiers = unify l env goals !typ_ret expect in
+         let unifiers = unify l env (KidSet.diff goals (ambiguous_vars !typ_ret)) !typ_ret expect in
          record_unifiers unifiers;
          let unifiers = KBindings.bindings unifiers in
          typ_debug (lazy (Util.("Unifiers " |> magenta |> clear)