From a7ea32fbf3829d1ce39ce9cc24b71791727090c5 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 26 Jun 2016 23:29:55 +0200 Subject: 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. --- pretyping/coercion.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping') 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 -- cgit v1.2.3