cleanups

Author: datokrat

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

@@ -37,6 +37,16 @@ private def resumePostponed (savedContext : SavedContext) (stx : Syntax) (mvarId
         let mvarDecl     ← getMVarDecl mvarId
         let expectedType ← instantiateMVars mvarDecl.type
         withInfoHole mvarId do
+          /-
+          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.

src/Lean/Elab/Term/TermElabM.lean

@@ -482,7 +482,7 @@ depend on them (i.e. they should not be inspected beforehand).
 def withNarrowedArgTacticReuse [Monad m] [MonadReaderOf Context m] [MonadLiftT BaseIO m]
     [MonadWithReaderOf Core.Context m] [MonadWithReaderOf Context m] [MonadOptions m]
     (argIdx : Nat) (act : Syntax → m α) (stx : Syntax) : m α :=
-  withNarrowedTacticReuse (fun stx => (mkNullNode stx.getArgs[*...argIdx].copy, stx[argIdx])) act stx
+  withNarrowedTacticReuse (fun stx => (mkNullNode stx.getArgs[*...argIdx], stx[argIdx])) act stx
 
 /--
 Disables incremental tactic reuse *and* reporting for `act` if `cond` is true by setting `tacSnap?`

src/Lean/Linter/Coe.lean

@@ -52,7 +52,7 @@ def coeLinter : Linter where
                 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 ()
-                logWarningAt ci.stx <| .tagged ``deprecatedAttr <|
+                logLint linter.deprecatedCoercions ci.stx <| .tagged ``deprecatedAttr <|
                   m!"This term uses the deprecated coercion `{.ofConstName coeDecl true}`."
         | _ => pure ()
         return true) (fun _ _ _ _ => return)

src/Lean/Meta/Coe.lean

@@ -40,29 +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 :=
-  withReducibleAndInstances do
-    transform e fun e => do
-      let f := e.getAppFn
-      if f.isConst then
-        let declName := f.constName!
-        if isCoeDecl (← getEnv) declName then
-          /-
-          Unfolding an instance projection corresponds to unfolding the target of the projection
-          (and then reducing the projection). Thus we can recursively visit projections before
-          recording the declaration. We shouldn't need to record any other arguments because they
-          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
-      return .continue
-
-
-
-/-- Expand coercions occurring in `e` -/
-partial def expandCoe' (e : Expr) : MetaM (Expr × List Name) := StateT.run (s := ([] : List Name)) do
+/--
+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
@@ -77,6 +59,10 @@ partial def expandCoe' (e : Expr) : MetaM (Expr × List Name) := StateT.run (s :
           -/
           recordExtraModUseFromDecl (isMeta := false) (← recProjTarget e)
           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
@@ -99,7 +85,7 @@ def coerceSimple? (expr expectedType : Expr) : MetaM (LOption (Expr × List Name
   let coeTInstType := mkAppN (mkConst ``CoeT [u, v]) #[eType, expr, expectedType]
   match ← trySynthInstance coeTInstType with
   | .some inst =>
-    let result ← expandCoe' (mkAppN (mkConst ``CoeT.coe [u, v]) #[eType, expr, expectedType, inst])
+    let result ← expandCoe (mkAppN (mkConst ``CoeT.coe [u, v]) #[eType, expr, expectedType, inst])
     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
@@ -114,7 +100,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}"
@@ -128,7 +114,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}"
@@ -217,7 +203,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`
@@ -244,7 +233,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
@@ -254,10 +243,15 @@ 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. -/
+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 coerce? (expr expectedType : Expr) : MetaM (LOption (Expr × List Name)) := do
   if let some lifted ← coerceMonadLift? expr expectedType then
     return .some (lifted, [])

tests/lean/run/coeLinter.lean

@@ -9,6 +9,8 @@ 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"
 
 /--
@@ -17,9 +19,39 @@ warning: This term uses the coercion `instCoeSubarrayArray`, which is banned in
 #guard_msgs in
 def g : Array Nat := #[1, 2, 3][*...*]
 
-set_option trace.Elab.info true
+/--
+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