chore: revert automatically exposing derived instances (#10101)

Heed surrounding `@[expose]` instead

src/Init/Data/Int/Linear.lean

@@ -39,7 +39,7 @@ inductive Expr where
   | neg (a : Expr)
   | mulL (k : Int) (a : Expr)
   | mulR (a : Expr) (k : Int)
-  deriving Inhabited, BEq
+  deriving Inhabited, @[expose] BEq
 
 @[expose]
 def Expr.denote (ctx : Context) : Expr → Int
@@ -54,7 +54,7 @@ def Expr.denote (ctx : Context) : Expr → Int
 inductive Poly where
   | num (k : Int)
   | add (k : Int) (v : Var) (p : Poly)
-  deriving BEq
+  deriving @[expose] BEq
 
 @[expose]
 protected noncomputable def Poly.beq' (p₁ : Poly) : Poly → Bool :=

src/Lean/Elab/Deriving/BEq.lean

@@ -108,8 +108,8 @@ def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Command := do
   if ctx.usePartial then
     `(partial def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Bool := $body:term)
   else
-    let expAttr := ctx.mkExposeAttrFromCtors
-    `(@[$expAttr] $vis:visibility def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Bool := $body:term)
+    let expAttr := ctx.mkNoExposeAttrFromCtors
+    `(@[$[$expAttr],*] $vis:visibility def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Bool := $body:term)
 
 def mkMutualBlock (ctx : Context) : TermElabM Syntax := do
   let mut auxDefs := #[]
@@ -129,8 +129,8 @@ private def mkBEqInstanceCmds (declName : Name) : TermElabM (Array Syntax) := do
 private def mkBEqEnumFun (ctx : Context) (name : Name) : TermElabM Syntax := do
   let auxFunName := ctx.auxFunNames[0]!
   let vis := ctx.mkVisibilityFromTypes
-  let expAttr := ctx.mkExposeAttrFromCtors
-  `(@[$expAttr] $vis:visibility def $(mkIdent auxFunName):ident  (x y : $(mkCIdent name)) : Bool := x.toCtorIdx == y.toCtorIdx)
+  let expAttr := ctx.mkNoExposeAttrFromCtors
+  `(@[$[$expAttr],*] $vis:visibility def $(mkIdent auxFunName):ident  (x y : $(mkCIdent name)) : Bool := x.toCtorIdx == y.toCtorIdx)
 
 private def mkBEqEnumCmd (name : Name): TermElabM (Array Syntax) := do
   let ctx ← mkContext "beq" name

src/Lean/Elab/Deriving/DecEq.lean

@@ -103,7 +103,7 @@ def mkAuxFunction (ctx : Context) (auxFunName : Name) (indVal : InductiveVal): T
     else `(Parser.Termination.suffix|)
   let type    ← `(Decidable ($target₁ = $target₂))
   let vis := ctx.mkVisibilityFromTypes
-  `(@[expose] $vis:visibility def $(mkIdent auxFunName):ident $binders:bracketedBinder* : $type:term := $body:term
+  `($vis:visibility def $(mkIdent auxFunName):ident $binders:bracketedBinder* : $type:term := $body:term
     $termSuffix:suffix)
 
 def mkAuxFunctions (ctx : Context) : TermElabM (TSyntax `command) := do

src/Lean/Elab/Deriving/Inhabited.lean

@@ -85,8 +85,8 @@ where
       ctorArgs := ctorArgs.push (← ``(Inhabited.default))
     let val ← `(⟨@$(mkIdent ctorName):ident $ctorArgs*⟩)
     let vis := ctx.mkVisibilityFromTypes
-    let expAttr := ctx.mkExposeAttrFromCtors
-    `(@[$expAttr] $vis:visibility instance $binders:bracketedBinder* : $type := $val)
+    let expAttr := ctx.mkNoExposeAttrFromCtors
+    `(@[$[$expAttr],*] $vis:visibility instance $binders:bracketedBinder* : $type := $val)
 
   mkInstanceCmd? : TermElabM (Option Syntax) := do
     let ctorVal ← getConstInfoCtor ctorName

src/Lean/Elab/Deriving/Nonempty.lean

@@ -30,9 +30,9 @@ private def mkNonemptyInstance (declName : Name) : TermElabM Syntax.Command := d
   let ctorTacs ← indVal.ctors.toArray.mapM fun ctor =>
     `(tactic| apply @$(mkCIdent ctor) <;> exact Classical.ofNonempty)
   let vis := ctx.mkVisibilityFromTypes
-  let expAttr := ctx.mkExposeAttrFromCtors
+  let expAttr := ctx.mkNoExposeAttrFromCtors
   `(command| variable $binders* in
-    @[$expAttr] $vis:visibility instance : Nonempty (@$(mkCIdent declName) $indArgs*) :=
+    @[$[$expAttr],*] $vis:visibility instance : Nonempty (@$(mkCIdent declName) $indArgs*) :=
       by constructor; first $[| $ctorTacs:tactic]*)
 
 def mkNonemptyInstanceHandler (declNames : Array Name) : CommandElabM Bool := do

src/Lean/Elab/Deriving/Util.lean

@@ -81,12 +81,13 @@ def Context.mkVisibilityFromTypes (ctx : Context) : TSyntax ``visibility :=
 
 open Parser.Term in
 /--
-Returns `no_expose` or `expose` depending on whether any types with private constructors are
-referenced in the `deriving` clause.
+Returns `no_expose` if any types with private constructors are referenced in the `deriving` clause.
+`expose` is assumed to be specified explicitly by the user.
 -/
-def Context.mkExposeAttrFromCtors (ctx : Context) : TSyntax ``attrInstance :=
-  Unhygienic.run <|
-    if ctx.typeInfos.any (·.ctors.any isPrivateName) then `(attrInstance| no_expose) else `(attrInstance| expose)
+def Context.mkNoExposeAttrFromCtors (ctx : Context) : Array (TSyntax ``attrInstance) :=
+  if ctx.typeInfos.any (·.ctors.any isPrivateName) then
+    #[Unhygienic.run <| `(attrInstance| no_expose)]
+  else #[]
 
 def mkContext (fnPrefix : String) (typeName : Name) : TermElabM Context := do
   let indVal ← getConstInfoInduct typeName
@@ -144,8 +145,8 @@ def mkInstanceCmds (ctx : Context) (className : Name) (typeNames : Array Name) (
       if useAnonCtor then
         val ← `(⟨$val⟩)
       let vis := ctx.mkVisibilityFromTypes
-      let expAttr := ctx.mkExposeAttrFromCtors
-      let instCmd ← `(@[$expAttr] $vis:visibility instance $binders:implicitBinder* : $type := $val)
+      let expAttr := ctx.mkNoExposeAttrFromCtors
+      let instCmd ← `(@[$[$expAttr],*] $vis:visibility instance $binders:implicitBinder* : $type := $val)
       instances := instances.push instCmd
   return instances
 

tests/lean/decEqMutualInductives.lean.expected.out

@@ -1,6 +1,5 @@
 [Elab.Deriving.decEq] 
     [mutual
-       @[expose✝]
        public def decEqTree✝ (x✝ : @Tree✝) (x✝¹ : @Tree✝) : Decidable✝ (x✝ = x✝¹) :=
          match x✝, x✝¹ with
          | @Tree.node a✝, @Tree.node b✝ =>
@@ -8,7 +7,6 @@
            if h✝ : @a✝ = @b✝ then by subst h✝; exact isTrue✝ rfl✝
            else isFalse✝ (by intro n✝; injection n✝; apply h✝ _; assumption)
        termination_by structural x✝
-       @[expose✝]
        public def decEqListTree✝ (x✝² : @ListTree✝) (x✝³ : @ListTree✝) : Decidable✝ (x✝² = x✝³) :=
          match x✝², x✝³ with
          | @ListTree.nil, @ListTree.nil => isTrue✝¹ rfl✝¹
@@ -24,12 +22,11 @@
            else isFalse✝³ (by intro n✝²; injection n✝²; apply h✝² _; assumption)
        termination_by structural x✝²
      end,
-     @[expose✝]
+     @[]
      public instance : DecidableEq✝ (@ListTree✝) :=
        decEqListTree✝]
 [Elab.Deriving.decEq] 
     [mutual
-       @[expose✝]
        public def decEqFoo₁✝ (x✝ : @Foo₁✝) (x✝¹ : @Foo₁✝) : Decidable✝ (x✝ = x✝¹) :=
          match x✝, x✝¹ with
          | @Foo₁.foo₁₁, @Foo₁.foo₁₁ => isTrue✝ rfl✝
@@ -40,7 +37,6 @@
            if h✝¹ : @a✝ = @b✝ then by subst h✝¹; exact isTrue✝¹ rfl✝¹
            else isFalse✝¹ (by intro n✝; injection n✝; apply h✝¹ _; assumption)
        termination_by structural x✝
-       @[expose✝]
        public def decEqFoo₂✝ (x✝² : @Foo₂✝) (x✝³ : @Foo₂✝) : Decidable✝ (x✝² = x✝³) :=
          match x✝², x✝³ with
          | @Foo₂.foo₂ a✝¹, @Foo₂.foo₂ b✝¹ =>
@@ -48,7 +44,6 @@
            if h✝² : @a✝¹ = @b✝¹ then by subst h✝²; exact isTrue✝² rfl✝²
            else isFalse✝² (by intro n✝¹; injection n✝¹; apply h✝² _; assumption)
        termination_by structural x✝²
-       @[expose✝]
        public def decEqFoo₃✝ (x✝⁴ : @Foo₃✝) (x✝⁵ : @Foo₃✝) : Decidable✝ (x✝⁴ = x✝⁵) :=
          match x✝⁴, x✝⁵ with
          | @Foo₃.foo₃ a✝², @Foo₃.foo₃ b✝² =>
@@ -57,6 +52,6 @@
            else isFalse✝³ (by intro n✝²; injection n✝²; apply h✝³ _; assumption)
        termination_by structural x✝⁴
      end,
-     @[expose✝]
+     @[]
      public instance : DecidableEq✝ (@Foo₁✝) :=
        decEqFoo₁✝]

tests/lean/run/decEq.lean

@@ -17,7 +17,7 @@ def t1 [DecidableEq α] : DecidableEq (Vec α n) :=
 def t2 [DecidableEq α] : DecidableEq (Test α) :=
   inferInstance
 
-/-! Public structures should yield public exposed instances independent of `public section`. -/
+/-! Public structures should yield public instances independent of `public section`. -/
 
 /--
 trace: [Elab.Deriving.decEq] ⏎
@@ -37,25 +37,20 @@ public inductive PubEnum where
   | a | b
 deriving DecidableEq
 
-/--
-trace: [Elab.Deriving.decEq] ⏎
-    [mutual
-       @[expose✝]
-       public def decEqPubInd✝ (x✝ : @PubInd✝) (x✝¹ : @PubInd✝) : Decidable✝ (x✝ = x✝¹) :=
-         match x✝, x✝¹ with
-         | @PubInd.a a✝, @PubInd.a b✝ =>
-           if h✝ : @a✝ = @b✝ then by subst h✝; exact isTrue✝ rfl✝
-           else isFalse✝ (by intro n✝; injection n✝; apply h✝ _; assumption)
-         | PubInd.a .., PubInd.b .. => isFalse✝¹ (by intro h✝¹; injection h✝¹)
-         | PubInd.b .., PubInd.a .. => isFalse✝¹ (by intro h✝¹; injection h✝¹)
-         | @PubInd.b, @PubInd.b => isTrue✝¹ rfl✝¹
-     end,
-     @[expose✝]
-     public instance : DecidableEq✝ (@PubInd✝) :=
-       decEqPubInd✝]
--/
-#guard_msgs in
-set_option trace.Elab.Deriving.decEq true in
 public inductive PubInd where
   | a (n : Nat) | b
 deriving DecidableEq
+
+/-- info: Decidable.rec (fun h => false) (fun h => true) (decEqPubInd✝ PubInd.b PubInd.b) -/
+#guard_msgs in
+#with_exporting
+#reduce decide (PubInd.b = PubInd.b)
+
+public inductive PubExpInd where
+  | a (n : Nat) | b
+deriving @[expose] DecidableEq
+
+/-- info: true -/
+#guard_msgs in
+#with_exporting
+#reduce decide (PubExpInd.b = PubExpInd.b)

tests/lean/run/derivingBEq.lean

@@ -4,7 +4,7 @@ public section
 
 inductive Foo
   | mk1 | mk2 | mk3
-  deriving BEq
+  deriving @[expose] BEq
 
 namespace Foo
 theorem ex1 : (mk1 == mk2) = false :=
@@ -22,7 +22,7 @@ end Foo
 inductive Vec (α : Type u) : Nat → Type u
   | nil  : Vec α 0
   | cons : α → {n : Nat} → Vec α n → Vec α (n+1)
-  deriving BEq
+  deriving @[expose] BEq
 
 namespace Vec
 theorem ex1 : (cons 10 Vec.nil == cons 20 Vec.nil) = false :=