MData and unification

Stream: lean4

[Alexander Bentkamp]

When unifying a meta variable with an expression that has metadata on the top level, the metadata disappears:

import Lean

open Lean
open Lean.Meta

#check Expr

def test : MetaM Unit := do
  let e ← mkAnnotation `test (mkConst `Nat)
  let m ← mkFreshExprMVar none
  let _ ← isDefEq e m
  let m ← instantiateMVars m
  trace[Meta.debug] "e: {toString e}"
  trace[Meta.debug] "m: {toString m}"

set_option trace.Meta.debug true

#eval test
/-
[Meta.debug] e: [mdata test:1 Nat]
[Meta.debug] m: Nat
-/

Is this the intended behavior? I'd prefer if it wasn't :grinning:

[Leonardo de Moura]

Yes, this is the intended behavior. In this particular example, it would be feasible to modify isDefEq to make sure the metadata is part of the expression assigned to m, but it would not be a general solution. Not sure why you need the metadata to be preserved.