Fix #9631: Instance: anomaly grounding non evar-free term

8 files changed, 30 insertions, 22 deletions

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index d732544c5c..1496712bbc 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -124,12 +124,14 @@ let typeclass_univ_instance (cl, u) =
 
 let class_info c =
   try GlobRef.Map.find c !classes
-  with Not_found -> not_a_class (Global.env()) (EConstr.of_constr (printable_constr_of_global c))
+  with Not_found ->
+    let env = Global.env() in
+    not_a_class env (Evd.from_env env) (EConstr.of_constr (printable_constr_of_global c))
 
 let global_class_of_constr env sigma c =
   try let gr, u = Termops.global_of_constr sigma c in
-	class_info gr, u
-  with Not_found -> not_a_class env c
+    GlobRef.Map.find gr !classes, u
+  with Not_found -> not_a_class env sigma c
 
 let dest_class_app env sigma c =
   let cl, args = EConstr.decompose_app sigma c in
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index 2720a3e4de..af5b3016c9 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -20,10 +20,10 @@ type typeclass_error =
     | NotAClass of constr
     | UnboundMethod of GlobRef.t * lident (* Class name, method *)
 
-exception TypeClassError of env * typeclass_error
+exception TypeClassError of env * Evd.evar_map * typeclass_error
 
-let typeclass_error env err = raise (TypeClassError (env, err))
+let typeclass_error env sigma err = raise (TypeClassError (env, sigma, err))
 
-let not_a_class env c = typeclass_error env (NotAClass c)
+let not_a_class env sigma c = typeclass_error env sigma (NotAClass c)
 
-let unbound_method env cid id = typeclass_error env (UnboundMethod (cid, id))
+let unbound_method env sigma cid id = typeclass_error env sigma (UnboundMethod (cid, id))
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index 9831627a9a..fd75781ed5 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -18,9 +18,10 @@ type typeclass_error =
   | NotAClass of constr
   | UnboundMethod of GlobRef.t * lident (** Class name, method *)
 
-exception TypeClassError of env * typeclass_error
+exception TypeClassError of env * Evd.evar_map * typeclass_error
 
-val not_a_class : env -> constr -> 'a
+val typeclass_error : env -> Evd.evar_map -> typeclass_error -> 'a
 
-val unbound_method : env -> GlobRef.t -> lident -> 'a
+val not_a_class : env -> Evd.evar_map -> constr -> 'a
 
+val unbound_method : env -> Evd.evar_map -> GlobRef.t -> lident -> 'a
diff --git a/test-suite/bugs/closed/bug_9631.v b/test-suite/bugs/closed/bug_9631.v
new file mode 100644
index 0000000000..8afeccccd4
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9631.v
@@ -0,0 +1,7 @@
+
+Fail Instance x : _.
+
+Existing Class True.
+(* the type is checked for typeclass-ness before interping the body so
+   this is the same error *)
+Fail Instance x : _ := I.
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 39c086eff5..306b5d9f0e 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -234,7 +234,7 @@ let do_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode ct
       in
       match rest with
       | (n, _) :: _ ->
-        unbound_method env' k.cl_impl (get_id n)
+        unbound_method env' sigma k.cl_impl (get_id n)
       | _ ->
         let kcl_props = List.map (Termops.map_rel_decl of_constr) k.cl_props in
         let sigma, res = type_ctx_instance ~program_mode (push_rel_context ctx' env') sigma kcl_props props subst in
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index 06428b53f2..2bc95dbfcd 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -64,8 +64,8 @@ let process_vernac_interp_error exn = match fst exn with
       wrap_vernac_error exn (Himsg.explain_pretype_error ctx sigma te)
   | Notation.PrimTokenNotationError(kind,ctx,sigma,te) ->
       wrap_vernac_error exn (Himsg.explain_prim_token_notation_error kind ctx sigma te)
-  | Typeclasses_errors.TypeClassError(env, te) ->
-      wrap_vernac_error exn (Himsg.explain_typeclass_error env te)
+  | Typeclasses_errors.TypeClassError(env, sigma, te) ->
+      wrap_vernac_error exn (Himsg.explain_typeclass_error env sigma te)
   | Implicit_quantifiers.MismatchedContextInstance(e,c,l,x) ->
     wrap_vernac_error exn (Himsg.explain_mismatched_contexts e c l x)
   | InductiveError e ->
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 9dd321be51..9e92d936d2 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -1039,12 +1039,10 @@ let explain_module_internalization_error = function
 
 (* Typeclass errors *)
 
-let explain_not_a_class env c =
-  let sigma = Evd.from_env env in
-  let c = EConstr.to_constr sigma c in
-  pr_constr_env env sigma c ++ str" is not a declared type class."
+let explain_not_a_class env sigma c =
+  pr_econstr_env env sigma c ++ str" is not a declared type class."
 
-let explain_unbound_method env cid { CAst.v = id } =
+let explain_unbound_method env sigma cid { CAst.v = id } =
   str "Unbound method name " ++ Id.print (id) ++ spc () ++
   str"of class" ++ spc () ++ pr_global cid ++ str "."
 
@@ -1059,9 +1057,9 @@ let explain_mismatched_contexts env c i j =
     fnl () ++ brk (1,1) ++
     hov 1 (str"Found:" ++ brk (1, 1) ++ pr_constr_exprs i)
 
-let explain_typeclass_error env = function
-  | NotAClass c -> explain_not_a_class env c
-  | UnboundMethod (cid, id) -> explain_unbound_method env cid id
+let explain_typeclass_error env sigma = function
+  | NotAClass c -> explain_not_a_class env sigma c
+  | UnboundMethod (cid, id) -> explain_unbound_method env sigma cid id
 
 (* Refiner errors *)
 
diff --git a/vernac/himsg.mli b/vernac/himsg.mli
index f22354cdbf..d0f42ea16b 100644
--- a/vernac/himsg.mli
+++ b/vernac/himsg.mli
@@ -26,7 +26,7 @@ val explain_inductive_error : inductive_error -> Pp.t
 
 val explain_mismatched_contexts : env -> contexts -> Constrexpr.constr_expr list -> Constr.rel_context -> Pp.t
 
-val explain_typeclass_error : env -> typeclass_error -> Pp.t
+val explain_typeclass_error : env -> Evd.evar_map -> typeclass_error -> Pp.t
 
 val explain_recursion_scheme_error : env -> recursion_scheme_error -> Pp.t