Merge PR #13188: Default disable automatic generalization of Instance type

Ack-by: Blaisorblade
Reviewed-by: JasonGross
Reviewed-by: Zimmi48
Ack-by: jfehrle
Reviewed-by: ppedrot

12 files changed, 75 insertions, 45 deletions

diff --git a/doc/changelog/02-specification-language/13188-instance-gen.rst b/doc/changelog/02-specification-language/13188-instance-gen.rst
new file mode 100644
index 0000000000..6a431f85ed
--- /dev/null
+++ b/doc/changelog/02-specification-language/13188-instance-gen.rst
@@ -0,0 +1,6 @@
+- **Removed:** The type given to :cmd:`Instance` is no longer automatically
+  generalized over unbound and :ref:`generalizable <implicit-generalization>` variables.
+  Use :n:`Instance : \`{@type}` instead of :n:`Instance : @type` to get the old behaviour, or
+  enable the compatibility flag :flag:`Instance Generalized Output`.
+  (`#13188 <https://github.com/coq/coq/pull/13188>`_, fixes `#6042
+  <https://github.com/coq/coq/issues/6042>`_, by Gaëtan Gilbert).
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 56d90b33d8..2474c784b8 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -391,6 +391,16 @@ Summary of the commands
       equivalent to ``Hint Resolve ident : typeclass_instances``, except it
       registers instances for :cmd:`Print Instances`.
 
+   .. flag:: Instance Generalized Output
+
+      .. deprecated:: 8.13
+
+      Disabled by default, this provides compatibility with Coq
+      version 8.12 and earlier.
+
+      When enabled, the type of the instance is implicitly generalized
+      over unbound and :ref:`generalizable <implicit-generalization>` variables as though surrounded by ``\`{}``.
+
 .. cmd:: Print Instances @reference
 
    Shows the list of instances associated with the typeclass :token:`reference`.
diff --git a/test-suite/bugs/closed/bug_3513.v b/test-suite/bugs/closed/bug_3513.v
index 462a615d91..f3a19c2b89 100644
--- a/test-suite/bugs/closed/bug_3513.v
+++ b/test-suite/bugs/closed/bug_3513.v
@@ -13,7 +13,7 @@ Infix "|--"  := lentails (at level 79, no associativity).
 Class ILogic Frm {ILOps: ILogicOps Frm} := { lentailsPre:> PreOrder lentails }.
 Definition lequiv `{ILogic Frm} P Q := P |-- Q /\ Q |-- P.
 Infix "-|-"  := lequiv (at level 85, no associativity).
-Instance lequiv_inverse_lentails `{ILogic Frm} : subrelation lequiv (inverse lentails) := admit.
+Instance lequiv_inverse_lentails `{ILogic Frm} {inverse} : subrelation lequiv (inverse lentails) := admit.
 Record ILFunFrm (T : Type) `{e : Equiv T} `{ILOps : ILogicOps Frm} := mkILFunFrm { ILFunFrm_pred :> T -> Frm }.
 Section ILogic_Fun.
   Context (T: Type) `{TType: type T}.
diff --git a/test-suite/bugs/closed/bug_4095.v b/test-suite/bugs/closed/bug_4095.v
index d667022e68..2d4d7d02cc 100644
--- a/test-suite/bugs/closed/bug_4095.v
+++ b/test-suite/bugs/closed/bug_4095.v
@@ -15,7 +15,7 @@ Infix "|--"  := lentails (at level 79, no associativity).
 Class ILogic Frm {ILOps: ILogicOps Frm} := { lentailsPre:> PreOrder lentails }.
 Definition lequiv `{ILogic Frm} P Q := P |-- Q /\ Q |-- P.
 Infix "-|-"  := lequiv (at level 85, no associativity).
-Instance lequiv_inverse_lentails `{ILogic Frm} : subrelation lequiv (inverse lentails) := admit.
+Instance lequiv_inverse_lentails `{ILogic Frm} {inverse} : subrelation lequiv (inverse lentails) := admit.
 Record ILFunFrm (T : Type) `{e : Equiv T} `{ILOps : ILogicOps Frm} := mkILFunFrm { ILFunFrm_pred :> T -> Frm }.
 Section ILogic_Fun.
   Context (T: Type) `{TType: type T}.
diff --git a/test-suite/bugs/closed/bug_6042.v b/test-suite/bugs/closed/bug_6042.v
new file mode 100644
index 0000000000..72f612560b
--- /dev/null
+++ b/test-suite/bugs/closed/bug_6042.v
@@ -0,0 +1,7 @@
+Class C (n: nat) := T{x:True}.
+Generalizable All Variables.
+
+Fail Instance i : C n.
+
+Instance i : `(C n).
+Proof. repeat constructor. Defined.
diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v
index 9a3a1d3709..aae24e0e0a 100644
--- a/theories/Classes/CMorphisms.v
+++ b/theories/Classes/CMorphisms.v
@@ -1,4 +1,4 @@
-(* -*- coding: utf-8; coq-prog-args: ("-coqlib" "../.." "-R" ".." "Coq" "-top" "Coq.Classes.CMorphisms") -*- *)
+(* -*- coding: utf-8; coq-prog-args: ("-top" "Coq.Classes.CMorphisms") -*- *)
 (************************************************************************)
 (*         *   The Coq Proof Assistant / The Coq Development Team       *)
 (*  v      *         Copyright INRIA, CNRS and contributors             *)
@@ -308,7 +308,7 @@ Section GenericInstances.
 
   Global Program 
   Instance trans_contra_inv_impl_type_morphism
-  `(Transitive A R) : Proper (R --> flip arrow) (R x) | 3.
+  `(Transitive A R) {x} : Proper (R --> flip arrow) (R x) | 3.
 
   Next Obligation.
   Proof with auto.
@@ -318,7 +318,7 @@ Section GenericInstances.
 
   Global Program 
   Instance trans_co_impl_type_morphism
-    `(Transitive A R) : Proper (R ++> arrow) (R x) | 3.
+    `(Transitive A R) {x} : Proper (R ++> arrow) (R x) | 3.
 
   Next Obligation.
   Proof with auto.
@@ -328,7 +328,7 @@ Section GenericInstances.
 
   Global Program 
   Instance trans_sym_co_inv_impl_type_morphism
-    `(PER A R) : Proper (R ++> flip arrow) (R x) | 3.
+    `(PER A R) {x} : Proper (R ++> flip arrow) (R x) | 3.
 
   Next Obligation.
   Proof with auto.
@@ -337,7 +337,7 @@ Section GenericInstances.
   Qed.
 
   Global Program Instance trans_sym_contra_arrow_morphism
-    `(PER A R) : Proper (R --> arrow) (R x) | 3.
+    `(PER A R) {x} : Proper (R --> arrow) (R x) | 3.
 
   Next Obligation.
   Proof with auto.
@@ -346,7 +346,7 @@ Section GenericInstances.
   Qed.
 
   Global Program Instance per_partial_app_type_morphism
-  `(PER A R) : Proper (R ==> iffT) (R x) | 2.
+  `(PER A R) {x} : Proper (R ==> iffT) (R x) | 2.
 
   Next Obligation.
   Proof with auto.
@@ -399,17 +399,17 @@ Section GenericInstances.
   (** Coq functions are morphisms for Leibniz equality,
      applied only if really needed. *)
 
-  Global Instance reflexive_eq_dom_reflexive `(Reflexive B R') :
+  Global Instance reflexive_eq_dom_reflexive `(Reflexive B R') {A} :
     Reflexive (@Logic.eq A ==> R').
   Proof. simpl_crelation. Qed.
 
   (** [respectful] is a morphism for crelation equivalence . *)
 
-  Global Instance respectful_morphism :
+  Global Instance respectful_morphism {A B} :
     Proper (relation_equivalence ++> relation_equivalence ++> relation_equivalence) 
            (@respectful A B).
   Proof. 
-    intros A B R R' HRR' S S' HSS' f g. 
+    intros R R' HRR' S S' HSS' f g.
     unfold respectful , relation_equivalence in *; simpl in *.
     split ; intros H x y Hxy.
     - apply (fst (HSS' _ _)). apply H. now apply (snd (HRR' _ _)).
@@ -511,9 +511,9 @@ Ltac partial_application_tactic :=
 
 (** Bootstrap !!! *)
 
-Instance proper_proper : Proper (relation_equivalence ==> eq ==> iffT) (@Proper A).
+Instance proper_proper {A} : Proper (relation_equivalence ==> eq ==> iffT) (@Proper A).
 Proof.
-  intros A R R' HRR' x y <-. red in HRR'.
+  intros R R' HRR' x y <-. red in HRR'.
   split ; red ; intros. 
   - now apply (fst (HRR' _ _)).
   - now apply (snd (HRR' _ _)).
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index c70e3fe478..867d9cb9b3 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -1,4 +1,4 @@
-(* -*- coding: utf-8; coq-prog-args: ("-coqlib" "../.." "-R" ".." "Coq" "-top" "Coq.Classes.Morphisms") -*- *)
+(* -*- coding: utf-8; coq-prog-args: ("-top" "Coq.Classes.Morphisms") -*- *)
 (************************************************************************)
 (*         *   The Coq Proof Assistant / The Coq Development Team       *)
 (*  v      *         Copyright INRIA, CNRS and contributors             *)
@@ -309,7 +309,7 @@ Section GenericInstances.
 
   Global Program 
   Instance trans_contra_inv_impl_morphism
-  `(Transitive A R) : Proper (R --> flip impl) (R x) | 3.
+  `(Transitive A R) {x} : Proper (R --> flip impl) (R x) | 3.
 
   Next Obligation.
   Proof with auto.
@@ -319,7 +319,7 @@ Section GenericInstances.
 
   Global Program 
   Instance trans_co_impl_morphism
-    `(Transitive A R) : Proper (R ++> impl) (R x) | 3.
+    `(Transitive A R) {x} : Proper (R ++> impl) (R x) | 3.
 
   Next Obligation.
   Proof with auto.
@@ -329,7 +329,7 @@ Section GenericInstances.
 
   Global Program 
   Instance trans_sym_co_inv_impl_morphism
-    `(PER A R) : Proper (R ++> flip impl) (R x) | 3.
+    `(PER A R) {x} : Proper (R ++> flip impl) (R x) | 3.
 
   Next Obligation.
   Proof with auto.
@@ -338,7 +338,7 @@ Section GenericInstances.
   Qed.
 
   Global Program Instance trans_sym_contra_impl_morphism
-    `(PER A R) : Proper (R --> impl) (R x) | 3.
+    `(PER A R) {x} : Proper (R --> impl) (R x) | 3.
 
   Next Obligation.
   Proof with auto.
@@ -347,7 +347,7 @@ Section GenericInstances.
   Qed.
 
   Global Program Instance per_partial_app_morphism
-  `(PER A R) : Proper (R ==> iff) (R x) | 2.
+  `(PER A R) {x} : Proper (R ==> iff) (R x) | 2.
 
   Next Obligation.
   Proof with auto.
@@ -520,9 +520,9 @@ Ltac partial_application_tactic :=
 
 (** Bootstrap !!! *)
 
-Instance proper_proper : Proper (relation_equivalence ==> eq ==> iff) (@Proper A).
+Instance proper_proper {A} : Proper (relation_equivalence ==> eq ==> iff) (@Proper A).
 Proof.
-  intros A x y H y0 y1 e; destruct e.
+  intros x y H y0 y1 e; destruct e.
   reduce in H.
   split ; red ; intros H0.
   - setoid_rewrite <- H.
diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v
index a168a8e7cd..964786d8e6 100644
--- a/theories/Classes/Morphisms_Relations.v
+++ b/theories/Classes/Morphisms_Relations.v
@@ -22,11 +22,11 @@ Generalizable Variables A l.
 
 (** Morphisms for relations *)
 
-Instance relation_conjunction_morphism : Proper (relation_equivalence (A:=A) ==>
+Instance relation_conjunction_morphism {A} : Proper (relation_equivalence (A:=A) ==>
   relation_equivalence ==> relation_equivalence) relation_conjunction.
   Proof. firstorder. Qed.
 
-Instance relation_disjunction_morphism : Proper (relation_equivalence (A:=A) ==>
+Instance relation_disjunction_morphism {A} : Proper (relation_equivalence (A:=A) ==>
   relation_equivalence ==> relation_equivalence) relation_disjunction.
   Proof. firstorder. Qed.
 
@@ -43,11 +43,11 @@ Proof. do 2 red. unfold predicate_implication. auto. Qed.
 (** The instantiation at relation allows rewriting applications of relations
     [R x y] to [R' x y]  when [R] and [R'] are in [relation_equivalence]. *)
 
-Instance relation_equivalence_pointwise :
+Instance relation_equivalence_pointwise {A} :
   Proper (relation_equivalence ==> pointwise_relation A (pointwise_relation A iff)) id.
 Proof. intro. apply (predicate_equivalence_pointwise (Tcons A (Tcons A Tnil))). Qed.
 
-Instance subrelation_pointwise :
+Instance subrelation_pointwise {A} :
   Proper (subrelation ==> pointwise_relation A (pointwise_relation A impl)) id.
 Proof. intro. apply (predicate_implication_pointwise (Tcons A (Tcons A Tnil))). Qed.
 
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 5381e91997..401d7007e2 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -395,7 +395,7 @@ Notation "∙⊥∙" := false_predicate : predicate_scope.
 
 (** Predicate equivalence is an equivalence, and predicate implication defines a preorder. *)
 
-Program Instance predicate_equivalence_equivalence : 
+Program Instance predicate_equivalence_equivalence {l} :
   Equivalence (@predicate_equivalence l).
 
   Next Obligation.
@@ -413,7 +413,7 @@ Program Instance predicate_equivalence_equivalence :
       firstorder.
   Qed.
 
-Program Instance predicate_implication_preorder :
+Program Instance predicate_implication_preorder {l} :
   PreOrder (@predicate_implication l).
   Next Obligation.
     intro l; induction l ; firstorder.
@@ -480,7 +480,7 @@ Hint Extern 3 (PartialOrder (flip _)) => class_apply PartialOrder_inverse : type
 
 (** The partial order defined by subrelation and relation equivalence. *)
 
-Program Instance subrelation_partial_order :
+Program Instance subrelation_partial_order {A} :
   PartialOrder (@relation_equivalence A) subrelation.
 
 Next Obligation.
diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v
index b4034b9cf9..09c25b38a6 100644
--- a/theories/Classes/RelationPairs.v
+++ b/theories/Classes/RelationPairs.v
@@ -61,11 +61,9 @@ Class Measure {A B} (f : A -> B).
 
 (** Standard measures. *)
 
-Instance fst_measure : @Measure (A * B) A Fst.
-Defined.
+Instance fst_measure {A B} : @Measure (A * B) A Fst := {}.
 
-Instance snd_measure : @Measure (A * B) B Snd.
-Defined.
+Instance snd_measure {A B} : @Measure (A * B) B Snd := {}.
 
 (** We define a product relation over [A*B]: each components should
     satisfy the corresponding initial relation. *)
@@ -96,11 +94,11 @@ Section RelCompFun_Instances.
     `(Measure A B f, Irreflexive _ R) : Irreflexive (R@@f).
   Proof. firstorder. Qed.
 
-  Global Program Instance RelCompFun_Equivalence
-    `(Measure A B f, Equivalence _ R) : Equivalence (R@@f).
+  Global Instance RelCompFun_Equivalence
+    `(Measure A B f, Equivalence _ R) : Equivalence (R@@f) := {}.
 
-  Global Program Instance RelCompFun_StrictOrder
-    `(Measure A B f, StrictOrder _ R) : StrictOrder (R@@f).
+  Global Instance RelCompFun_StrictOrder
+    `(Measure A B f, StrictOrder _ R) : StrictOrder (R@@f) := {}.
 
 End RelCompFun_Instances.
 
diff --git a/theories/Compat/Coq812.v b/theories/Compat/Coq812.v
index f52b559f84..992b00e834 100644
--- a/theories/Compat/Coq812.v
+++ b/theories/Compat/Coq812.v
@@ -11,4 +11,6 @@
 (** Compatibility file for making Coq act similar to Coq v8.12 *)
 
 Require Export Coq.Compat.Coq813.
+Local Set Warnings "-deprecated".
 Set Firstorder Solver auto with *.
+Export Set Instance Generalized Output.
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 054addc542..062cc90f8f 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -502,9 +502,16 @@ let do_instance_program ~pm env env' sigma ?hook ~global ~poly cty k u ctx ctx'
   else
     declare_instance_program pm env sigma ~global ~poly id pri imps decl term termtype
 
-let interp_instance_context ~program_mode env ctx ~generalize pl tclass =
+let auto_generalize =
+  Goptions.declare_bool_option_and_ref
+    ~depr:true
+    ~key:["Instance";"Generalized";"Output"]
+    ~value:false
+
+let interp_instance_context ~program_mode env ctx ?(generalize=auto_generalize()) pl tclass =
   let sigma, decl = interp_univ_decl_opt env pl in
   let tclass =
+    (* when we remove this code, we can remove the middle argument of CGeneralization *)
     if generalize then CAst.make @@ CGeneralization (Glob_term.MaxImplicit, Some AbsPi, tclass)
     else tclass
   in
@@ -530,10 +537,10 @@ let interp_instance_context ~program_mode env ctx ~generalize pl tclass =
   let sigma = resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env sigma in
   sigma, cl, u, c', ctx', ctx, imps, args, decl
 
-let new_instance_common ~program_mode ~generalize env instid ctx cl =
+let new_instance_common ~program_mode ?generalize env instid ctx cl =
   let ({CAst.loc;v=instid}, pl) = instid in
   let sigma, k, u, cty, ctx', ctx, imps, subst, decl =
-    interp_instance_context ~program_mode env ~generalize ctx pl cl
+    interp_instance_context ~program_mode env ?generalize ctx pl cl
   in
   (* The name generator should not be here *)
   let id =
@@ -548,20 +555,20 @@ let new_instance_common ~program_mode ~generalize env instid ctx cl =
 
 let new_instance_interactive ?(global=false)
     ~poly instid ctx cl
-    ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook
+    ?generalize ?(tac:unit Proofview.tactic option) ?hook
     pri opt_props =
   let env = Global.env() in
   let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl =
-    new_instance_common ~program_mode:false ~generalize env instid ctx cl in
+    new_instance_common ~program_mode:false ?generalize env instid ctx cl in
   id, do_instance_interactive env env' sigma ?hook ~tac ~global ~poly
     cty k u ctx ctx' pri decl imps subst id opt_props
 
 let new_instance_program ?(global=false) ~pm
     ~poly instid ctx cl opt_props
-    ?(generalize=true) ?hook pri =
+    ?generalize ?hook pri =
   let env = Global.env() in
   let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl =
-    new_instance_common ~program_mode:true ~generalize env instid ctx cl in
+    new_instance_common ~program_mode:true ?generalize env instid ctx cl in
   let pm =
     do_instance_program ~pm env env' sigma ?hook ~global ~poly
       cty k u ctx ctx' pri decl imps subst id opt_props in
@@ -569,10 +576,10 @@ let new_instance_program ?(global=false) ~pm
 
 let new_instance ?(global=false)
     ~poly instid ctx cl props
-    ?(generalize=true) ?hook pri =
+    ?generalize ?hook pri =
   let env = Global.env() in
   let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl =
-    new_instance_common ~program_mode:false ~generalize env instid ctx cl in
+    new_instance_common ~program_mode:false ?generalize env instid ctx cl in
   do_instance env env' sigma ?hook ~global ~poly
     cty k u ctx ctx' pri decl imps subst id props;
   id