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

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

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))

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

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.

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

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 ->

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 *)
 

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