universe shadows a local universe

Stream: general

[Sean Leather]

In a file with only this:

universes u
variables α β : Type*

I get this:

error: invalid universe declaration, 'u_1' shadows a local universe

Why?

[Kenny Lau]

This also annoys me but I just didn't bother to ask

[Brendan Zabarauskas]

What does Type* do? Does it elaborate into introducing some hidden u universe?

[Sean Leather]

Yeah, it happened once too often for me: passed the annoyance threshold. :wink:

[Sean Leather]

What does Type* do? Does it elaborate into introducing some hidden u universe?

It uses an implicit universe, as far as I understand it.

[Johan Commelin]

set.option annoyance_threshold 100

[Johan Commelin]

Solves it

[Brendan Zabarauskas]

I've kind of noticed that Lean's elaboration isn't hygenic... guessing that's by design though?

[Sean Leather]

It's very powerful, but it does have some annoying corner cases in various places. I believe the idea is that as long as the kernel is safe and the core language is well-typed, elaboration and tactics can be less so.

[Brendan Zabarauskas]

By hygiene I mean in the macro sense. Racket works hard to preserve it. It might make encapsulation harder and increase the chance of breaking things downstream due to updates in libraries.

[Brendan Zabarauskas]

(warning, might be being imprecise in my language here, feel free to correct me)

[Sean Leather]

I sometimes like to think of Lean as one big code generator. I tries by various means to produce kernel code for definitions and theorems. Elaboration is an advanced form of unification and uses definitional equality to try to convert terms into other terms. Tactics are like imperatively programming the code generation. Type class instance resolution is another code generation mechanism. All of these try to interpret what you want and produce some kernel code. But they are all imperfect and sometimes require fiddling to get what you want.

(Edit: Language is also imprecise, but the idea helps me comprehend it.)

[Brendan Zabarauskas]

Yeah, definitely. That's how I'm starting to sort of see it. Just wondering if some of the learning from languages like Scheme and Racket into theorem provers. Not experienced enough with Coq to know how they handle hygiene (if they do any identifier generation in their tactics/elaboration). :thinking_face:

[Mario Carneiro]

Hygenic macros are a planned feature in the next version of lean

[Brendan Zabarauskas]

Oh nice!

[Brendan Zabarauskas]

Yeah thought it might just be an intermediate state of affairs. Hard to do everything at once.

[Mario Carneiro]

As for the given error, basically this is because variables A B : Type* desugars to

universe u_1
variable A : Type u_1
universe u_1
variable B : Type u_1

and universe shadowing is disallowed (for some reason...). This is a known bug, but it's unlikely to be addressed in the current version of lean

[Mario Carneiro]

the workaround is to write variables (A : Type*) (B : Type*)

[Brendan Zabarauskas]

So I'm guessing universes u does nothing to affect the issue?

[Mario Carneiro]

no, it's unrelated

[Mario Carneiro]

although I bet you can also get a name shadowing issue with only one variable if it was universe u_1

[Sean Leather]

Yeah, I discovered that, too. What is the difference from this?

variable α : Type*
variable β : Type*

[Mario Carneiro]

that desugars to

universe u_1
variable A : Type u_1
universe u_2
variable B : Type u_2

which is okay

[Brendan Zabarauskas]

In the future, is the intention to make those generated u_1 identifiers inaccessable?

[Mario Carneiro]

the variable command in general is more than a little hackish

[Sean Leather]

Ah. So, it's smart enough to create a fresh universe variable there.

[Mario Carneiro]

inaccessible? Why?

[Mario Carneiro]

I think "fresh" is more appropriate

[Mario Carneiro]

In fact, they come up explicitly in proofs, although it's bad form to refer to autogenerated names

[Mario Carneiro]

but the fact that they are literal names like u_1 and not some mystery private thing is important

[Brendan Zabarauskas]

Hah, I might be conflicting with an existing term by the use of 'inaccessable', but yeah, it seems like it could result in fragile code if you referred to those generated names.

[Brendan Zabarauskas]

But happy to be persuaded otherwise - I'm still new to Lean and might not fully understand.

[Sean Leather]

Here's my first experience with variable name shadowing.

[Mario Carneiro]

I'm not advocating explicit reference to generated names, just the opposite (that's what I mean by "bad form"). But I can believe that sometimes it is necessary to refer to an autogenerated name, maybe because the tactic that produced the name doesn't have enough configuration space to supply nice names.

[Brendan Zabarauskas]

What do you mean by 'configuration space'?

[Mario Carneiro]

Some tactics have complicated logic for when they introduce new names, intro variables, etc, and it may not be easy to specify names at the top level so that after the tactic you know what you will get

[Brendan Zabarauskas]

Interesting! That seems like a tantilising design problem to solve! :simple_smile:

[Mario Carneiro]

The lazy option (for the tactic writer) is not to bother with providing names to the tactic, so you get what you get, and then after the tactic you might need to refer to those auto names (if only to rename them)

[Mario Carneiro]

I think that finish has this problem, although it's not really designed for nonterminal use so it's not a big problem

[Mario Carneiro]

Some tactics like injections just take a big list of names at the start and pull from that pool whenever something is intro'd

[Patrick Massot]

@Brendan Zabarauskas see https://github.com/leanprover/lean/issues/1674 which, I believe, is one the main issue Lean 4 is meant to solve, and contains "Hygienic macro system" in the title. Lean 4 is currently worked on (but won't come soon).

[Brendan Zabarauskas]

Very cool! And understandable that it will take time - good to know it's coming though.

[Johan Commelin]

Wow, I like the ideas in that issue! @Patrick Massot do you remember asking about tikzcd notation for commutative diagrams in lean? That might become a true option then! I like it (-;

[Patrick Massot]

Indeed I was thinking about this when I mentioned tikz-cd syntax