Coq: fix false existential problem

3 files changed, 17 insertions, 6 deletions

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 7a31465d..32a560ea 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1023,16 +1023,17 @@ let doc_exp_lem, doc_let_lem =
             (* Decide whether to unpack an existential result, pack one, or cast.
                To do this we compare the expected type stored in the checked expression
                with the inferred type. *)
-            let ret_typ_inst =
-              match infer_exp env (strip_exp full_exp) with
-              | typed_exp -> typ_of typed_exp
+            let inst =
+              match instantiation_of_without_type full_exp with
+              | x -> x
               (* Not all function applications can be inferred, so try falling back to the
                  type inferred when we know the target type.
                  TODO: there are probably some edge cases where this won't pick up a need
                  to cast. *)
-              | exception _ ->
-                 let inst = instantiation_of full_exp in
-                 let inst = KBindings.fold (fun k u m -> KBindings.add (orig_kid k) u m) inst KBindings.empty in
+              | exception _ -> instantiation_of full_exp
+            in
+            let inst = KBindings.fold (fun k u m -> KBindings.add (orig_kid k) u m) inst KBindings.empty in
+            let ret_typ_inst =
                  subst_unifiers inst ret_typ
             in
             let unpack,build_ex,autocast =
diff --git a/src/type_check.ml b/src/type_check.ml
index db85bf33..2d1241b9 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -3302,6 +3302,12 @@ and instantiation_of (E_aux (exp_aux, (l, _)) as exp) =
   | E_app (f, xs) -> snd (infer_funapp' l (Env.no_casts env) f (Env.get_val_spec f env) (List.map strip_exp xs) (Some (typ_of exp)))
   | _ -> invalid_arg ("instantiation_of expected application,  got " ^ string_of_exp exp)
 
+and instantiation_of_without_type (E_aux (exp_aux, (l, _)) as exp) =
+  let env = env_of exp in
+  match exp_aux with
+  | E_app (f, xs) -> snd (infer_funapp' l (Env.no_casts env) f (Env.get_val_spec f env) (List.map strip_exp xs) None)
+  | _ -> invalid_arg ("instantiation_of expected application,  got " ^ string_of_exp exp)
+
 and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ =
   let annot_exp exp typ eff = E_aux (exp, (l, Some (env, typ, eff))) in
   let switch_annot env typ = function
diff --git a/src/type_check.mli b/src/type_check.mli
index fd1ddb92..665981e9 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -355,6 +355,10 @@ val alpha_equivalent : Env.t -> typ -> typ -> bool
 (** Throws Invalid_argument if the argument is not a E_app expression *)
 val instantiation_of : tannot exp -> uvar KBindings.t
 
+(** Doesn't use the type of the expression when calculating instantiations.
+    May fail if the arguments aren't sufficient to calculate all unifiers. *)
+val instantiation_of_without_type : tannot exp -> uvar KBindings.t
+
 (* Type variable instantiations that inference will extract from constraints *)
 val instantiate_simple_equations : quant_item list -> uvar KBindings.t