Fix #10225 (Instance := {} accepts duplicate fields)

This replaces the mismatched context error, which occurred when
Instance := {} was used with strictly more fields than declared.

Since we later check that field names match those declared for the
instance, now that we reject duplicates we know that there are no
extra fields.

5 files changed, 4 insertions, 32 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index b64af52b6e..20402ebf95 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -281,9 +281,6 @@ let existing_instance glob g info =
                          ~hdr:"declare_instance"
                          (Pp.str "Constant does not build instances of a declared type class.")
 
-let mismatched_params env n m = Implicit_quantifiers.mismatched_ctx_inst_err env Parameters n m
-let mismatched_props env n m = Implicit_quantifiers.mismatched_ctx_inst_err env Properties n m
-
 (* Declare everything in the parameters as implicit, and the class instance as well *)
 
 let type_ctx_instance ~program_mode env sigma ctx inst subst =
@@ -479,9 +476,8 @@ let do_instance_interactive env sigma ?hook ~tac ~global ~poly cty k u ctx ctx'
 let do_instance env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imps subst id props =
   let term, termtype, sigma =
     match props with
-    | (true, { CAst.v = CRecord fs }) ->
-      if List.length fs > List.length k.cl_props then
-        mismatched_props env' (List.map snd fs) k.cl_props;
+    | (true, { CAst.v = CRecord fs; loc }) ->
+      check_duplicate ?loc fs;
       let subst, sigma = do_instance_type_ctx_instance fs k env' ctx' sigma ~program_mode:false subst in
       let term, termtype =
         do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in
@@ -502,9 +498,8 @@ let do_instance env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imp
 let do_instance_program env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imps subst id opt_props =
   let term, termtype, sigma =
     match opt_props with
-    | Some (true, { CAst.v = CRecord fs }) ->
-      if List.length fs > List.length k.cl_props then
-        mismatched_props env' (List.map snd fs) k.cl_props;
+    | Some (true, { CAst.v = CRecord fs; loc }) ->
+      check_duplicate ?loc fs;
       let subst, sigma =
         do_instance_type_ctx_instance fs k env' ctx' sigma ~program_mode:true subst in
      let term, termtype =
diff --git a/vernac/classes.mli b/vernac/classes.mli
index ace9096469..36c2d22c1d 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -14,12 +14,6 @@ open Constrexpr
 open Typeclasses
 open Libnames
 
-(** Errors *)
-
-val mismatched_params : env -> constr_expr list -> Constr.rel_context -> 'a
-
-val mismatched_props : env -> constr_expr list -> Constr.rel_context -> 'a
-
 (** Instance declaration *)
 
 val declare_instance : ?warn:bool -> env -> Evd.evar_map ->
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index 2bc95dbfcd..9733a751a8 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -66,8 +66,6 @@ let process_vernac_interp_error exn = match fst exn with
       wrap_vernac_error exn (Himsg.explain_prim_token_notation_error kind ctx sigma 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 ->
       wrap_vernac_error exn (Himsg.explain_inductive_error e)
   | Modops.ModuleTypingError e ->
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index a1f7835cbe..d10b704a48 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -1095,19 +1095,6 @@ 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 "."
 
-let pr_constr_exprs env sigma exprs =
-  hv 0 (List.fold_right
-         (fun d pps -> ws 2 ++ Ppconstr.pr_constr_expr env sigma d ++ pps)
-         exprs (mt ()))
-
-let explain_mismatched_contexts env c i j =
-  let sigma = Evd.from_env env in
-  let pm, pn = with_diffs (pr_rel_context env sigma j) (pr_constr_exprs env sigma i) in
-  str"Mismatched contexts while declaring instance: " ++ brk (1,1) ++
-    hov 1 (str"Expected:" ++ brk (1, 1) ++ pm) ++
-    fnl () ++ brk (1,1) ++
-    hov 1 (str"Found:" ++ brk (1, 1) ++ pn)
-
 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
diff --git a/vernac/himsg.mli b/vernac/himsg.mli
index d1c1c092e3..09384cb859 100644
--- a/vernac/himsg.mli
+++ b/vernac/himsg.mli
@@ -24,8 +24,6 @@ val explain_pretype_error : env -> Evd.evar_map -> pretype_error -> Pp.t
 
 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 -> Evd.evar_map -> typeclass_error -> Pp.t
 
 val explain_recursion_scheme_error : env -> recursion_scheme_error -> Pp.t