use Array

fix test and simp 'copy' to 'toArray'

write linter

add backticks

make the linter more defensive to avoid panics

make sure stage0 is updated after merging

revert the changes in src/Lean

why doesn't this work?

Revert "revert the changes in src/Lean"

This reverts commit 75c70823b5.

revert the changes in src/Lean

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

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 α} :

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

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

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

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

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

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

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;

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

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