calc does not try to unify with expected type

[collares]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

Although example : 3 + 9 = 12 := rfl works, the following code

example : 3 + 9 = 12 :=
  calc
    3 + 9 = 12 := rfl

fails with

type mismatch
  rfl
has type
  3 + 9 = 3 + 9 : Prop
but is expected to have type
  3 + 9 = 12 : Prop

Replacing rfl with by rfl or by exact rfl above makes it work, but I think it shouldn't be necessary.

Context

Phil Wadler encountered this issue while porting his "Programming Language Foundations in Agda" book to Lean: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Debugging.20an.20issue.20with.20calc.20mode

This is a regression pointed out by Wadler after upgrading from an old nightly. I bisected it and it works on the 2023-01-05 nightly and fails on the 2023-01-06 one. According to https://github.com/leanprover/lean4-nightly/releases/tag/nightly-2023-01-06 this points to fedf235, but see also 474f1a4 where this was worked around for the show tactic.

In particular, plfa/plfl@a4684b2 contains three more calc uses which now require type ascriptions (and didn't need them before fedf235).

Versions

Lean 4.3.0-rc2 on Linux

Impact

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

[Kha]

Seems to have been fixed!

[collares]

Indeed, this fails on v4.10.0 but works on v4.11.0! Not sure which change fixed it, will bisect later.

(cc @wadler, since the ascriptions added in plfa/plfl@a4684b2 aren't needed since Lean v4.11.0)

[collares]

Bisected to #4596:

commit 6080e3dd5cc76d9f8807de19d6575f517ee11899
Author: Leonardo de Moura <leomoura@amazon.com>
Date:   Tue Jul 2 15:42:47 2024 +0200

    fix: enforce `isDefEqStuckEx` at `unstuckMVar` procedure (#4596)
    
    Closes #2736
    
    See comment at `ExprDefEq.lean` for explanation.
    Side effects:
    - Improved error messages in two tests.
    - Had to improve `getSuccesses` procedure at `App.lean`. It now
      discards candidates that contain postponed elaboration problems.
      If it is too disruptive for Mathlib, we should try to discard the
      ones that have postponed metavariables.