Hygiene and shadowing

Stream: metaprogramming / tactics

[Michael Ballantyne]

I'm trying to understand how Lean's hygiene interacts with shadowing, and I'm a bit confused. The #eval in this program yields "top", whereas I would expect it to yield "defined by m1":

def x := "top"
macro "m1" : command => `(
  def x := "defined by m1"
  #eval x
)
m1

What's more confusing is that if I omit the def x := "top" definition I do get the result "defined by m1". So it's not that the macro-introduced definition is not visible in the macro-introduced #eval x. Instead, it seems that the top-level definition is preferred over the macro-introduced one somehow.

I'm most familiar with Racket; the equivalent program there would be:

(define x "top")
(define-syntax-rule (m1)
  (begin
    (define x "defined by m1")
    (displayln x)))
(m1)

which does produce "defined by m1". The way that I understand this in Racket is that the macro-introduced names belong to a lexical scope whose parent scope is the macro definition site, so resolution first looks for bindings in new scopes created by the expansion and then in the definition site. (The story under the hood is more complicated with various scope set manipulations, of course.)

Any hints on the right mental model for Lean's behavior?

[Aaron Liu]

If you swap def x := "top" and macro "m1" : command => `( (so that x doesn't exist at the time the macro is defined) then it does give "defined by m1"

[Sebastian Ullrich]

Yes, the scoping story on the top level is a bit less clear than on the term level (and also quite different from Racket given strict declaration ordering, not that that makes this specific behavior more reasonable). The main hygiene property there is to disallow "retroactive" bindings like in Aaron's example.

[Michael Ballantyne]

With the resolution code from your dissertation it looks like this would produce an ambiguity error, which would make more sense to me. I just tried the example with the code from the paper supplement (https://github.com/Kha/macro-supplement/tree/master) and that indeed seems to be the result there. Maybe I'll keep digging to see why it behaves differently in current Lean.

[Michael Ballantyne]

Hmm, okay, it's as simple as the version in the supplement appending the global resolution with the pre-resolveds (code) whereas current Lean only tries global resolution if there are no pre-resolveds (code).

[David Renshaw]

Here's one way to avoid potential collisions:

import Lean

def x := "top"

macro "m1" : command => do
  let xx ← Lean.Elab.Term.mkFreshIdent (←`(x))
  `(
    def $xx := "defined by m1"
    #eval $xx
  )

m1

[David Renshaw]

Not sure if there's a better way.

[Michael Ballantyne]

I guess if the types of the surrounding binding and the introduced binding are the same, the ambiguity error forces you to choose a different name in your macro just the same. But if the types are different, more programs should work with the design from the supplement, e.g.:

def x: Int := 42
macro "m1" n:ident : command => `(
  def x := "defined by m1"
  def $n:ident : String := x
)
m1 y
#eval y

[Michael Ballantyne]

It's also interesting that the resolution that happens when quoting a name (here) appends the pre-resolveds, unlike the term resolveName, so in the following program you do get the ambiguous resolution behavior:

def x := "top"
macro "m1" : command => `(
  def x := "defined by m1"
  macro "m2" : command => `(#eval x))
m1
m2