Unknown universe metavariable

Stream: lean4

[Leni Aniva]

Consider this example

example : ∀ (n m: Nat), n + m = m + n := by
  intro n m
  rw [Nat.add_comm]

I'm trying to execute this example in Lean while inspecting its proof state

I have this function which elaborates an expression from a syntax

    syn <- Lean.Parser.runParserCategory
      (env := env)
      (catName := `term)
      (input := "∀ (n m: Nat), n + m = m + n")
      (fileName := "<stdin>")
  let termElabM : Lean.Elab.TermElabM (Except String Lean.Expr) :=
    try
      let expr ← Lean.Elab.Term.elabTerm syn
        (expectedType? := none)
        (catchExPostpone := false)
        (implicitLambda := true)
      return .ok expr
    catch ex => return .error (← ex.toMessageData.toString)

However when I procedurally run the same series of tactics on the expression generated by the above termElabM, I get the following error messages

#[unknown universe metavariable '?_uniq.9']

In comparison, if I extract the expression directly from env.find? name |>.get! |>.type (where name is Nat.add_comm), the series of tactics will result in 0 goals. How can I fix this issue? I think the problem is in the elaborator?

[Leni Aniva]

The same behaviour shows up if instead of elabTerm that I use elabType (which internally calls elabTerm.

[Leni Aniva]

If anyone is interested I can post a minimal example but I'm mainly just interested in how elabTerm's expression is different from the one from ConstantInfo.type

[Kyle Miller]

ConstantInfo.type uses the level variables from ConstantInfo.levelParams. What elabTerm does when it comes across a constant is that it uses fresh universe level metavariables. I'm just answering this question, but I'm not sure this will help with your earlier question.

The "unknown universe metavariable" error is pointing toward you using the expr in a different metavariable context than the one you generated it.

If you think that all the metavariables should be solved for right after elaborating, you could thrown in docs4#Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing before the return and then use instantiateMVars expr to substitute in all the solutions to all the metavariables.

[Leni Aniva]

Kyle Miller said:

ConstantInfo.type uses the level variables from ConstantInfo.levelParams. What elabTerm does when it comes across a constant is that it uses fresh universe level metavariables. I'm just answering this question, but I'm not sure this will help with your earlier question.

The "unknown universe metavariable" error is pointing toward you using the expr in a different metavariable context than the one you generated it.

If you think that all the metavariables should be solved for right after elaborating, you could thrown in docs4#Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing before the return and then use instantiateMVars expr to substitute in all the solutions to all the metavariables.

Yes. In my applications I have to save the Lean.Elab.Tactic.SavedState and resume it with state.term.restore. I'll try your suggestions. Thanks

[Leni Aniva]

Kyle Miller said:

ConstantInfo.type uses the level variables from ConstantInfo.levelParams. What elabTerm does when it comes across a constant is that it uses fresh universe level metavariables. I'm just answering this question, but I'm not sure this will help with your earlier question.

The "unknown universe metavariable" error is pointing toward you using the expr in a different metavariable context than the one you generated it.

If you think that all the metavariables should be solved for right after elaborating, you could thrown in docs4#Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing before the return and then use instantiateMVars expr to substitute in all the solutions to all the metavariables.

Is there a way to InstantiateMVars on the metavariables generated by tactics?

[Leni Aniva]

I tried with unsolvedGoals.forM Lean.instantiateMVarDeclMVars but executing a tactic like apply Or.inr still results in

tactic 'apply' failed, failed to unify
  ?a ∨ ?b
with
  q ∨ p
case inl
p q : Prop
h✝ : p
⊢ q ∨ p

I have the Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing right before executing the tactic:

        Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing
        let unsolvedGoals ← Lean.Elab.Tactic.run mvarId tac
        unsolvedGoals.forM Lean.instantiateMVarDeclMVars
        let nextState : Lean.Elab.Tactic.SavedState := {
          term := (← Lean.Elab.Term.saveState),
          tactic := { goals := unsolvedGoals }
        }
        return .ok nextState

[Leni Aniva]

The theorem I'm trying to prove is this one. It runs fine in the IDE but when I try to run the same sequence of tactics with Lean.Elab.Tactic.SavedState it gives the above error.

example: ∀ (p q: Prop), p ∨ q → q ∨ p := by
  intro p q h
  cases h
  apply Or.inr
  assumption
  apply Or.inl
  assumption