sigma notation overriden by local sigma def

Stream: lean4

[Alex Keizer]

It seems that if we have a definition called Sigma in a namespace, that the Σ notation will refer to this local Sigma, rather than the usual, root, Sigma.

namespace MySigma
  /-- We define a new `Sigma` -/
  def Sigma {α : Type u} (β : α → Type v)
    := String

  /- Now, `Σ` notatation refers to `MySigma.Sigma`, rather than the root `Sigma` -/
  #reduce Σ a, a -- This reduces to `String`
end MySigma

Looking at the definition, this surprises me bit.

macro "Σ" xs:explicitBinders ", " b:term : term => expandExplicitBinders ``Sigma xs b

I though the double quotes in ``Sigma were supposed to prevent exactly this kind of shadowing.

So, is this behaviour of sigma a bug? I wouldn't mind digging in deeper and seeing if I can make a PR that fixes it, but I heard the core team is not really able to accept outside PRs right now, is that true?

[Alex Keizer]

Interestingly, even if we change the notation to mention _root_.Sigmaexplicitly, it still has this same shadowing behaviour

macro "Σ''" xs:explicitBinders ", " b:term : term => expandExplicitBinders ``_root_.Sigma xs b

[Sebastian Ullrich]

Oh looks like a simple oversight in expandExplicitBinders

[Alex Keizer]

Ah, yeah, it seems that if we change

let combinator := mkIdentFrom (← getRef) combinatorDeclName

to

let combinator := mkCIdentFrom (← getRef) combinatorDeclName

in expandExplicitBinders, then everything works.

[Sebastian Ullrich]

Yep https://github.com/leanprover/lean4/commit/3f6c5f17db30c2a2dcaca1b9e9faec4e2cf04b95

[Sebastian Ullrich]

Oh well, I could have used mkCIdentFromRef

[Alex Keizer]

Cool, thanks for fixing it!