Regression in coercion inference

Stream: lean4

[Mario Carneiro]

I noticed this while bumping mathlib4. It is easy enough to work around but I wanted to confirm the intentionality of this change:

example (a : Int) (b c : Nat) : a = ↑b - ↑c := sorry
-- failed to synthesize instance
--   HSub Nat Nat Int

This kind of syntax is not uncommon in mathported files since this is how you indicate where you want the coercion to go in lean 3. I'm guessing some change related to the 2 * n HMul stuff is related to this issue.

[Leonardo de Moura]

Thanks for pointing this out. I will take a look.

[Leonardo de Moura]

Pushed a fix for this issue. It improves the custom elaborator (binrel%) for binary relations. However, the new binrel% always puts coercions on the "leaves", and makes its behavior consistent with the binop% one. Example

theorem ex1 (a : Int) (b c : Nat) : a = ↑b - ↑c := sorry
#check ex1
-- ex1 : ∀ (a : Int) (b c : Nat), a = Int.ofNat b - Int.ofNat c
theorem ex2 (a : Int) (b c : Nat) : a = b - c := sorry
#check ex2
-- ex2 : ∀ (a : Int) (b c : Nat), a = Int.ofNat b - Int.ofNat c
theorem ex3 (a : Int) (b c : Nat) : a = ↑(b - c) := sorry
#check ex3
-- ex3 : ∀ (a : Int) (b c : Nat), a = Int.ofNat (b - c)

[Leonardo de Moura]

The fix is here: https://github.com/leanprover/lean4/commit/7ce0471f283feb37c313a09d15a27ea69a7f4eaa

[Leonardo de Moura]

The explanation for the regression is here: https://github.com/leanprover/lean4/commit/1768067aa0a6ac06526949bae1b918794819faf3