universe with dot notation

Stream: lean4

[Kenny Lau]

def Foo : Type u := sorry
def Foo.inv : Foo -> Foo := sorry

variable (x : Foo.{u})
#check x.inv.{u} -- invalid use of explicit universe parameters, 'x' is a local variable
#check x.inv -- succeeds

[Kenny Lau]

Is it intentional that .{u} notation cannot be used with dot notation?

[Edward van de Meent]

it can, just not when x is a variable:

def Foo : Type u := sorry
def Foo.inv : Foo -> Foo := sorry

def x : Foo := sorry

universe u in
#check x.inv.{u}

[Kenny Lau]

sure, but it could still be useful when x is a variable

[Kyle Miller]

There's no syntax for dot notation (you can check that (x).inv.{u} is a syntax error).

True dot notation is (x).inv, and when you write x.inv, what happens is that the elaborator sees that x.inv isn't a constant, so it automatically splits the last name component off and tries (x).inv. This is why x.inv.{u} parses at all.

I think it's clear you've found a bug. I'm not sure it was intentional that x.inv.{u} even attempts to elaborate. Could you file a Lean 4 issue? I think it's reasonable to ask for this new feature in that issue as well.

[Edward van de Meent]

i suspect this tries to apply the universe level to x?

[Edward van de Meent]

but when it's a variable, it already has a universe level, so it complains

[Kyle Miller]

Edward van de Meent said:

i suspect this tries to apply the universe level to x?

Yes, that's what the error is indicating.

Edward van de Meent said:

but when it's a variable, it already has a universe level, so it complains

No, given that it's apparently interpreting x.inv.{u} as (x.{u}).inv, the issue is that only Expr.const has universe levels. This x is a local variable (an Expr.fvar).

[Edward van de Meent]

Kyle Miller said:

Edward van de Meent said:

but when it's a variable, it already has a universe level, so it complains

No, the issue is that only Expr.const has universe levels. This x is a local variable (an Expr.fvar).

i feel like we're saying the same thing here?

[Eric Wieser]

This came up in a PR as P.Obj.{v} for docs#PFunctor.Obj, which wasn't legal and we had to write Obj.{v} P instead.

[Kenny Lau]

Created lean4#8743

[Kyle Miller]

Edward van de Meent said:

i feel like we're saying the same thing here?

(It doesn't make sense to say x already has a universe level. Local variables don't have universe levels at all.)

[Edward van de Meent]

right, i guess the way to phrase it is "there are no free universe variables to fill in the type"?

[Kyle Miller]

That's still inaccurate — it's about filling in the universe levels of a constant; constants need to be instantiated with particular universe levels. The types of expressions doesn't come into this.