Dealing with level params in metaprogramming

Stream: lean4

[Max Nowak 🐉]

I have arg : Type v and inductive T.{u} : Type u -> Type u, and then my expr is T arg, which gets a repr of .app (.const T [v]) (.const arg [v]), so this far everything is working correctly when Lean does it for me.

But in my tactic I want to construct such expressions myself, and I don't know which functions exist to deal with level params like this, nor do I know much theory regarding level params (though I'm guessing this will be some kind of unification problem). Any pointers?

Currently I essentially re-implemented "mkAppN" myself to some degree, since I need to partially apply some function parameters with some specific pattern (context: I'm doing some monomorphization). As such, I have a recursive function which goes through a forall telescope, and in each step does:

def myfunc := do
  Meta.forallBoundedTelescope expr (some 1) fun fvars body => do
    ...
    let body' := body.replaceFvar fvars[0]! arg
    myfunc body'

I can't use mkAppOptM' here since we're dealing with foralls instead of lambdas. But I think the problem stems from the replaceFvar, since arg contains levelParams with name v, which do not exist in the context that I'm working with, and replaceFVar is not smart enough to unify them with anyhing.

[Reid Barton]

It sounds like something is wrong with arg already, if it contains universe level parameters that are not in scope

[Reid Barton]

I thought the question was going to go in the direction of: how do I work out what universe parameters to pass to T, so that it type checks with arg.

[Reid Barton]

I guess the answer to that would be something like: apply T to a fresh level metavariable, and then unify the types before doing replaceFvar.

[Max Nowak 🐉]

Hm, yeah, now that you say it, arg does contain universe level parameters that are not in scope. I didn't realize that was the key problem.

I construct my own T' given T, specifically I have an expression T arg₁ arg₂ and want to monomorphize it to T_arg₁ arg₂ for example.

[Reid Barton]

Anyways the theory of how universes occur in expressions is pretty simple: only constants (i.e. top-level definitions, instances, etc) can quantify over universe levels, they always do so at the outermost position, and you always specify all the universe parameters when referring to a constant.

[Max Nowak 🐉]

Yeah that took me a little while to fully wrap my head around. Helps to imagine they are essentially binders, but since it's so simple, a list with names is enough.

[Reid Barton]

It's the same way quantification over types works in standard Haskell, if that helps

[Max Nowak 🐉]

I skipped Haskell and went directly for Idris and Lean, unfortunately :P. But I understand how levels work now, just not how to handle them easily in metaprogramming. Currently looking at the metavar approach you suggested.

[Max Nowak 🐉]

Can I just disable universe checking? It's actually not very important for what I'm doing.
(Googling "lean unsafe level" did not bring up the results I thought it would xD)

[Reid Barton]

Kind of. Do you actually need universe polymorphism at all?
If you're trying to use existential types or something then I think with unsafe you can write inductive types that ignore the universe rules.

[Max Nowak 🐉]

I specified isUnsafe := true to addDecl, and it still complains about invalid reference to undeclared universe parameter.

[Max Nowak 🐉]

I do not need universe polymorphism at all, in fact, I won't even have polymorphism when I'm done haha. This is all just an intermediate step, and I eventually end up with something I can shove into an SMT solver.

[Reid Barton]

Oh, if you are making a new universe-polymorphic definition, then you need to include the parameters in the declaration.

[Max Nowak 🐉]

Do you know of a function to collect all of them? There is Lean.collectLevelParams, but it needs to be run in some monad and it feels like some internal function.

[Kyle Miller]

I think you're just expected to write (Lean.collectLevelParams {} e).params. I don't know exactly why they're designed this way, but my guess has been that this lets you easily take the union across multiple expressions.

[Kyle Miller]

like (Lean.collectLevelParams (Lean.collectLevelParams {} e1) e2).params (or you could imagine a fold across a List or Array).

[Max Nowak 🐉]

Ah, yeah, that makes sense I suppose.

[Reid Barton]

Depending on what you're doing, you might already know in advance what the universe parameters of the new definition should be

[Max Nowak 🐉]

Reid Barton said:

I guess the answer to that would be something like: apply T to a fresh level metavariable, and then unify the types before doing replaceFvar.

I can't quite make out what you meant with this. The problem (as we found earlier today) is that arg already has concrete level params when given to myfunc. How would a metavariable help here?

[Reid Barton]

This was meant to be an answer to how to figure out the correct universe parameters for T

[Max Nowak 🐉]

Given an inductive type inductive T : τ where | ctors..., in order to find all its levelParams, it is sufficient to check τ, right? I don't have to scan the ctors for extra levelParams.

[Max Nowak 🐉]

And second question, all ctors have the exact same level params on them as well? (Some small experimentation with #check T.c seems to allude to that)

[Max Nowak 🐉]

If the answers to those questions are true, I think I found a somewhat-proper way of dealing with level params, using something like
Lean.instantiateLevelParams T.type T.levelParams levelParamsFromConst.

[Max Nowak 🐉]

Oh my dog it works. I can't believe it took me a whole day to figure this out.