MVarId.assign vs IsDefEq

Stream: lean4

[Floris van Doorn]

The docstring for docs#Lean.MVarId.assign suggest to use docs#Lean.Meta.isDefEq instead. However, this doesn't have the same behavior for me:

import Lean.Elab.Tactic.Simp

open Lean Meta Elab Tactic Term

elab "abstract" tacs:ppDedent(tacticSeq) : tactic => do
  let target ← getMainTarget
  let goal ← getMainGoal
  let newGoal ← mkFreshExprMVar target
  setGoals [newGoal.mvarId!]
  evalTactic tacs
  let newGoal ← instantiateMVars newGoal
  let newMVars ← getMVars newGoal
  -- _ ← goal.assign newGoal -- uncomment this line and the kernel error disappears
  _ ← isDefEq (mkMVar goal) newGoal
  setGoals newMVars.toList

/--
error: unsolved goals
case left
f : True ∧ True → Nat
n : Nat
⊢ True

case right
f : True ∧ True → Nat
n : Nat
⊢ True
---
error: (kernel) declaration has metavariables '_example'
-/
#guard_msgs in
example (f : True ∧ True → Nat) (n : Nat) :
  n = f (by abstract constructor) := sorry

The isDefEq generates a kernel error, while the assign doesn't. What causes the difference? Am I doing something wrong? (This is a bare-bones version of #22296, and I think I can safely use assign in this case.)

[Eric Wieser]

(deleted)

[Aaron Liu]

isDefEq does not assign synthetic opaque metavariables, so it is resolved with proof irrelevance.

[Eric Wieser]

withAssignableSyntheticOpaque <| isDefEq indeed makes it work

[Kyle Miller]

What I usually see is doing isDefEq on the types, and then using MVarId.assign if that succeeds. The batteries function docs#Lean.MVarId.assignIfDefeq does this for you.

MVarId.assign does no checking of anything (not even occurs checks), and I think it probably shouldn't be used by metaprogrammers.

[Floris van Doorn]

Aaron Liu said:

isDefEq does not assign synthetic opaque metavariables, so it is resolved with proof irrelevance.

Thanks!

Is there already a place where I can learn what the different kinds metavariables are, so that I can learn what this means? (The reference manual currently doesn't, but I just opened leanprover/reference-manual#329 asking for it.)

[Kyle Miller]

There's at least the docstring to docs#Lean.MetavarKind

Synthetic mvars have a docs#Lean.Elab.Term.SyntheticMVarKind entry

Synthetic opaque metavariables are generally used for goals. They exist because unification/elaboration might otherwise solve for a goal metavariable using an unassigned non-goal metavariable, causing the goal to disappear from the goal list.