failed defeq check with mvar

Stream: lean4

[Tomas Skrivan]

I have a defeq check with meta variable that fails for some reason. It happens inside of a new tactic I'm writing and in any attempt of minimizing it the defeq check passes.

I'm checking

fun x x => Function.invFun (fun x => x - s) 0 =?= ?g

and it fails. I'm expecting that fun x x => Function.invFun (fun x => x - s) 0 gets assigned to ?g

The trace says

    [Meta.isDefEq] ❌ fun x x => Function.invFun (fun x => x - s) 0 =?= ?g
      [Meta.isDefEq] fun x x => Function.invFun (fun x => x - s) 0 [nonassignable] =?= ?g [assignable]
      [Meta.isDefEq.assign] ❌ ?g := fun x x => Function.invFun (fun x => x - s) 0
        [Meta.isDefEq.assign.outOfScopeFVar] s @ ?g [] := fun x x => Function.invFun (fun x => x - s) 0
        [Meta.isDefEq.foApprox] ?g [] := fun x x => Function.invFun (fun x => x - s) 0
        [Meta.isDefEq.constApprox] ?g [] := fun x x => Function.invFun (fun x => x - s) 0
        [Meta.isDefEq.assign.outOfScopeFVar] s @ ?g [] := fun x x => Function.invFun (fun x => x - s) 0

The type of ?g and the expression are the same and it is Unit → Unit → R

Any tip on how to debug this? Any trace option I can't turn on to reveal more info? Is there explanation of outOfScopeFVar, foApprox and constApprox traces?

[Jannis Limperg]

The outOfScopeFVar seems to indicate that an fvar from the potential assignment, so s, is not present in the local context of ?g.

[Tomas Skrivan]

That would make sense why it fails. I have to investigate, but s should be in the context of ?g. Maybe I have messed up when creating the mvar.

[Tomas Skrivan]

Indeed s is not in the context of ?g. Now I have to figure out why :)