Local notation with local variable

[fgdorais]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Local notation defined using a local variable no longer works.

Steps to Reproduce

variable {α} (op : α → α → α)
local infixr:60 " ∙ " => op
example (x y : α) : x ∙ y = y ∙ x := sorry

Expected behavior:

Local notation accepted and usable locally.

Actual behavior:

error: unknown identifier 'op'
Test.lean:2:25: error: unknown identifier 'op'
Test.lean:2:0: error: cannot evaluate code because it uses 'sorry' and/or contains errors
Test.lean:3:20: error: elaboration function for 'term_∙_' has not been implemented
  x ∙ y

Reproduces how often: Always

Versions

Lean (version 4.0.0-nightly-2021-05-02, commit e20a07bd6dd0, Release)

Linux pop-os 5.11.0-7614-generic #15~1618626693~20.10~ecb25cd-Ubuntu SMP Thu Apr 22 16:00:45 UTC x86_64 x86_64 x86_64 GNU/Linux

Additional Information

Works fine with version nightly-2021-04-27 but breaks on nightly-2021-04-28.

[fgdorais]

@leodemoura Thank you for fixing so quickly!

There appears to be a remnant of this issue. This snippet fails:

structure Op (α : Type _) where op : α → α → α
variable {α} (s : Op α)
local infixr:60 " ∙ " => s.op
example (x y : α) : x ∙ y = y ∙ x := sorry

with

Test.lean:3:25: error: unknown identifier 's.op'
Test.lean:3:0: error: cannot evaluate code because it uses 'sorry' and/or contains errors
Test.lean:4:20: error: elaboration function for 'term_∙_' has not been implemented
  x ∙ y
Test.lean:4:37: warning: declaration uses 'sorry'

However, there is an easy workaround since this works as expected:

structure Op (α : Type _) where op : α → α → α
variable {α} (s : Op α)
local infixr:60 " ∙ " => Op.op s
example (x y : α) : x ∙ y = y ∙ x := sorry

Lean version: Lean (version 4.0.0-nightly-2021-05-04, commit a5c28f7dfcca, Release)