Interesting `withAssignableSyntheticOpaque` `isDefEq` bug

Stream: lean4

[Thomas Murrills]

I figure this has to do with delayed-assigned metavariables. Consider the following apparent refine bug:

example : (fun _ : Nat => 2) = (fun _ => 2) := by
  refine (?_ : (fun _ : Nat => ?e) = _) -- unknown free variable '_uniq.39413'

This seems to actually be due to elabTermEnsuringType:

import Lean

open Lean Meta Elab Tactic in
elab "test1 " stx:term : tactic => withMainContext do
  discard <| elabTermEnsuringType (←`(term|(?_ : $stx))) (← getMainTarget)

example : (fun _ : Nat => 2) = (fun _ => 2) := by
  test1 (fun _ : Nat => ?e) = _ -- unknown free variable '_uniq.46964'

which in turn seems to be due to an issue with isDefEq under withAssignableSyntheticOpaque:

import Lean

open Lean Meta Elab Tactic in
elab "test2 " stx:term : tactic => withMainContext do
  let e ← elabTerm stx none
  discard <| withAssignableSyntheticOpaque <| isDefEq e (← getMainTarget)

example : (fun _ : Nat => 2) = (fun _ => 2) := by
  test2 (fun _ : Nat => ?e) = _ -- unknown free variable '_uniq.48582'

Removing withAssignableSyntheticOpaque fixes the issue.

Note: replacing the underscore on the rhs of the = with the explicit term fixes the issue as well.

[Kyle Miller]

It seems to be that there's a bug in how ?... holes are abstracted? Just elaborating the term fun _ : Nat => ?_ leads to an expression with a metavariable that (through delayed assignment) is a metavariable with a type with the offending unbound fvar.

import Lean

open Lean Meta Elab Tactic in
elab "test" stx:term : tactic => withMainContext do
  let e ← Term.elabTerm stx none
  logInfo m!"e = {e}"
  let mvs ← getMVars e
  logInfo m!"mvars = {mvs.map Expr.mvar}\n{← mvs.mapM MVarId.isDelayedAssigned}"

example : False := by
  test fun _ : Nat => ?_
  /-
  e = fun x ↦ ?m.4341 x
  mvars = [?m.4341, ?m.4339]
  [true, false]
  -- ?m.4341 : (x : Nat) → ?m.4340 x
  -- ?m.4339 : ?m.4340 _uniq.4336
  -/
  test fun _ : Nat => _
  /-
  e = fun x ↦ ?m.4348 x
  mvars = [?m.4348]
  [false]
  -- ?m.4348 : (x : Nat) → ?m.4347 x
  -/

[Thomas Murrills]

Oh interesting! Hmmm...the offending fvar is present in local context of the mvar that has that fvar in its type, at least, though.

import Lean

open Lean Meta Elab Tactic

def showLCtxFVars (m : MVarId) : MetaM (List Name) := m.withContext do
  return (← getLCtx).fvarIdToDecl.toList.map (·.1.name)

elab "test" stx:term : tactic => withMainContext do
  let e ← Term.elabTerm stx none
  logInfo m!"e = {e}"
  let mvs ← getMVars e
  let fvars ← liftM <| mvs.mapM showLCtxFVars
  let types ← liftM <| mvs.mapM MVarId.getType
  logInfo m!"mvars = {mvs.map Expr.mvar}\n{fvars}\n{types}\n{← mvs.mapM MVarId.isDelayedAssigned}"

example : False := by
  test fun _ : Nat => ?_
  /-
  mvars = [?m.7027, ?m.7025]
  [[_uniq.7019], [_uniq.7019, _uniq.7022]]
  [(x : Nat) → ?m.7026 x, ?m.7026 _uniq.7022]
  [true, false]
  -/

If all the eventual delayed-assignment-related substitutions worked as intended, this would be ok, right?