Fixing the "IllTypedInstance" anomaly part of #5512.

It remains to accept resolving Type(u)<=Prop for u arbitrary sort variable.

3 files changed, 24 insertions, 5 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index cbf539c1e9..00d4c7b3d8 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1620,12 +1620,15 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 =
      in
       Success (solve_refl ~can_drop:true f flags env evd
                  (position_problem true pbty) evk1 args1 args2)
-  | Evar ev1, Evar ev2 when app_empty ->
+  | Evar (evk1,_ as ev1), Evar ev2 when app_empty ->
     (* solve_evar_evar handles the cases ev1 and/or ev2 are frozen *)
-      Success (solve_evar_evar ~force:true
+      (try
+        Success (solve_evar_evar ~force:true
                  (evar_define evar_unify flags ~choose:true)
                  evar_unify flags env evd
                  (position_problem true pbty) ev1 ev2)
+      with IllTypedInstance (env,t,u) ->
+            UnifFailure (evd,InstanceNotSameType (evk1,env,t,u)))
   | Evar ev1,_ when is_evar_allowed flags (fst ev1) && Array.length l1 <= Array.length l2 ->
       (* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *)
       (* and otherwise second-order matching *)
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 8ff2d7fc63..094dae4828 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -99,7 +99,9 @@ type conversion_check = unify_flags -> unification_kind ->
     Preconditions:
     - [ev] does not occur in [c].
     - [c] does not contain any Meta(_)
- *)
+
+    If [ev] and [c] have non inferably convertible types, an exception
+    [IllTypedInstance] is raised *)
 
 val instantiate_evar : unifier -> unify_flags -> env -> evar_map ->
   Evar.t -> constr -> evar_map
@@ -107,7 +109,9 @@ val instantiate_evar : unifier -> unify_flags -> env -> evar_map ->
 (** [evar_define choose env ev c] try to instantiate [ev] with [c] (typed in [env]),
    possibly solving related unification problems, possibly leaving open
    some problems that cannot be solved in a unique way (except if choose is
-   true); fails if the instance is not valid for the given [ev] *)
+   true); fails if the instance is not valid for the given [ev];
+   If [ev] and [c] have non inferably convertible types, an exception
+   [IllTypedInstance] is raised *)
 
 val evar_define : unifier -> unify_flags -> ?choose:bool -> ?imitate_defs:bool ->
   env -> evar_map -> bool option -> existential -> constr -> evar_map
@@ -129,6 +133,8 @@ val solve_evar_evar : ?force:bool ->
   (env -> evar_map -> bool option -> existential -> constr -> evar_map) ->
   unifier -> unify_flags ->
   env ->  evar_map -> bool option -> existential -> existential -> evar_map
+  (** The two evars are expected to be in inferably convertible types;
+      if not, an exception IllTypedInstance is raised *)
 
 val solve_simple_eqn : unifier -> unify_flags -> ?choose:bool -> ?imitate_defs:bool -> env ->  evar_map ->
   bool option * existential * constr -> unification_result
@@ -147,9 +153,9 @@ val noccur_evar : env -> evar_map -> Evar.t -> constr -> bool
 
 exception IllTypedInstance of env * types * types
 
-(* May raise IllTypedInstance if types are not convertible *)
 val check_evar_instance : unifier -> unify_flags ->
   env -> evar_map -> Evar.t -> constr -> evar_map
+  (** May raise IllTypedInstance if types are not convertible *)
 
 val remove_instance_local_defs :
   evar_map -> Evar.t -> 'a list -> 'a list
diff --git a/test-suite/bugs/closed/bug_5512.v b/test-suite/bugs/closed/bug_5512.v
new file mode 100644
index 0000000000..f885e31352
--- /dev/null
+++ b/test-suite/bugs/closed/bug_5512.v
@@ -0,0 +1,10 @@
+(* Check that an anomaly is not raised *)
+(* It should however eventually succeed... *)
+Goal exists x, x.
+Proof.
+simple refine (ex_intro _ _ _).
+shelve.
+(* The failure is due to Type(u)<=Prop for u an arbitrary sort
+   variable being rejected *)
+Fail simple refine (_ _).
+Abort.