Resolve all level mvars

Stream: lean4

[Leni Aniva]

Consider this expression:

universe u
#check ∀ (a: Sort (u + 1)), List a

The type is Type (u + 1), as expected.

However, if I were to construct this expression from its building blocks (the use case is expression generation from SMT solvers, etc.) as such:

import Lean

open Lean

def metaM : MetaM Unit := do
  let bindName: Name := "a".toName
  let domain: Level := .succ $ .param ("u".toName)
  let uMVar ← Meta.mkFreshLevelMVar
  let e: Expr := .forallE bindName (.sort domain) (.app (.const `List [uMVar]) (.bvar 0)) .default
  let t: Expr ← Meta.inferType e
  println! "e: {← Meta.ppExpr e}"
  println! "t: {← Meta.ppExpr t}"


def main : IO Unit := do
  let env: Environment ← importModules
    (imports := #["Init"].map (λ str => { module := str.toName, runtimeOnly := false }))
    (opts := {})
    (trustLevel := 1)
  let coreM := Meta.MetaM.run' metaM
  let coreContext: Lean.Core.Context := {
    currNamespace := "PrintExpr".toName,
    openDecls := [],     -- No 'open' directives needed
    fileName := "<stdin>",
    fileMap := { source := "", positions := #[0] }
    options := Lean.Options.empty
  }
  match ← (coreM.run' coreContext { env := env }).toBaseIO with
  | .error exception =>
    IO.println s!"{← exception.toMessageData.toString}"
  | .ok _            =>
    IO.println "Finished"

The resulting type is

e: (a : Type u) → List a
t: Type (max (u + 1) ?u.1)

Is there a way for Lean to automatically resolve ?u.1 during the generation of the call to List?

I read elabAppFnId, but in this case I don't have the types for the intermediate expression building blocks, so I can't use it.

[Kyle Miller]

Functions like Expr.app etc. are very low-level — they're just constructors. You need to use higher-level meta functions such as mkAppM to build expressions while doing unification.

[Leni Aniva]

Kyle Miller said:

Functions like Expr.app etc. are very low-level — they're just constructors. You need to use higher-level meta functions such as mkAppM to build expressions while doing unification.

so I should use a function like Meta.withNewLocalInstances to bring every binder in .lambdaE and .forallE into scope and build expressions with free variables only?

[Kyle Miller]

Or, rather than using a level metavariable, you compute the level

[Leni Aniva]

Kyle Miller said:

Or, rather than using a level metavariable, you compute the level

is there a function to do this

[Kyle Miller]

That's not what Meta.withNewLocalInstances does. This function is responsible for updating the instance cache after you've brought every binder into scope using something like forallTelescope

[Kyle Miller]

Take a look at the AppBuilder module to see how to create complete expressions. docs#Lean.Meta.mkEq is an example

[Kyle Miller]

(And as a consistency check, you can use docs#Lean.Meta.check to typecheck completed expressions)

[Kyle Miller]

I read elabAppFnId, but in this case I don't have the types for the intermediate expression building blocks, so I can't use it.

That's a private function and you're not meant to use it. An alternative to mkAppM/mkAppOptM for the TermElabM monad is docs#Lean.Elab.Term.elabAppArgs, which is the core algorithm for elaborating function applications. If your terms aren't complicated then there's no need to use it, but it's sometimes helpful in in some contexts.

[Leni Aniva]

Is there a way to calculate the level at the invocation point? I already have the entire expression structure but it is just stored in another format. The reason I didn't wnat to use mkAppM is because it would require me to bring the bound variables into scope using some sort of telescope mechanism

[Kyle Miller]

Any reason you don't want to bring them into scope?

[Kyle Miller]

There's no way to reliably calculate levels or types if your expressions have bvars — if you're working with bvars, you are mostly on your own.

[Leni Aniva]

Kyle Miller said:

There's no way to reliably calculate levels or types if your expressions have bvars — if you're working with bvars, you are mostly on your own.

is there not a way to calculate them after the mvars have been created?

[Leni Aniva]

Kyle Miller said:

Any reason you don't want to bring them into scope?

this would require me to invoke the AppBuilder module monads from the C side, which requires a lot of state tracking. If there's no way to determine levels or types without using monads I'll use them

[Kyle Miller]

Is it out of the question to determine that uMVar is u when you construct your expression?

[Leni Aniva]

Kyle Miller said:

That's not what Meta.withNewLocalInstances does. This function is responsible for updating the instance cache after you've brought every binder into scope using something like forallTelescope

Then what function should I use during the construction of a .lam or .forallE that brings into scope the argument and then abstract out the argument into a .bvar?

[Leni Aniva]

Kyle Miller said:

Is it out of the question to determine that uMVar is u when you construct your expression?

yes, because the source expression representation in C does not carry universe information

[Kyle Miller]

There are a few, for example withLocalDeclD, which then you use mkForallFVars and mkLambdaFVars to create terms rather than raw constructors.

[Kyle Miller]

yes, because the source expression representation in C does not carry universe information

It must be determinable in some way, otherwise how would Lean be able to solve for it through unification?

[Leni Aniva]

Kyle Miller said:

yes, because the source expression representation in C does not carry universe information

It must be determinable in some way, otherwise how would Lean be able to solve for it through unification?

I know but I don't know what algorithm I can use to determine them from the C side

[Kyle Miller]

I'm afraid I can only give this general advice about constructing expressions without knowing a lot more about the concrete details about what you're working on.

[Leni Aniva]

I don't have more details either, the representation I have is very general. I think I should just use withLocalDeclD and other functions

[Kyle Miller]

A difference here is that you know what that representation is and I can only guess, and I don't know any of the constraints that you're dealing with — What part has to be in C? What part can be done in Lean? What the concrete representation? Can it be changed? If so, can it be changed to make this easier? etc. etc. etc.

[Leni Aniva]

Kyle Miller said:

A difference here is that you know what that representation is and I can only guess, and I don't know any of the constraints that you're dealing with — What part has to be in C? What part can be done in Lean? What the concrete representation? Can it be changed? If so, can it be changed to make this easier? etc. etc. etc.

The C representation is the same as Lean's Expr but without the .mdata, .proj, and universe level informations. I cannot change it without major refactoring on the solver side