Add an option to disable typeclass resolution during conversion, which

is has non-local effects. For now it is not disabled by default, but we'll
try to disable it once the test-suite and contribs are stabilized.

2 files changed, 21 insertions, 4 deletions

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 125517aec..dfaff327a 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -30,6 +30,18 @@ open Evd
 open Termops
 open Globnames
 
+let use_typeclasses_for_conversion = ref true
+
+let _ =
+  Goptions.declare_bool_option
+    { Goptions.optsync  = true;
+      optdepr  = false;
+      optname  = "use typeclass resolution during conversion";
+      optkey   = ["Typeclass"; "Resolution"; "For"; "Conversion"];
+      optread  = (fun () -> !use_typeclasses_for_conversion);
+      optwrite = (fun b -> use_typeclasses_for_conversion := b) }
+
+
 (* Typing operations dealing with coercions *)
 exception NoCoercion
 exception NoCoercionNoUnifier of evar_map * unification_error
@@ -371,7 +383,8 @@ 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 when not resolve_tc -> (evd, j)
+  | Not_found when not resolve_tc 
+    || not !use_typeclasses_for_conversion -> (evd, j)
   | Not_found ->
     try inh_app_fun env (saturate_evd env evd) j
     with Not_found -> (evd, j)
@@ -475,7 +488,7 @@ let inh_conv_coerce_to_gen resolve_tc rigidonly loc env evd cj t =
 	  coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t
 	else raise NoSubtacCoercion
       with
-      | NoSubtacCoercion when not resolve_tc ->
+      | NoSubtacCoercion when not resolve_tc || not !use_typeclasses_for_conversion ->
 	  error_actual_type_loc loc env best_failed_evd cj t e
       | NoSubtacCoercion ->
 	let evd' = saturate_evd env evd in
diff --git a/test-suite/bugs/opened/3325.v b/test-suite/bugs/opened/3325.v
index b4d1a79c0..b84b1fb18 100644
--- a/test-suite/bugs/opened/3325.v
+++ b/test-suite/bugs/opened/3325.v
@@ -1,3 +1,5 @@
+Unset Typeclass Resolution For Conversion.
+
 Typeclasses eauto := debug.
 Set Printing All.
 
@@ -14,6 +16,7 @@ Instance NatStateIs : StateIs := {
   valueType := nat;
   stateIs := fun _ => sp
 }.
+Canonical Structure NatStateIs.
 
 Class LogicOps F := { land: F -> F }.
 Instance : LogicOps SProp. Admitted.
@@ -26,7 +29,7 @@ Definition vn' := (@stateIs _ n).
 Definition GOOD : SProp :=
   @land _ _ vn'.
 (* This doesn't resolve, if PropLogicOps is defined later than SPropLogicOps *)
-Fail Definition BAD : SProp :=
+Definition BAD : SProp :=
   @land _ _ vn.
 
 
@@ -36,6 +39,7 @@ Instance: A Set. Admitted.
 
 Class B := { U : Type ; b : U }.
 Instance bi: B := {| U := nat ; b := 0 |}.
+Canonical Structure bi.
 
 Notation b0N := (@b _ : nat).
 Notation b0Ni := (@b bi : nat).
@@ -43,4 +47,4 @@ Definition b0D := (@b _ : nat).
 Definition GOOD1 := (@foo _ _ b0D).
 Definition GOOD2 := (let x := b0N in @foo _ _ x).
 Definition GOOD3 := (@foo _ _ b0Ni).
-Fail Definition BAD1 := (@foo _ _ b0N). (* Error: The term "b0Ni" has type "nat" while it is expected to have type "Set". *)
+Definition BAD1 := (@foo _ _ b0N). (* Error: The term "b0Ni" has type "nat" while it is expected to have type "Set". *)