Level MVar Unification

[marcusrossel]

When calling isDefEq on expressions containing level mvars, those level mvars aren't necessarily assigned. This causes problems, e.g. when using Config.Encoding.eraseConstLvls.
Using a syntactic unification like the example below won't work as we still need to be able to unify syntactically different expressions if we want to (a) use natlit-conversions and (b) skip proofs by refl in proof reconstruction.

-- Note: This function expects its input expression to be normalized (cf. `Egg.normalize`).
def unify : Expr → Expr → MetaM Bool
  | e₁@(.mvar _), e₂ | e₁, e₂@(.mvar _) => isDefEq e₁ e₂
  | e₁@(.bvar _), e₂@(.bvar _) | e₁@(.fvar _), e₂@(.fvar _) | e₁@(.lit _), e₂@(.lit _) =>
    return e₁ == e₂
  | .app e₁₁ e₁₂, .app e₂₁ e₂₂ | .lam _ e₁₁ e₁₂ _, .lam _ e₂₁ e₂₂ _
  | .forallE _ e₁₁ e₁₂ _, .forallE _ e₂₁ e₂₂ _ =>
    unify e₁₁ e₂₁ <&&> unify e₁₂ e₂₂
  | .sort lvl₁, .sort lvl₂ => isLevelDefEq lvl₁ lvl₂
  | .const name₁ lvls₁, .const name₂ lvls₂ => do
    unless name₁ == name₂ && lvls₁.length == lvls₂.length do return false
    let mut result := true
    for lvl₁ in lvls₁, lvl₂ in lvls₂ do
      result ← (return result) <&&> isLevelDefEq lvl₁ lvl₂
    return result
  | .mdata .., _ | _, .mdata .. | .proj .., _ | _, .proj .. | .letE .., _ | _, .letE .. =>
    panic! "'Egg.unify' received non-normalized expression"
  | _, _ => return false

[marcusrossel]

An approach that might work is to perform the syntactic level mvar unification as far as the syntax is equal and the perform isDefEq.

[marcusrossel]

This shouldn't be an issue anymore as universe level erasure doesn't work anyway (cf. issue #20).