Unify level mvars

Stream: lean4

[Marcus Rossel]

I was hoping I could use isDefEq to unify level mvars, but apparently this doesn't work:

import Lean
open Lean Meta

-- Eq.{?_uniq.1061}
#eval do
  let e₁ := Expr.const `Eq [1]
  let e₂ ← mkConstWithFreshMVarLevels `Eq
  unless ← isDefEq e₁ e₂ do throwError "not defeq"
  return e₂

What would be the right approach here?

[Marcus Rossel]

Ah, as always the solution was instantiateMVars e₂.

[Notification Bot]

Marcus Rossel has marked this topic as resolved.

[Notification Bot]

Marcus Rossel has marked this topic as unresolved.

[Marcus Rossel]

Actually, in this example even instantiating mvars doesn't help:

import Lean
open Lean Meta

#eval do -- OfNat.ofNat.{?_uniq.1} Nat (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) instOfNatNat.{0}
  let u ← mkFreshLevelMVar
  let e₁ := mkAppN (.const `OfNat.ofNat [0]) #[(.const `Nat []), (mkNatLit 0), (.const `instOfNatNat [0])]
  let e₂ := mkAppN (.const `OfNat.ofNat [u]) #[(.const `Nat []), (mkNatLit 0), (.const `instOfNatNat [0])]
  unless ← isDefEq e₁ e₂ do throwError "not defeq"
  let e₂' ← instantiateMVars e₂
  IO.println e₂'

[Kyle Miller]

isDefEq assumes that your expressions are well-typed. I wouldn't be surprised if it's skipping steps it knows it can skip with this assumption.

[Kyle Miller]

How are you in this situation where you have a metavariable in an expression like that, where it's not already constrained by the other arguments?

[Kyle Miller]

By the way, docs#Lean.mkNatLit is how you make a natlit expression for Nat

[Kyle Miller]

There's also docs#Lean.Meta.mkNumeral for general types

[Marcus Rossel]

Kyle Miller said:

How are you in this situation where you have a metavariable in an expression like that, where it's not already constrained by the other arguments?

I'm using an external solver to generate a sequence of rewrites for a proof, and the expression language of that external solver doesn't have a notion universe levels. Now I'm trying to reconstruct Lean expressions from those external expression and my idea was to fill in the missing pieces with mvars which can then all be inferred during further steps.
Is there some other way to tell Lean to figure out the level mvars? Or is this not generally possible?

[Eric Wieser]

I was expecting instantiateLevelMVars to help here, but it doesn't seem to