local notation and implicit variables

Stream: general

[Andrew Yang]

In the following code, the argument α is explicit in foo despite the variable {α} before it. Is this intended? Could I somehow make it implicit?

variable (α : Type)

local notation `β` := α

variable {α}

def foo : β → β := id

#check foo -- gives `foo : Π (α : Type), α → α`

[Eric Wieser]

This has come up before, but I don't remember having as short a mwe last time, so thanks for that