isDefEq fails in presence of unassignable metavariable

Description

In the unification problem ?a =?= (fun x => ?a) b, when ?a is not assignable then unification fails.

Context

Zulip discussion, reported by Jovan Gerbscheid.

Steps to Reproduce

Expected behavior: the following test returns true. Actual behavior: it returns false.

import Lean

open Lean Meta

elab "foo" : term => do
  let a ← mkFreshExprSyntheticOpaqueMVar (mkConst ``Nat)
  let c := mkApp (mkLambda `x .default (mkConst ``Nat) a) (mkConst ``Nat.zero)
  return toExpr <| ← isExprDefEq a c

set_option trace.Meta.isDefEq true
#check foo

This can be triggered with metacontext depth as well:

elab "foo" : term => do
  let a ← mkFreshExprMVar (mkConst ``Nat)
  let c := mkApp (mkLambda `x .default (mkConst ``Nat) a) (mkConst ``Nat.zero)
  return toExpr <| ← withNewMCtxDepth do isExprDefEq a c

Additional information

The following test helps localize the issue to isDefEqQuickOther returning LBool.false.

import Lean

open Lean Meta

elab "foo" : term => do
  let a ← mkFreshExprSyntheticOpaqueMVar (mkConst ``Nat)
  let c := mkApp (mkLambda `x .default (mkConst ``Nat) a) (mkConst ``Nat.zero)
  withTheReader Meta.Context (fun c => {c with config := {c.config with isDefEqStuckEx := true}}) do
  return toExpr <| ← isExprDefEq a c

set_option trace.Meta.isDefEq true
set_option trace.Meta.isDefEq.stuck true
#check foo
-- ...
-- [] ?m.654 [nonassignable] =?= (fun x ↦ ?m.654) Nat.zero [nonassignable] 
-- [stuck] ?m.654 =?= (fun x ↦ ?m.654) Nat.zero

Versions

#eval Lean.versionString
-- "4.6.0-rc1"

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start with the provided reproducer using isExprDefEq and the trace output, then inspect the isDefEqQuickOther path identified in the issue. Confirm the behavior for an unassignable metavariable in both examples and verify that the expected equality result is returned.