Wrong universe levels when stored in structure

[SReichelt]

Thank you very much for this library. I'm migrating my code over to it, which mostly works well, but now I'm stuck at a serious problem and I don't understand the code well enough yet to fix it myself. Here is an example:

set_option pp.all true

structure UnivTest where
α : Sort u
β : Sort v

def univTest : UnivTest := ⟨Prop, Type⟩

-- this is fine
def qUnivTest := q(univTest)
#print qUnivTest

structure LevelTest where
{u v : Level}
t : Q(UnivTest.{u, v})

-- contains `udummy`
def extract_t (lt : LevelTest) := q($lt.t)
#print extract_t

-- wrongly chooses the value for `v` also for `u`
def extract_t_fail := extract_t ⟨qUnivTest⟩
#print extract_t_fail

-- (related problem? fails to compile)
def extract_t_fail' := extract_t ⟨q(univTest)⟩

When an expression that depends on two or more universe levels is stored in a structure, and the structure field is used in an antiquotation, the universe levels are not obtained correctly. Somehow the same value is used for all universes.

[gebner]

the universe levels are not obtained correctly.

The good news is that this is just a bug in the pretty-printer. I've now added a pp.qq option to disable it (setting pp.all will also disable it).

-- (related problem? fails to compile)
def extract_t_fail' := extract_t ⟨q(univTest)⟩

This is a technical issue with the translation of metavariables. The expected type inside the anonymous constructor is something like QQ (mkConst ``UnivTest [?u, ?v]). In general, this is supported. The q(_) constructor will take all these metavariables ?u : Level, ?v : Level (and also potentially other metavariables like ?m : QQ (mkSort ?u)) and turn them into universe/expression metavariables inside the quotation. If metavariables remain after elaborating the quotation, those metavariables are turned back into metavariables on the meta level.

For this it is necessary that the (outside) metavariables are in the same local context. Otherwise we'd introduce assignments that depend on hypotheses that are not in scope:

show (u : Level) × ((v : Level) → (e : Q(Type $v)) → Q(Sort $u)) from
  ⟨_, fun v e => q($e)⟩ -- would require assigning ?u := mkLevelSucc v

The check should not trigger in your example, I'll need to look at this in more detail.

[SReichelt]

The good news is that this is just a bug in the pretty-printer. I've now added a pp.qq option to disable it (setting pp.all will also disable it).

Sorry, I messed up the example a bit. With your new option, I can see that the following updated example generates incorrect code:

set_option pp.all true

structure UnivTest where
α : Sort u
β : Sort v

structure LevelTest where
{u v : Level}
t : Q(UnivTest.{u, v})

-- wrongly chooses `lt.2` for both universes
def extract_α (lt : LevelTest) := q(($lt.t).α)
#print extract_α

[gebner]

Thanks for reporting this bug! What happened is that both lt.1 and lt.2 were turned into the same universe level (udummy) inside the quote.

[SReichelt]

Thank you for fixing it so quickly! I noticed the udummy but didn't realize that names played such a significant role.

Could the same fix be needed here? https://github.com/gebner/quote4/blob/e46540ec1d52a76630bc1431f152962cb825aef6/Qq/Macro.lean#L119 I haven't noticed any concrete problem, but just to make sure.

[gebner]

Could the same fix be needed here?

That one's fine because it creates a free variable with a fresh unique name. So there's two pieces of information identifying the free variable, and it's not a big problem if one of them clashes. Level parameters only have the user-facing name, and that's why they clash.