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.

12 files changed, 17 insertions, 47 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 4c8aff3f2e..63c936fa81 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1299,7 +1299,7 @@ let find_pattern_variable qid =
   if qualid_is_ident qid then qualid_basename qid
   else raise (InternalizationError(qid.CAst.loc,NotAConstructor qid))
 
-let check_duplicate loc fields =
+let check_duplicate ?loc fields =
   let eq (ref1, _) (ref2, _) = qualid_eq ref1 ref2 in
   let dups = List.duplicates eq fields in
   match dups with
@@ -1344,7 +1344,7 @@ let sort_fields ~complete loc fields completer =
           try Nametab.shortest_qualid_of_global ?loc Id.Set.empty global_record_id
           with Not_found ->
             anomaly (str "Environment corruption for records.") in
-        let () = check_duplicate loc fields in
+        let () = check_duplicate ?loc fields in
         let (end_index,    (* one past the last field index *)
              first_field_index,  (* index of the first field of the record *)
              proj_list)    (* list of projections *)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 0d4bc91f57..2e4d7479a9 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -189,3 +189,7 @@ val for_grammar : ('a -> 'b) -> 'a -> 'b
 
 (** Placeholder for global option, should be moved to a parameter *)
 val get_asymmetric_patterns : unit -> bool
+
+val check_duplicate : ?loc:Loc.t -> (qualid * constr_expr) list -> unit
+(** Check that a list of record field definitions doesn't contain
+    duplicates. *)
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index e8d10488b2..32290f0430 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -23,9 +23,6 @@ open Libobject
 open Nameops
 open Context.Rel.Declaration
 
-exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Constr.rel_context (* found, expected *)
-let mismatched_ctx_inst_err env c n m = raise (MismatchedContextInstance (env, c, n, m))
-
 module RelDecl = Context.Rel.Declaration
 (*i*)
 
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index d28d35f3a1..8536a2dee0 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -30,7 +30,3 @@ val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t
 val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits
 
 val implicit_application : Id.Set.t -> constr_expr -> constr_expr * Id.Set.t
-
-(* Should be likely located elsewhere *)
-exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Constr.rel_context (* found, expected *)
-val mismatched_ctx_inst_err : Environ.env -> Typeclasses_errors.contexts -> constr_expr list -> Constr.rel_context -> 'a
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index af5b3016c9..90ecab1608 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -8,13 +8,9 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(*i*)
 open Names
 open EConstr
 open Environ
-(*i*)
-
-type contexts = Parameters | Properties
 
 type typeclass_error =
     | NotAClass of constr
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index fd75781ed5..21bb5f8443 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -12,8 +12,6 @@ open Names
 open EConstr
 open Environ
 
-type contexts = Parameters | Properties
-
 type typeclass_error =
   | NotAClass of constr
   | UnboundMethod of GlobRef.t * lident (** Class name, method *)
diff --git a/test-suite/bugs/closed/bug_10225.v b/test-suite/bugs/closed/bug_10225.v
new file mode 100644
index 0000000000..6d6bb39a65
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10225.v
@@ -0,0 +1,7 @@
+
+Class Bar := {}.
+Instance bb : Bar := {}.
+
+Class Foo := { xx : Bar; foo : nat }.
+
+Fail Instance bar : Foo := { foo := 1 + 1; foo := 2 + 2 }.
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