let this

Stream: lean4

[Reid Barton]

How come let this makes a local variable without a definition?

def x : { n : Nat // n = 1 + 1 } := by
  let this : Nat := 2
  exact ⟨this, rfl⟩

It works with a different name.

[Ruben Van de Velde]

I think there's a general issue where this needs to be special cased leading to weird inconsistencies

[Eric Wieser]

My understanding is that this is by design in some way

[Mario Carneiro]

the weird inconsistencies are not by design, but they are a consequence of the design

[Reid Barton]

The design seems buggy.

[Mac Malone]

this is a pseudo-keyword, which I suspect is the problem here.

[Mac Malone]

For reference, the this keyword definition: https://github.com/leanprover/lean4/blob/5661b15e35285a4ed11e0d1d70a960117ea501a9/src/Init/Notation.lean#L499-L503

[Mac Malone]

In fact, the whole point of that definition was to forbid bindings like (this : Nat), but it doesn't work in the case of let presumably because let permits arbitrary terms in its LHS (which are in turn presumably expanded leading to the keyword this becoming the identifier this and the binding working as normal).

[Mario Carneiro]

In fact, the whole point of that definition was to forbid bindings like (this : Nat),

That may be the effect but it wasn't the point of the design. The reason this was made a keyword was so that it does not participate in hygiene, so that `(have := $e) => `(have this := $e) does "what you expect". In practice I think the breakage far outweighs the benefit of being able to write this instead of `(have $(mkIdent `this) := $e) to explicitly make an unhygienic identifier

[Reid Barton]

FWIW what happened to me here was:

• originally wrote a have := blah blah, later use this
• realize that I need to use the definition so change have to let
• let := blah blah isn't allowed any more for some reason so change it to let this := blah blah
• it still doesn't work
• eventually notice that let isn't performing its actual function of making a definition...

[Sebastian Ullrich]

Mario Carneiro said:

`(have $(mkIdent `this) := $e) to explicitly make an unhygienic identifier

I think we've before gone through how that doesn't work in quoted tactics. The two consistent solution I can see are:

• tweak the current implementation by disallowing this in patterns, e.g. by making it an elaborator
• globally make this a special, hygiene-free identifier by specializing it in the hygiene algorithm

The latter is closer to Lean 3's behavior as it allows this to be bound by anyone

[Mario Carneiro]

I think we've before gone through how that doesn't work in quoted tactics.

I don't think we have. Can you show an example?

[Mario Carneiro]

(We have gone through this issue before but not issues with mkIdent `this)

[Mario Carneiro]

The latter is closer to Lean 3's behavior as it allows this to be bound by anyone

I disagree with this: in lean 3 this was not special in any way. It is just an identifier named this, that happened to be the default name used by some tactics. The reason for the unhygienic stuff was simply because everything is unhygienic in lean 3. But I do not believe that any solution that makes this special will work, because this is not the only variable name which has to deal with this issue. h and H are also used at various points in lean 3, and suffer from the same issues

[Mario Carneiro]

I think that the tactic should be the one to opt in to hygiene-less behavior for a particular identifier. If mkIdent `this doesn't work, what about a no-hygiene hygiene you can put on an identifier? For example unhygienicIdent `this which expands to this._@._unhygienic and is handled appropriately by the hygiene manipulation functions

[Sebastian Ullrich]

Mario Carneiro said:

I think we've before gone through how that doesn't work in quoted tactics.

I don't think we have. Can you show an example?

macro "have2" e:term : tactic =>
  `(tactic| have $(mkIdent `this2):ident := $e)
example : Nat := by have2 0; exact this2
macro "foo" : tactic =>
  `(tactic| (have2 0; exact this2))
example : Nat := by foo  -- unknown identifier 'this2'

[Mario Carneiro]

that's expected behavior though

[Mario Carneiro]

foo would need to do mkIdent `this2 as well

[Mario Carneiro]

this is a good thing, because in foo this2 might be a regular variable

[Mario Carneiro]

treating a variable as hygieneless should be opt-in

[Sebastian Ullrich]

It doesn't look reasonable to me at all. We should expect tactic sequences to be liftable into macros without randomly breaking. I don't expect most users to be able to implement have2, but simple reuse like foo should ideally be accessible to anyone

[Sebastian Ullrich]

Mario Carneiro said:

I think that the tactic should be the one to opt in to hygiene-less behavior for a particular identifier. If mkIdent `this doesn't work, what about a no-hygiene hygiene you can put on an identifier? For example unhygienicIdent `this which expands to this._@._unhygienic and is handled appropriately by the hygiene manipulation functions

OTOH that sounds reasonable to me at a first glance

[Mario Carneiro]

that would also not fix the example you just showed, since this2 in foo is a regular identifier and would get hygiened separately

[Mario Carneiro]

In practice I really don't see your example as being an issue. We would just tell someone confused about the situation to use have this := ... instead of have := ... in foo

[Mario Carneiro]

having this be poisoned as a variable name in the rest of foo sounds like a bigger issue

[Sebastian Ullrich]

Mario Carneiro said:

that would also not fix the example you just showed, since this2 in foo is a regular identifier and would get hygiened separately

It depends on whether you strip off macro scopes before checking whether a reference has a corresponding unhygienic binding, which I assumed we would do

[Sebastian Ullrich]

I believe this would also be the approach closest to how anaphoric macros work in Scheme languages

[Mario Carneiro]

I guess I don't know the name resolution mechanism you have in mind then

[Sebastian Ullrich]

Any identifier syntactically equal to X, whether it was later applied macro scopes or not, would bind to X._@._unhygienic if it exists. Introducing such a binding would effectively deactivate hygiene for that identifier

[Mario Carneiro]

so if you have fun (X : A) (X._@._unhygienic : B) (X._@.Foo.0 : C) => ...

• ... => X resolves to A -> B -> C -> B
• ... => X._@._unhygienic resolves to A -> B -> C -> B
• ... => X._@.Foo.0 resolves to A -> B -> C -> C
• ... => X._@.Foo.1 resolves to A -> B -> C -> B

[Sebastian Ullrich]

Probably, yeah. Not that we have a use case for using unhygienic on references like in the second case yet

[Mario Carneiro]

true

[Mario Carneiro]

it can probably come up though when uses are both a binding and a use

[Sebastian Ullrich]

Which in itself is rare :)

[Mario Carneiro]

it does still break things like

macro "have2" e:term : tactic =>
  `(tactic| have $(mkIdent `this):ident := $e)
macro "foo" e:term : tactic =>
  `(tactic| (have2 (); exact $e))
example (this : Nat) : Nat := by foo this

if we wanted the exact $e use to skip the have2 1 binding

[Mario Carneiro]

Last time we talked about this I recall us discussing a way to capture just the macro scope without parsing an identifier. That is sufficient to cover have this := style tactics without any need for unhygienic idents

[Mario Carneiro]

e.g.

macro "have2" sc:macroScope e:term : tactic =>
  `(tactic| have $(sc.mkIdent `this):ident := $e)

[Sebastian Ullrich]

Right, this might even be the most natural one to implement. Nothing more fundamental than the quotation elaborator would have to be changed

[Sebastian Ullrich]

So effectively we would inject this into the calling lexical scope, not all scopes

[Mario Carneiro]

boom, this is working error free:

macro "have2" sc:macroScope e:term : tactic =>
  `(tactic| have $(sc.mkIdent `this2):ident := $e)

example : Nat := by have2 1; exact this2

macro "foo"  : tactic =>
  `(tactic| (have2 1; exact this2))
example : Nat := by foo

macro "bar" e:term : tactic =>
  `(tactic| (have2 (); exact $e))
example (this2 : Nat) : Nat := by bar this2

[Mario Carneiro]

the way it works is that the macroScope parser just generates mkNode `macroScope #[mkIdent .anonymous], more or less. Amusingly, the quotation parser didn't even need to be changed, since it sees the ident node and marks it up just like any other

[Sebastian Ullrich]

I think you'll get into trouble with Syntax.reprint this way (and the pretty printer, but that one we could of course override), that's why I wanted to avoid the ident

[Sebastian Ullrich]

But perhaps changing reprint is the path of least resistance

[Mario Carneiro]

the pretty printer is fine, the formatter and parenthesizer implementations for the macroScope parser are the same as for pushNone

[Mario Carneiro]

for reprint I think it's also fine, because the ident has empty leading & trailing info and also has an empty rawVal

[Mario Carneiro]

I'm not exactly sure what happens if you use a syntax pattern match and ignore the macroScope arg though

[Mario Carneiro]

experimentally, it looks like it matches the macroScope against .anonymous after erasing macro scopes, which is always true so I guess this is fine

[Sebastian Ullrich]

Oh yes, I somehow didn't think of rawVal. Sounds good.

[Mario Carneiro]

Now that lean4#2246 is merged, this is once more a variable name, and we can finally remove the mathlib hacks and uses of «this»