Standardize handling of Automatic Introduction.

This fixes #8791.
We explicitly specify for intro the names of binders which are
given by the user. This still can suffer from spurious collisions,
see #8819.

6 files changed, 27 insertions, 9 deletions

diff --git a/CHANGES.md b/CHANGES.md
index 91763ba35c..267a2e2d32 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -52,6 +52,9 @@ Vernacular commands
 - `Combined Scheme` can now work when inductive schemes are generated in sort
   `Type`. It used to be limited to sort `Prop`.
 
+- Binders for an `Instance` now act more like binders for a `Theorem`.
+  Names may not be repeated, and may not overlap with section variable names.
+
 Tools
 
 - The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values:
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5cead11a5c..1646906daa 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1062,6 +1062,12 @@ let intros_replacing ids =
       (Tacticals.New.tclMAP (fun (id,pos) -> intro_move (Some id) pos) posl)
   end
 
+(* The standard for implementing Automatic Introduction *)
+let auto_intros_tac ids =
+  Tacticals.New.tclMAP (function
+      | Name id -> intro_mustbe_force id
+      | Anonymous -> intro) (List.rev ids)
+
 (* User-level introduction tactics *)
 
 let lookup_hypothesis_as_renamed env sigma ccl = function
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 7efadb2c28..b298524ff8 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -70,6 +70,9 @@ val intros_using         : Id.t list -> unit Proofview.tactic
 val intros_replacing     : Id.t list -> unit Proofview.tactic
 val intros_possibly_replacing : Id.t list -> unit Proofview.tactic
 
+(** [auto_intros_tac names] handles Automatic Introduction of binders *)
+val auto_intros_tac : Names.Name.t list -> unit Proofview.tactic
+
 val intros               : unit Proofview.tactic
 
 (** [depth_of_quantified_hypothesis b h g] returns the index of [h] in
diff --git a/test-suite/bugs/closed/bug_8791.v b/test-suite/bugs/closed/bug_8791.v
new file mode 100644
index 0000000000..9be1936cdf
--- /dev/null
+++ b/test-suite/bugs/closed/bug_8791.v
@@ -0,0 +1,9 @@
+Class Inhabited (A : Type) : Type := populate { inhabitant : A }.
+
+Definition A := 42.
+
+Instance foo (A: Type): Inhabited (list A).
+Check A.
+Abort.
+
+Fail Instance foo (A : nat) (A : Type) : Inhabited nat.
diff --git a/vernac/classes.ml b/vernac/classes.ml
index f4b0015851..39919a141a 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -146,7 +146,7 @@ let do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imp
   Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma);
   instance_hook k pri global imps ?hook (ConstRef cst); id
 
-let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl len term termtype =
+let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl ids term termtype =
   let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
   if program_mode then
     let hook _ _ vis gr =
@@ -189,10 +189,10 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id
           in
           ignore (Pfedit.by init_refine)
         else if Flags.is_auto_intros () then
-          ignore (Pfedit.by (Tacticals.New.tclDO len Tactics.intro));
+          ignore (Pfedit.by (Tactics.auto_intros_tac ids));
         (match tac with Some tac -> ignore (Pfedit.by tac) | None -> ())) ()
 
-let do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props len =
+let do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props =
   let props =
     match props with
     | Some (true, { CAst.v = CRecord fs }) ->
@@ -275,7 +275,7 @@ let do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~pro
   if not (Evd.has_undefined sigma) && not (Option.is_empty term) then
     declare_instance_constant k pri global imps ?hook id decl poly sigma (Option.get term) termtype
   else if program_mode || refine || Option.is_empty term then
-    declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl len term termtype
+    declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl (List.map RelDecl.get_name ctx) term termtype
   else CErrors.user_err Pp.(str "Unsolved obligations remaining.");
   id
 
@@ -341,7 +341,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) ~
     do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imps subst id
   else
     do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode
-      cty k u ctx ctx' pri decl imps subst id props len
+      cty k u ctx ctx' pri decl imps subst id props
 
 let named_of_rel_context l =
   let open Vars in
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 8aa459729c..9019fa15d5 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -368,10 +368,7 @@ let rec_tac_initializer finite guard thms snl =
        | _ -> assert false
 
 let start_proof_with_initialization kind sigma decl recguard thms snl hook =
-  let intro_tac (_, (_, (ids, _))) =
-    Tacticals.New.tclMAP (function
-    | Name id -> Tactics.intro_mustbe_force id
-    | Anonymous -> Tactics.intro) (List.rev ids) in
+  let intro_tac (_, (_, (ids, _))) = Tactics.auto_intros_tac ids in
   let init_tac,guard = match recguard with
   | Some (finite,guard,init_tac) ->
       let rec_tac = rec_tac_initializer finite guard thms snl in