Qq footgun

Stream: lean4

[Thomas Murrills]

What do you think the following code does? :)

import Qq

open Lean Qq

def etaNatQ (a : Q(Nat → Nat)) : MetaM Q(Nat → Nat) := do
  let a := a.eta
  logInfo m!"{a}"
  return q($a)

#eval etaNatQ q(fun i => Nat.succ i)

[Adam Topaz]

Is this a hygiene issue in Qq?

[Eric Wieser]

This is https://github.com/leanprover-community/quote4/pull/11 I think

[Eric Wieser]

The let a is of type Expr so is not visible in the context of q($a), and so the original a is unshadowed

[Thomas Murrills]

Ah, nice! I checked the issues, but not the PRs...

[Eric Wieser]

I think maybe the thing to do here is copy how `() quotes work

[Eric Wieser]

That is, they just show the whole context:

def foo (i : String) (x : Term) : MetaM Term := `(id $x + $i)

and produce a type error on bad variables

[Eric Wieser]

But I guess then you lose the niceness of the Q() wrappers going away