Bug in `deprecated` linter

Stream: lean4

[Yury G. Kudryashov]

Here is an #mwe

@[deprecated] def Implies (p q : Prop) := p → q

def MyNS.Implies (α : Type) (p q : α → Prop) : Prop :=
  ∀ x, p x → q x

open MyNS

namespace MyNS2

example (h : Implies Nat (fun _ ↦ True) fun _ ↦ False) : False :=
  h 0 trivial

In this example, Lean says that Implies is deprecated but in fact this is the non-deprecated MyNS.Implies.

[Damiano Testa]

Slight minimization:

@[deprecated] def Implies (_p : Unit) := True

def MyNS.Implies := True

open MyNS

example (h : Implies) : True := h

[Yury G. Kudryashov]

Note: if the definition is in namespace MyNS, then everything works fine. It fails only with open MyNS; probably, because it tried to unify _root_.Implies too (and failed) but this is just a guess.

[Mario Carneiro]

this is a known issue, I recall there being a comment about it in the code

[Mario Carneiro]

https://github.com/leanprover/lean4/blob/ad068824d05878da799567f0ae56b4048eef9022/src/Lean/Elab/Term.lean#L1602

    Linter.checkDeprecated declName -- TODO: check is occurring too early if there are multiple alternatives. Fix if it is not ok in practice

[Mario Carneiro]

in short, whenever lean has to use typing to differentiate between ambiguous name resolutions, it can potentially mark things as deprecated before it has committed to one of the possibilities, so you see phantom warnings from parses that didn't make the cut

[Yury G. Kudryashov]

Thank you.

[Yury G. Kudryashov]

I'll just use full name.