Change in pattern matching; expected behaviour?

Stream: lean4

[Scott Morrison]

While bumping mathlib4 I had to change

protected lemma add_comm : ∀ a b : ℤ, a + b = b + a
| (n : ℕ), (m : ℕ) => by simp [Nat.add_comm]
| (_ : ℕ), -[1+ _] => rfl
| -[1+ _], (_ : ℕ) => rfl
| -[1+ _], -[1+ _] => by simp [Nat.add_comm]

to

protected lemma add_comm : ∀ a b : ℤ, a + b = b + a
| (n : ℕ), (m : ℕ) => by simp [Nat.add_comm]
| (n : ℕ), -[1+ _] => rfl
| -[1+ _], (m : ℕ) => rfl
| -[1+ _], -[1+ _] => by simp [Nat.add_comm]

as the (_ : ℕ) patterns are now causing errors:

type mismatch
  ?m.11643
has type
  ℕ : Type
but is expected to have type
  ℤ : Type

I don't think this is a particularly bad regression, but just wanted to check in case it was an unintentional side-effect.

[Leonardo de Moura]

@Scott Morrison Thanks for reporting this issue. Do you know which commit triggered the issue?

[Mario Carneiro]

I don't know which commit it is, but here is a #mwe that can be used to bisect:

example : Int → Nat
| (_ : Nat) => 0
| Int.negSucc n => 0

[Scott Morrison]

bisected and reported as https://github.com/leanprover/lean4/issues/742.

[Leonardo de Moura]

@Scott Morrison @Mario Carneiro Thanks for the feedback (mwe and exact commit), it is very useful.

[Leonardo de Moura]

Fixed this issue.