diff --git a/src/Init/Data/Slice/Array/Iterator.lean b/src/Init/Data/Slice/Array/Iterator.lean
index d71ed6821772..7b4c36d1e3c8 100644
--- a/src/Init/Data/Slice/Array/Iterator.lean
+++ b/src/Init/Data/Slice/Array/Iterator.lean
@@ -130,16 +130,34 @@ The implementation of `ForIn.forIn` for `Subarray`, which allows it to be used w
 def Subarray.forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (s : Subarray α) (b : β) (f : α → β → m (ForInStep β)) : m β :=
   ForIn.forIn s b f
 
-namespace Array
-
 /--
 Allocates a new array that contains the contents of the subarray.
 -/
 @[coe]
-def ofSubarray (s : Subarray α) : Array α :=
+def Subarray.toArray (s : Subarray α) : Array α :=
   Slice.toArray s
 
-instance : Coe (Subarray α) (Array α) := ⟨ofSubarray⟩
+instance instCoeSubarrayArray : Coe (Subarray α) (Array α) :=
+  ⟨Subarray.toArray⟩
+
+@[inherit_doc Subarray.toArray]
+def Subarray.copy (s : Subarray α) : Array α :=
+  Slice.toArray s
+
+@[simp]
+theorem Subarray.copy_eq_toArray {s : Subarray α} :
+    s.copy = s.toArray :=
+  (rfl)
+
+theorem Subarray.sliceToArray_eq_toArray {s : Subarray α} :
+    Slice.toArray s = s.toArray :=
+  (rfl)
+
+namespace Array
+
+@[inherit_doc Subarray.toArray]
+def ofSubarray (s : Subarray α) : Array α :=
+  Slice.toArray s
 
 instance : Append (Subarray α) where
   append x y :=
@@ -157,7 +175,3 @@ instance [ToString α] : ToString (Subarray α) where
   toString s := toString s.toArray
 
 end Array
-
-@[inherit_doc Array.ofSubarray]
-def Subarray.toArray (s : Subarray α) : Array α :=
-  Array.ofSubarray s
diff --git a/src/Init/Data/Slice/Array/Lemmas.lean b/src/Init/Data/Slice/Array/Lemmas.lean
index 25f2d212ec68..8ad92f832988 100644
--- a/src/Init/Data/Slice/Array/Lemmas.lean
+++ b/src/Init/Data/Slice/Array/Lemmas.lean
@@ -110,7 +110,7 @@ public instance : LawfulSliceSize (Internal.SubarrayData α) where
 
 public theorem toArray_eq_sliceToArray {α : Type u} {s : Subarray α} :
     s.toArray = Slice.toArray s := by
-  simp [Subarray.toArray, Array.ofSubarray]
+  simp [Subarray.toArray]
 
 @[simp]
 public theorem forIn_toList {α : Type u} {s : Subarray α}
@@ -206,12 +206,12 @@ public theorem Subarray.size_eq {xs : Subarray α} :
 @[simp]
 public theorem Subarray.toArray_toList {xs : Subarray α} :
     xs.toList.toArray = xs.toArray := by
-  simp [Std.Slice.toList, Subarray.toArray, Array.ofSubarray, Std.Slice.toArray]
+  simp [Std.Slice.toList, Subarray.toArray, Std.Slice.toArray]
 
 @[simp]
 public theorem Subarray.toList_toArray {xs : Subarray α} :
     xs.toArray.toList = xs.toList := by
-  simp [Std.Slice.toList, Subarray.toArray, Array.ofSubarray, Std.Slice.toArray]
+  simp [Std.Slice.toList, Subarray.toArray, Std.Slice.toArray]
 
 @[simp]
 public theorem Subarray.length_toList {xs : Subarray α} :
diff --git a/src/Lean/Elab/InfoTree/Main.lean b/src/Lean/Elab/InfoTree/Main.lean
index d1e93f50f437..cad5a83e3085 100644
--- a/src/Lean/Elab/InfoTree/Main.lean
+++ b/src/Lean/Elab/InfoTree/Main.lean
@@ -489,6 +489,10 @@ def withMacroExpansionInfo [MonadFinally m] [Monad m] [MonadInfoTree m] [MonadLC
     }
   withInfoContext x mkInfo
 
+/--
+Runs `x`. The last info tree that is pushed while running `x` is assigned to `mvarId`. All other
+pushed info trees are silently discarded.
+-/
 @[inline] def withInfoHole [MonadFinally m] [Monad m] [MonadInfoTree m] (mvarId : MVarId) (x : m α) : m α := do
   if (← getInfoState).enabled then
     let treesSaved ← getResetInfoTrees
diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean
index 147d18447dfc..db7383014991 100644
--- a/src/Lean/Elab/SyntheticMVars.lean
+++ b/src/Lean/Elab/SyntheticMVars.lean
@@ -38,10 +38,21 @@ private def resumePostponed (savedContext : SavedContext) (stx : Syntax) (mvarId
         let mvarDecl     ← getMVarDecl mvarId
         let expectedType ← instantiateMVars mvarDecl.type
         withInfoHole mvarId do
-          let result ← resumeElabTerm stx expectedType (!postponeOnError)
-          /- We must ensure `result` has the expected type because it is the one expected by the method that postponed stx.
-            That is, the method does not have an opportunity to check whether `result` has the expected type or not. -/
-          let result ← withRef stx <| ensureHasType expectedType result
+          /-
+          NOTE: `withInfoTree` discards all but the last info tree pushed inside this `do` block.
+          `resumeElabTerm` usually pushes the term info node and `ensureHasType` sometimes
+          pushes a custom info node with information about the coercions that were applied.
+
+          In order for both trees to be preserved, we use `withTermInfoContext'` to wrap these
+          trees into a single node. Although this results in two nested term nodes for the same
+          syntax element, this should be unproblematic. For example, `hoverableInfoAtM?` selects
+          the innermost info tree.
+          -/
+          let result ← withTermInfoContext' .anonymous stx do
+            let result ← resumeElabTerm stx expectedType (!postponeOnError)
+            /- We must ensure `result` has the expected type because it is the one expected by the method that postponed stx.
+              That is, the method does not have an opportunity to check whether `result` has the expected type or not. -/
+            withRef stx <| ensureHasType expectedType result
           /- We must perform `occursCheck` here since `result` may contain `mvarId` when it has synthetic `sorry`s. -/
           if (← occursCheck mvarId result) then
             mvarId.assign result
@@ -537,7 +548,11 @@ mutual
         if (← occursCheck mvarId e) then
           mvarId.assign e
           return true
-      if let .some coerced ← coerce? e expectedType then
+      if let .some (coerced, expandedCoeDecls) ← coerceCollectingNames? e expectedType then
+        pushInfoLeaf (.ofCustomInfo {
+          stx := mvarSyntheticDecl.stx
+          value := Dynamic.mk <| CoeExpansionTrace.mk expandedCoeDecls
+        })
         if (← occursCheck mvarId coerced) then
           mvarId.assign coerced
           return true
diff --git a/src/Lean/Elab/Term/TermElabM.lean b/src/Lean/Elab/Term/TermElabM.lean
index 1b4664a4f83e..f6f80e2030c6 100644
--- a/src/Lean/Elab/Term/TermElabM.lean
+++ b/src/Lean/Elab/Term/TermElabM.lean
@@ -1209,14 +1209,23 @@ def synthesizeInstMVarCore (instMVar : MVarId) (maxResultSize? : Option Nat := n
             pure <| extraErrorMsg ++ useTraceSynthMsg
       throwNamedError lean.synthInstanceFailed "failed to synthesize instance of type class{indentExpr type}{msg}"
 
+structure CoeExpansionTrace where
+  expandedCoeDecls : List Name
+deriving TypeName
+
 def mkCoe (expectedType : Expr) (e : Expr) (f? : Option Expr := none) (errorMsgHeader? : Option String := none)
     (mkErrorMsg? : Option (MVarId → (expectedType e : Expr) → MetaM MessageData) := none)
     (mkImmedErrorMsg? : Option ((errorMsg? : Option MessageData) → (expectedType e : Expr) → MetaM MessageData) := none) : TermElabM Expr := do
   withTraceNode `Elab.coe (fun _ => return m!"adding coercion for {e} : {← inferType e} =?= {expectedType}") do
   try
     withoutMacroStackAtErr do
-      match ← coerce? e expectedType with
-      | .some eNew => return eNew
+      match ← coerceCollectingNames? e expectedType with
+      | .some (eNew, expandedCoeDecls) =>
+        pushInfoLeaf (.ofCustomInfo {
+          stx := ← getRef
+          value := Dynamic.mk <| CoeExpansionTrace.mk expandedCoeDecls
+        })
+        return eNew
       | .none => failure
       | .undef =>
         let mvarAux ← mkFreshExprMVar expectedType MetavarKind.syntheticOpaque
diff --git a/src/Lean/Linter.lean b/src/Lean/Linter.lean
index 4ae5c16450a5..db472340a66d 100644
--- a/src/Lean/Linter.lean
+++ b/src/Lean/Linter.lean
@@ -17,3 +17,4 @@ public import Lean.Linter.Omit
 public import Lean.Linter.List
 public import Lean.Linter.Sets
 public import Lean.Linter.UnusedSimpArgs
+public import Lean.Linter.Coe
diff --git a/src/Lean/Linter/Coe.lean b/src/Lean/Linter/Coe.lean
new file mode 100644
index 000000000000..7175d25061cc
--- /dev/null
+++ b/src/Lean/Linter/Coe.lean
@@ -0,0 +1,62 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+public import Lean.Elab.Command
+public import Lean.Server.InfoUtils
+import Lean.Linter.Basic
+import Lean.Linter.Deprecated
+import all Lean.Elab.Term.TermElabM
+
+public section
+set_option linter.missingDocs true -- keep it documented
+
+namespace Lean.Linter.Coe
+
+/--
+`set_option linter.deprecatedCoercions true` enables a linter emitting warnings on deprecated
+coercions.
+-/
+register_builtin_option linter.deprecatedCoercions : Bool := {
+  defValue := true
+  descr := "Validate that no deprecated coercions are used."
+}
+
+/--
+Checks whether the "deprecated coercions" linter is enabled.
+-/
+def shouldWarnOnDeprecatedCoercions [Monad m] [MonadOptions m] : m Bool :=
+  return (← getOptions).get linter.deprecatedCoercions.name true
+
+/-- A list of coercion names that must not be used in core. -/
+def coercionsBannedInCore : Array Name := #[``optionCoe, ``instCoeSubarrayArray]
+
+/-- Validates that no coercions are used that are either deprecated or are banned in core. -/
+def coeLinter : Linter where
+  run := fun _ => do
+    let mainModule ← getMainModule
+    let isCoreModule := mainModule = `lean.run.linterCoe ∨ (mainModule.getRoot ∈ [`Init, `Std])
+    let shouldWarnOnDeprecated := getLinterValue linter.deprecatedCoercions (← getLinterOptions)
+    let trees ← Elab.getInfoTrees
+    for tree in trees do
+      tree.visitM' (m := Elab.Command.CommandElabM) (fun _ info _ => do
+        match info with
+        | .ofCustomInfo ci =>
+          if let some trace := ci.value.get? Elab.Term.CoeExpansionTrace then
+            for coeDecl in trace.expandedCoeDecls do
+              if isCoreModule && coeDecl ∈ coercionsBannedInCore then
+                logWarningAt ci.stx m!"This term uses the coercion `{coeDecl}`, which is banned in Lean's core library."
+              if shouldWarnOnDeprecated then
+                let some attr := deprecatedAttr.getParam? (← getEnv) coeDecl | pure ()
+                logLint linter.deprecatedCoercions ci.stx <| .tagged ``deprecatedAttr <|
+                  m!"This term uses the deprecated coercion `{.ofConstName coeDecl true}`."
+        | _ => pure ()
+        return true) (fun _ _ _ _ => return)
+
+builtin_initialize addLinter coeLinter
+
+end Lean.Linter.Coe
diff --git a/src/Lean/Meta/Coe.lean b/src/Lean/Meta/Coe.lean
index f349cdced1a6..a46e8022ec5f 100644
--- a/src/Lean/Meta/Coe.lean
+++ b/src/Lean/Meta/Coe.lean
@@ -40,8 +40,11 @@ private partial def recProjTarget (e : Expr) (nm : Name := e.getAppFn.constName!
   else
     return nm
 
-/-- Expand coercions occurring in `e` -/
-partial def expandCoe (e : Expr) : MetaM Expr :=
+/--
+Expands coercions occurring in `e` and return the result together with a list of applied
+`Coe` instances.
+-/
+partial def expandCoe (e : Expr) : MetaM (Expr × List Name) := StateT.run (s := ([] : List Name)) do
   withReducibleAndInstances do
     transform e fun e => do
       let f := e.getAppFn
@@ -55,8 +58,18 @@ partial def expandCoe (e : Expr) : MetaM Expr :=
           should still appear after unfolding (unless there are unused variables in the instances).
           -/
           recordExtraModUseFromDecl (isMeta := false) (← recProjTarget e)
-          if let some e ← unfoldDefinition? e then
-            return .visit e.headBeta
+          if let some e' ← unfoldDefinition? e then
+            /-
+            If the unfolded coercion is an application of `Coe.coe` and its third argument is
+            an application of a constant, record this constant's name.
+            -/
+            if declName = ``Coe.coe then
+              if let some inst := e.getAppArgs[2]? then
+                let g := inst.getAppFn
+                if g.isConst then
+                  let instName := g.constName!
+                  StateT.set (instName :: (← StateT.get))
+            return .visit e'.headBeta
       return .continue
 
 register_builtin_option autoLift : Bool := {
@@ -65,7 +78,7 @@ register_builtin_option autoLift : Bool := {
 }
 
 /-- Coerces `expr` to `expectedType` using `CoeT`. -/
-def coerceSimple? (expr expectedType : Expr) : MetaM (LOption Expr) := do
+def coerceSimpleRecordingNames? (expr expectedType : Expr) : MetaM (LOption (Expr × List Name)) := do
   let eType ← inferType expr
   let u ← getLevel eType
   let v ← getLevel expectedType
@@ -73,12 +86,19 @@ def coerceSimple? (expr expectedType : Expr) : MetaM (LOption Expr) := do
   match ← trySynthInstance coeTInstType with
   | .some inst =>
     let result ← expandCoe (mkAppN (mkConst ``CoeT.coe [u, v]) #[eType, expr, expectedType, inst])
-    unless ← isDefEq (← inferType result) expectedType do
-      throwError "Could not coerce{indentExpr expr}\nto{indentExpr expectedType}\ncoerced expression has wrong type:{indentExpr result}"
+    unless ← isDefEq (← inferType result.1) expectedType do
+      throwError "Could not coerce{indentExpr expr}\nto{indentExpr expectedType}\ncoerced expression has wrong type:{indentExpr result.1}"
     return .some result
   | .undef => return .undef
   | .none => return .none
 
+/-- Coerces `expr` to `expectedType` using `CoeT`. -/
+def coerceSimple? (expr expectedType : Expr) : MetaM (LOption Expr) := do
+  match ← coerceSimpleRecordingNames? expr expectedType with
+  | .some (result, _) => return .some result
+  | .none => return .none
+  | .undef => return .undef
+
 /-- Coerces `expr` to a function type. -/
 def coerceToFunction? (expr : Expr) : MetaM (Option Expr) := do
   -- constructing expression manually because mkAppM wouldn't assign universe mvars
@@ -87,7 +107,7 @@ def coerceToFunction? (expr : Expr) : MetaM (Option Expr) := do
   let v ← mkFreshLevelMVar
   let γ ← mkFreshExprMVar (← mkArrow α (mkSort v))
   let .some inst ← trySynthInstance (mkApp2 (.const ``CoeFun [u,v]) α γ) | return none
-  let expanded ← expandCoe (mkApp4 (.const ``CoeFun.coe [u,v]) α γ inst expr)
+  let (expanded, _) ← expandCoe (mkApp4 (.const ``CoeFun.coe [u,v]) α γ inst expr)
   unless (← whnf (← inferType expanded)).isForall do
     throwError m!"Failed to coerce{indentExpr expr}\nto a function: After applying `CoeFun.coe`, result is still not a function{indentExpr expanded}"
       ++ .hint' m!"This is often due to incorrect `CoeFun` instances; the synthesized instance was{indentExpr inst}"
@@ -101,7 +121,7 @@ def coerceToSort? (expr : Expr) : MetaM (Option Expr) := do
   let v ← mkFreshLevelMVar
   let β ← mkFreshExprMVar (mkSort v)
   let .some inst ← trySynthInstance (mkApp2 (.const ``CoeSort [u,v]) α β) | return none
-  let expanded ← expandCoe (mkApp4 (.const ``CoeSort.coe [u,v]) α β inst expr)
+  let (expanded, _) ← expandCoe (mkApp4 (.const ``CoeSort.coe [u,v]) α β inst expr)
   unless (← whnf (← inferType expanded)).isSort do
     throwError m!"Failed to coerce{indentExpr expr}\nto a type: After applying `CoeSort.coe`, result is still not a type{indentExpr expanded}"
       ++ .hint' m!"This is often due to incorrect `CoeSort` instances; the synthesized instance was{indentExpr inst}"
@@ -190,7 +210,10 @@ def coerceMonadLift? (e expectedType : Expr) : MetaM (Option Expr) := do
   let saved ← saveState
   if (← isDefEq m n) then
     let some monadInst ← isMonad? n | restoreState saved; return none
-    try expandCoe (← mkAppOptM ``Lean.Internal.coeM #[m, α, β, none, monadInst, e]) catch _ => restoreState saved; return none
+    try
+      let (result, _) ← expandCoe (← mkAppOptM ``Lean.Internal.coeM #[m, α, β, none, monadInst, e])
+      pure result
+    catch _ => restoreState saved; return none
   else if autoLift.get (← getOptions) then
     try
       -- Construct lift from `m` to `n`
@@ -217,7 +240,7 @@ def coerceMonadLift? (e expectedType : Expr) : MetaM (Option Expr) := do
         let v ← getLevel β
         let coeTInstType := Lean.mkForall `a BinderInfo.default α <| mkAppN (mkConst ``CoeT [u, v]) #[α, mkBVar 0, β]
         let .some coeTInstVal ← trySynthInstance coeTInstType | return none
-        let eNew ← expandCoe (mkAppN (Lean.mkConst ``Lean.Internal.liftCoeM [u_1, u_2, u_3]) #[m, n, α, β, monadLiftVal, coeTInstVal, monadInst, e])
+        let (eNew, _) ← expandCoe (mkAppN (Lean.mkConst ``Lean.Internal.liftCoeM [u_1, u_2, u_3]) #[m, n, α, β, monadLiftVal, coeTInstVal, monadInst, e])
         let eNewType ← inferType eNew
         unless (← isDefEq expectedType eNewType) do return none
         return some eNew -- approach 3 worked
@@ -227,17 +250,34 @@ def coerceMonadLift? (e expectedType : Expr) : MetaM (Option Expr) := do
   else
     return none
 
-/-- Coerces `expr` to the type `expectedType`.
-Returns `.some coerced` on successful coercion,
+/--
+Coerces `expr` to the type `expectedType`.
+Returns `.some (coerced, appliedCoeDecls)` on successful coercion,
 `.none` if the expression cannot by coerced to that type,
-or `.undef` if we need more metavariable assignments. -/
-def coerce? (expr expectedType : Expr) : MetaM (LOption Expr) := do
+or `.undef` if we need more metavariable assignments.
+
+`appliedCoeDecls` is a list of names representing the names of the `Coe` instances that were
+applied.
+-/
+def coerceCollectingNames? (expr expectedType : Expr) : MetaM (LOption (Expr × List Name)) := do
   if let some lifted ← coerceMonadLift? expr expectedType then
-    return .some lifted
+    return .some (lifted, [])
   if (← whnfR expectedType).isForall then
     if let some fn ← coerceToFunction? expr then
       if ← isDefEq (← inferType fn) expectedType then
-        return .some fn
-  coerceSimple? expr expectedType
+        return .some (fn, [])
+  coerceSimpleRecordingNames? expr expectedType
+
+/--
+Coerces `expr` to the type `expectedType`.
+Returns `.some coerced` on successful coercion,
+`.none` if the expression cannot by coerced to that type,
+or `.undef` if we need more metavariable assignments.
+-/
+def coerce? (expr expectedType : Expr) : MetaM (LOption Expr) := do
+  match ← coerceCollectingNames? expr expectedType with
+  | .some (result, _) => return .some result
+  | .none => return .none
+  | .undef => return .undef
 
 end Lean.Meta
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 0f2ee3e7a4fa..82b0e04c6c8c 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -1,6 +1,7 @@
 #include "util/options.h"
 
 // this comment has been updated 1 time(s)
+// dear CI, please do a stage0 update after merging my PR so that the coercion linter becomes active
 namespace lean {
 options get_default_options() {
     options opts;
diff --git a/tests/lean/binopInfoTree.lean.expected.out b/tests/lean/binopInfoTree.lean.expected.out
index e4ccbcc93b52..12459a39f7d6 100644
--- a/tests/lean/binopInfoTree.lean.expected.out
+++ b/tests/lean/binopInfoTree.lean.expected.out
@@ -55,6 +55,9 @@ fun n m l => ↑n + (↑m + ↑l) : Nat → Nat → Nat → Int
             ===>
             binop% HAdd.hAdd✝ n (m +' l)
             • [Term] ↑n + (↑m + ↑l) : Int @ ⟨7, 29⟩†-⟨7, 41⟩† @ Lean.Elab.Term.Op.elabBinOp
+              • [CustomInfo(Lean.Elab.Term.CoeExpansionTrace)]
+              • [CustomInfo(Lean.Elab.Term.CoeExpansionTrace)]
+              • [CustomInfo(Lean.Elab.Term.CoeExpansionTrace)]
               • [Term] ↑n + (↑m + ↑l) : Int @ ⟨7, 29⟩†-⟨7, 41⟩†
                 • [Completion-Id] HAdd.hAdd✝ : none @ ⟨7, 29⟩†-⟨7, 41⟩†
                 • [Term] n : Nat @ ⟨7, 29⟩-⟨7, 30⟩ @ Lean.Elab.Term.elabIdent
diff --git a/tests/lean/run/linterCoe.lean b/tests/lean/run/linterCoe.lean
new file mode 100644
index 000000000000..ff87634bc23c
--- /dev/null
+++ b/tests/lean/run/linterCoe.lean
@@ -0,0 +1,59 @@
+module
+
+-- by default, linters are disabled when running tests
+set_option linter.all true
+
+structure X
+structure Y
+
+@[deprecated "" (since := "")]
+instance mycoe : Coe X Y where coe _ := ⟨⟩
+
+/-- warning: This term uses the coercion `optionCoe`, which is banned in Lean's core library. -/
+#guard_msgs in
+def f : Option String := "hi"
+
+/--
+warning: This term uses the coercion `instCoeSubarrayArray`, which is banned in Lean's core library.
+-/
+#guard_msgs in
+def g : Array Nat := #[1, 2, 3][*...*]
+
+/--
+warning: This term uses the deprecated coercion `mycoe`.
+
+Note: This linter can be disabled with `set_option linter.deprecatedCoercions false`
+-/
+#guard_msgs in
+def h (foo : X) : Y := foo
+
+/-- -/
+notation a " +' " b => a + b
+
+@[deprecated "" (since := "")]
+instance : Coe X Int where
+  coe _ := 0
+
+/--
+@ +1:31...32
+warning: This term uses the deprecated coercion `instCoeXInt`.
+
+Note: This linter can be disabled with `set_option linter.deprecatedCoercions false`
+---
+@ +1:36...37
+warning: This term uses the deprecated coercion `instCoeXInt`.
+
+Note: This linter can be disabled with `set_option linter.deprecatedCoercions false`
+---
+@ +1:41...42
+warning: This term uses the deprecated coercion `instCoeXInt`.
+
+Note: This linter can be disabled with `set_option linter.deprecatedCoercions false`
+-/
+#guard_msgs(positions := true) in
+example := fun (n m l : X) => (n + (m +' l) : Int)
+
+set_option linter.deprecatedCoercions false
+
+#guard_msgs in
+def h' (foo : X) : Y := foo