diff options
| author | Hugo Herbelin | 2020-11-14 16:46:19 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-16 11:43:27 +0100 |
| commit | daba2d7a4546a7d869fd4358b05ca488877bfe18 (patch) | |
| tree | d52205c4d8afebba56395c8fd2948879eb2cb200 /pretyping/evarconv.ml | |
| parent | 779d2b915a970cdfc87d3d1b69e10bab04094f33 (diff) | |
Fixing the "IllTypedInstance" anomaly part of #5512.
It remains to accept resolving Type(u)<=Prop for u arbitrary sort variable.
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 7 |
1 files changed, 5 insertions, 2 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 *) |