fix: reuse the instances of a non-exposed definition in inferInstanceAs

This PR makes `inferInstanceAs` reuse the existing instances of a non-exposed definition. This is done by checking the reusability of an instance in the private scope, as neither the auxiliary definitions being generated nor the ones in the existing instance are exposed in this case.

Closes #14470.

Author: gasparattila

src/Lean/Meta/WrapInstance.lean

@@ -233,7 +233,7 @@ where go (inst expectedType : Expr) (isEta : Bool) : MetaM (Option Expr) := do
             try
               if let .some new ← trySynthInstance argExpectedType then
                 -- ignore instances from non-defeq diamonds
-                if (← withDefault <| isDefEq new arg) then
+                if (← withoutExporting (when := !exposeAux) <| withDefault <| isDefEq new arg) then
                   trace[Meta.wrapInstance] "using existing instance {new}"
                   mvarId.assign new
                   isEta := false
@@ -264,7 +264,7 @@ where go (inst expectedType : Expr) (isEta : Bool) : MetaM (Option Expr) := do
                 if let .some existingBaseClassInst ← trySynthInstance baseClassType then
                   let proj ← mkProjection existingBaseClassInst fieldInfo.fieldName
                   -- ignore instances from non-defeq diamonds
-                  if (← withDefault <| isDefEq proj arg) then
+                  if (← withoutExporting (when := !exposeAux) <| withDefault <| isDefEq proj arg) then
                     trace[Meta.wrapInstance] "using projection of existing instance `{existingBaseClassInst}`"
                     mvarId.assign proj
                     continue

tests/elab/inferInstanceAs.lean

@@ -1,5 +1,7 @@
 module
 
+public import Lean
+
 class C (α : Type) where
   c : α → α
 
@@ -180,4 +182,42 @@ Nat.zero
 #guard_msgs in
 #print instInhabitedIsExposed._aux_1
 
+/-! Test the reuse of instances of `NotExposed` (#14470). -/
+
+class Base' (α : Type) where
+  b : α
+
+class Foo' (α : Type) extends Base' α where
+  a : α
+
+class Bar' (α : Type) extends Base' α where
+  c : α
+
+class FooBar' (α : Type) extends Foo' α, Bar' α
+
+instance : FooBar' Nat where
+  a := 0
+  b := 1
+  c := 2
+
+namespace NotExposed
+
+noncomputable instance : Foo' NotExposed := inferInstanceAs (Foo' Nat)
+noncomputable instance : Bar' NotExposed := inferInstanceAs (Bar' Nat)
+noncomputable instance : FooBar' NotExposed := inferInstanceAs (FooBar' Nat)
+
+open Lean Elab Tactic in
+elab "with_exporting" tac:tacticSeq : tactic =>
+  Lean.withExporting (isExporting := true) (Lean.Elab.Tactic.evalTactic tac)
+
+-- The instances must be reused for these defeqs to hold publicly.
+
+example : instFooBar'.toFoo' = instFoo' := by
+  with_exporting with_reducible_and_instances rfl
+
+example : instFooBar'.toBar' = instBar' := by
+  with_exporting with_reducible_and_instances rfl
+
+end NotExposed
+
 end