More on f9695eb4b, 827663982 on resolving #4782, #4813 (typing "with" clause).

When typing a "with clause fails, type classes are used to possibly
help to insert coercions. If this heuristic fails, do not consider it
anymore to be the best failure since it has made type classes choices
which may be inconsistent with other constraints and on which no
backtracking is possible anymore (see new example in test suite file
4782.v).

This does not mean that using type classes at this point is good. It
may find an instance which help to find a coercion, but which might
still be a choice of instance and coercion which is incompatible with
other constraints.

I tend to think that a convenient way to go to deal with the absence
of backtracking in inserting coercions would be to have special

For the record, here is a some comments of what happens regarding
f9695eb4b and 827663982.

In the presence of an instance (x:=t) given in a "with" clause, with
t:T, and x expected of type T', the situation is the following:

Before f9695eb4b:

- If T and T' are closed and T <= T' is not satisfiable (no coercion
  or not convertible), the test for possible insertion of a coercion
  is postponed to w_merge, even though there is no way to get more
  information since T ant T' are closed. As a result, t may be
  ill-typed and the unification may try to unify ill-formed terms,
  leading to #4872.

- If T and T' are not closed and contains evars of type a type class,
  inference of type classes is tried. If it fails, e.g. because a
  wrong type class instance is found, it was postponed to w_merge as
  above, and the test for coercion is retried now interleaved with
  type classes.

After f9695eb4b and 827663982e:

- If T and T' are closed and T <= T' is not satisfiable (no coercion
  or not convertible), the test for possible insertion of a coercion
  is an immediate failure. This fixes #4872.

- However, If T and T' are not closed and contains evars of type a
  type class, inference of type classes is tried. If it gives closed
  terms and fails, this is immediate failure without backtracking on
  type classes, resulting in the problem added here to file 4872.v.

The current fix does not consider the result of the use of type
classes while trying to insert a coercion to be the last word on
it. So, it fails with an error which is not the error for conversion
of closed terms (ConversionFailed), therefore in a way expected by
f9695eb4b and 827663982e, and the "with" typing problem is then
postponed again.

1 files changed, 1 insertions, 1 deletions

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index d00445958..71c55ae05 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -510,7 +510,7 @@ let inh_conv_coerce_to_gen resolve_tc rigidonly loc env evd cj t =
 	      error_actual_type_loc loc env best_failed_evd cj t e
 	    else 
       	      inh_conv_coerce_to_fail loc env evd' rigidonly (Some cj.uj_val) cj.uj_type t
-	  with NoCoercionNoUnifier (best_failed_evd,e) ->
+	  with NoCoercionNoUnifier (_evd,_error) ->
 	    error_actual_type_loc loc env best_failed_evd cj t e
   in
   let val' = match val' with Some v -> v | None -> assert(false) in