isDefEq creates type-incorrect terms when applying isDefEqSingleton rule

[kmill]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Given a projection of a metavariable for a one-field structure that's unified with a term of the wrong type, the result is a type-incorrect term assigned to the metavariable.

Context

[Broader context that the issue occurred in. If there was any prior discussion on the Lean Zulip, link it here as well.]

Steps to Reproduce

Consider the following code:

import Lean

open Lean

structure foo where
  bar : Nat

#eval show MetaM Unit from do
  let lhs := Expr.const ``foo []
  let m ← Meta.mkFreshExprMVar lhs
  let rhs := Expr.app (.const ``foo.bar []) m
  let defeq? ← Meta.isDefEq lhs rhs
  let m ← instantiateMVars m
  logInfo m!"unifiable? {defeq?}"
  logInfo m!"m is{indentExpr m}"
  logInfo m!"m is type correct? {← Meta.isTypeCorrect m}"

Expected behavior: We should see unifiable? false in the output.

Actual behavior: Instead this outputs

unifiable? true
m is
  { bar := foo }
m is type correct? false

Versions

Lean 4.16.0-nightly-2024-12-19
Target: x86_64-unknown-linux-gnu

Additional Information

Changing the structure to have more than one field causes the unification to correctly fail.

Reported on Zulip

Impact

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