TC: honor the use_typeclasses flag in pretyping

The coercion code was not seeing such flag and always trying
to resolve type classes.  In particular open_contr is pretyped
without type classes.

7 files changed, 46 insertions, 32 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index b0a4ebea4..104f26641 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -388,7 +388,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) =
 		let _ = e_cumul pb.env pb.evdref indt typ in
 		current
 	      else
-		(evd_comb2 (Coercion.inh_conv_coerce_to Loc.ghost pb.env)
+		(evd_comb2 (Coercion.inh_conv_coerce_to true Loc.ghost pb.env)
 		  pb.evdref (make_judge current typ) indt).uj_val in
 	    let sigma =  !(pb.evdref) in
 	    (current,try_find_ind pb.env sigma indt names))
@@ -1777,7 +1777,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
 let inh_conv_coerce_to_tycon loc env evdref j tycon =
   match tycon with
     | Some p ->
-	let (evd',j) = Coercion.inh_conv_coerce_to loc env !evdref j p in
+	let (evd',j) = Coercion.inh_conv_coerce_to true loc env !evdref j p in
           evdref := evd';
           j
     | None -> j
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 53fd925a2..d2c3282df 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -356,9 +356,11 @@ let inh_app_fun env evd j =
 	  with NoSubtacCoercion | NoCoercion ->
 	    (evd,j)
 
-let inh_app_fun env evd j =
+let inh_app_fun resolve_tc env evd j =
   try inh_app_fun env evd j
-  with Not_found ->
+  with
+  | Not_found when not resolve_tc -> (evd, j)
+  | Not_found ->
     try inh_app_fun env (saturate_evd env evd) j
     with Not_found -> (evd, j)
 
@@ -451,16 +453,19 @@ let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 =
       | _ -> raise (NoCoercionNoUnifier (best_failed_evd,e))
 
 (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
-let inh_conv_coerce_to_gen rigidonly loc env evd cj t =
+let inh_conv_coerce_to_gen resolve_tc rigidonly loc env evd cj t =
   let (evd', val') =
     try
       inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t
-    with NoCoercionNoUnifier _ ->
+    with NoCoercionNoUnifier (best_failed_evd,e) ->
       try
 	if Flags.is_program_mode () then
 	  coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t
 	else raise NoSubtacCoercion
-      with NoSubtacCoercion ->
+      with
+      | NoSubtacCoercion when not resolve_tc ->
+	  error_actual_type_loc loc env best_failed_evd cj t e
+      | NoSubtacCoercion ->
 	let evd = saturate_evd env evd in
       	  try
       	    inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t
@@ -470,8 +475,8 @@ let inh_conv_coerce_to_gen rigidonly loc env evd cj t =
   let val' = match val' with Some v -> v | None -> assert(false) in
     (evd',{ uj_val = val'; uj_type = t })
 
-let inh_conv_coerce_to = inh_conv_coerce_to_gen false
-let inh_conv_coerce_rigid_to = inh_conv_coerce_to_gen true
+let inh_conv_coerce_to resolve_tc = inh_conv_coerce_to_gen resolve_tc false
+let inh_conv_coerce_rigid_to resolve_tc = inh_conv_coerce_to_gen resolve_tc true
 
 let inh_conv_coerces_to loc env evd t t' =
   try
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index b397cc3d5..f5c548cc4 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -17,10 +17,12 @@ open Glob_term
 
 (** {6 Coercions. } *)
 
-(** [inh_app_fun env isevars j] coerces [j] to a function; i.e. it
+(** [inh_app_fun resolve_tc env isevars j] coerces [j] to a function; i.e. it
     inserts a coercion into [j], if needed, in such a way it gets as
-    type a product; it returns [j] if no coercion is applicable *)
-val inh_app_fun :
+    type a product; it returns [j] if no coercion is applicable.
+    resolve_tc=false disables resolving type classes (as the last
+    resort before failing) *)
+val inh_app_fun : bool ->
   env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment
 
 (** [inh_coerce_to_sort env isevars j] coerces [j] to a type; i.e. it
@@ -39,13 +41,15 @@ val inh_coerce_to_base : Loc.t ->
 val inh_coerce_to_prod : Loc.t ->
   env -> evar_map -> types -> evar_map * types
 
-(** [inh_conv_coerce_to Loc.t env isevars j t] coerces [j] to an object of type
-    [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and
-    [j.uj_type] are convertible; it fails if no coercion is applicable *)
-val inh_conv_coerce_to : Loc.t ->
+(** [inh_conv_coerce_to resolve_tc Loc.t env isevars j t] coerces [j] to an 
+    object of type [t]; i.e. it inserts a coercion into [j], if needed, in such
+    a way [t] and [j.uj_type] are convertible; it fails if no coercion is
+    applicable. resolve_tc=false disables resolving type classes (as the last
+    resort before failing) *)
+val inh_conv_coerce_to : bool -> Loc.t ->
   env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment
 
-val inh_conv_coerce_rigid_to : Loc.t ->
+val inh_conv_coerce_rigid_to : bool -> Loc.t ->
   env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment
 
 (** [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t]
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 74248301d..def8dbfb1 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -210,9 +210,10 @@ let evar_type_fixpoint loc env evdref lna lar vdefj =
       done
 
 (* coerce to tycon if any *)
-let inh_conv_coerce_to_tycon loc env evdref j = function
+let inh_conv_coerce_to_tycon resolve_tc loc env evdref j = function
   | None -> j
-  | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) evdref j t
+  | Some t ->
+      evd_comb2 (Coercion.inh_conv_coerce_to resolve_tc loc env) evdref j t
 
 (* used to enforce a name in Lambda when the type constraints itself
    is named, hence possibly dependent *)
@@ -293,7 +294,11 @@ let (f_genarg_interp, genarg_interp_hook) = Hook.make ()
 (* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *)
 (* in environment [env], with existential variables [evdref] and *)
 (* the type constraint tycon *)
-let rec pretype (tycon : type_constraint) env evdref lvar = function
+let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t =
+  let inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in
+  let pretype_type = pretype_type resolve_tc in
+  let pretype = pretype resolve_tc in
+  match t with
   | GRef (loc,ref) ->
       inh_conv_coerce_to_tycon loc env evdref
 	(pretype_ref loc evdref env ref)
@@ -452,7 +457,7 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function
 	| [] -> resj
 	| c::rest ->
 	    let argloc = loc_of_glob_constr c in
-	    let resj = evd_comb1 (Coercion.inh_app_fun env) evdref resj in
+	    let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc env) evdref resj in
             let resty = whd_betadeltaiota env !evdref resj.uj_type in
       	      match kind_of_term resty with
 	      | Prod (na,c1,c2) ->
@@ -730,7 +735,7 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function
       in inh_conv_coerce_to_tycon loc env evdref cj tycon
 
 (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *)
-and pretype_type valcon env evdref lvar = function
+and pretype_type resolve_tc valcon env evdref lvar = function
   | GHole (loc, knd, None) ->
       (match valcon with
        | Some v ->
@@ -750,7 +755,7 @@ and pretype_type valcon env evdref lvar = function
 	     { utj_val = e_new_evar evdref env ~src:(loc, knd) (mkSort s);
 	       utj_type = s})
   | c ->
-      let j = pretype empty_tycon env evdref lvar c in
+      let j = pretype resolve_tc empty_tycon env evdref lvar c in
       let loc = loc_of_glob_constr c in
       let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) evdref j in
 	match valcon with
@@ -765,11 +770,11 @@ let ise_pretype_gen flags sigma env lvar kind c =
   let evdref = ref sigma in
   let c' = match kind with
     | WithoutTypeConstraint ->
-        (pretype empty_tycon env evdref lvar c).uj_val
+        (pretype flags.use_typeclasses empty_tycon env evdref lvar c).uj_val
     | OfType exptyp ->
-	(pretype (mk_tycon exptyp) env evdref lvar c).uj_val
+	(pretype flags.use_typeclasses (mk_tycon exptyp) env evdref lvar c).uj_val
     | IsType ->
-	(pretype_type empty_valcon env evdref lvar c).utj_val 
+	(pretype_type flags.use_typeclasses empty_valcon env evdref lvar c).utj_val 
   in
   process_inference_flags flags env sigma (!evdref,c')
 
@@ -804,12 +809,12 @@ let on_judgment f j =
 
 let understand_judgment sigma env c =
   let evdref = ref sigma in
-  let j = pretype empty_tycon env evdref empty_lvar c in
+  let j = pretype true empty_tycon env evdref empty_lvar c in
   on_judgment (fun c ->
     snd (process_inference_flags all_and_fail_flags env sigma (!evdref,c))) j
 
 let understand_judgment_tcc evdref env c =
-  let j = pretype empty_tycon env evdref empty_lvar c in
+  let j = pretype true empty_tycon env evdref empty_lvar c in
   on_judgment (fun c ->
     let (evd,c) = process_inference_flags all_no_fail_flags env Evd.empty (!evdref,c) in
     evdref := evd; c) j
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index dd02423a8..6994723ac 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -105,11 +105,11 @@ val check_evars_are_solved :
 (**/**)
 (** Internal of Pretyping... *)
 val pretype :
-  type_constraint -> env -> evar_map ref ->
+  bool -> type_constraint -> env -> evar_map ref ->
   ltac_var_map -> glob_constr -> unsafe_judgment
 
 val pretype_type :
-  val_constraint -> env -> evar_map ref ->
+  bool -> val_constraint -> env -> evar_map ref ->
   ltac_var_map -> glob_constr -> unsafe_type_judgment
 
 val ise_pretype_gen :
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 4189741ba..5bb49c1c5 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -798,7 +798,7 @@ let is_mimick_head ts f =
 
 let try_to_coerce env evd c cty tycon =
   let j = make_judge c cty in
-  let (evd',j') = inh_conv_coerce_rigid_to Loc.ghost env evd j tycon in
+  let (evd',j') = inh_conv_coerce_rigid_to true Loc.ghost env evd j tycon in
   let evd' = Evarconv.consider_remaining_unif_problems env evd' in
   let evd' = Evd.map_metas_fvalue (nf_evar evd') evd' in
     (evd',j'.uj_val)
diff --git a/proofs/goal.ml b/proofs/goal.ml
index c40570c2c..4d1aa4124 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -193,7 +193,7 @@ module Refinable = struct
     let my_type = Retyping.get_type_of env !rdefs t in
     let j = Environ.make_judge t my_type in
     let (new_defs,j') =
-      Coercion.inh_conv_coerce_to (Loc.ghost) env !rdefs j typ
+      Coercion.inh_conv_coerce_to true (Loc.ghost) env !rdefs j typ
     in
     rdefs := new_defs;
     j'.Environ.uj_val