Unification not working on simple expected case.

[ericrbg]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

example (a b c : Nat) : a = b → a * c = b * c := congrArg _ --fails, works with (· * c) requires you to explicitly spell out the function. In lean3, this is not required, and often used in mathlib.

Expected behavior: Success.

Actual behavior:

type mismatch
  congrArg ?m.56535
has type
  ?m.56533 = ?m.56534 → ?m.56535 ?m.56533 = ?m.56535 ?m.56534 : Prop
but is expected to have type
  a = b → a * c = b * c : Prop

Reproduces how often: 100%

Versions

Lean (version 4.0.0-nightly-2023-01-16, commit 5349a08, Release)
OSX Ventura 13.1, M1 Mac

[ericrbg]

Just want to confirm that this is still an issue on new Lean4 releases.

[semorrison]

@leodemoura, do we know what exactly changed in Lean4 that resulted in this change in behaviour? I don't know here whether to say this is an unavoidable regression due to some deeper change, or something that could potentially be addressed.

[Kha]

@semorrison I believe this is

lean4/src/Lean/Elab/Config.lean

Line 14 in 29b09b0

In Lean3 and Lean 4, we used to use the quasi-pattern approximation during elaboration.

Indeed, carefully arranging the proof of a similar example such that Lean is sure that a may be used in the hole but b/c may not (making it a regular pattern unification problem) makes it work.

example : ∀ (a b c : Nat), b = c → b * a = c * a :=
  fun a =>
    let f := _
    fun b c => congrArg f  -- replace `f` with `_` to break it