instantiation of level metavariables in structure instances

Stream: lean4

[Matthew Ballard]

In the example,

import Lean

structure Foo where
  type : Type u

universe u v w

variable (α : Type u) (β : Type v) (γ : Type w)

-- set_option trace.Meta.isLevelDefEq true in
-- set_option trace.Elab.step true in
set_option trace.Elab.struct true in
set_option pp.all true in
-- set_option trace.Elab.struct true in
def foo : Foo where
  type := (α ⊕ β) ⊕ γ
/--
▶ expected type (15:15-18:1)
α : Type u
β : Type v
γ : Type w
⊢ Foo.{max w v u}

▶ 15:15-16:1: information:
[Elab.struct] {type := (α ⊕ β) ⊕ γ}

[Elab.struct] elabStruct type := (α ⊕ β) ⊕ γ, Type ?u.226 → Foo.{?u.226}

[Elab.struct] before propagate Foo.mk.{max w v u} (Sum.{max v u, w} (Sum.{u, v} α β) γ)
-/

It would seem that in the private Lean.Elab.Term.StructInst.elabStructInstAux which is called by docs#Lean.Elab.Term.StructInst.elabStructInst we should know the universe levels of foo when the trace for Elab.struct on line 1190 is hit. However, when I try to act on expression at that point via normalize, nothing happens. It seems there is a level metavariable in expression at this point in elaboration despite the trace showing something else.

• Am I correct?
• Where is the trace pulling the information from?
• If correct, when is the metavariable actually instantiated?

[Jovan Gerbscheid]

It is true that the trace will instantiate metavariables, so it could be that there is still a metavariable in the expression, but that it has an assignment, so the trace doesn't show the metavariable.

[Jovan Gerbscheid]

If you use

set_option trace.profiler true in
set_option trace.profiler.threshold 0 in

Then you can see that there is a step of instantiateMVarsProfiling that comes after the Elab.struct trace. So it seems probable that this is when they are instantiated.

[Jovan Gerbscheid]

the trace function makes a copy of the local context and metavariable context, in order to be able to nicely render the expressions, so that is how it gets the metavariable instantiations.

[Jovan Gerbscheid]

I've had this problem/confusion many times. But I just found out there is a solution: set_option pp.instantiateMVars false. :smiley:

[Matthew Ballard]

Thanks!