Misleading error: `match` leads to an error about `cases` where no tactic is used

[MiddleAdjunction]

Prerequisites

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

• [X] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
• [X] Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.
• [X] 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

Consider the following seemingly correct dependent pattern matching using match:

inductive LTE : (n m : Nat) → Type
  | base  : LTE 0 0
  | less  : LTE n m → LTE n       (m + l)
  | equal : LTE n m → LTE (n + l) (m + l)

open LTE

def comp_LTE (N : LTE n₁ n₂) (M : LTE n₂ n₃) : LTE n₁ n₃ :=
  match N , M with -- <-- error points [HERE]
  | N'       , base     => N'
  | N'       , less  M' => less  (comp_LTE N' M')
  | less  N' , equal M' => less  (comp_LTE N' M')
  | equal N' , equal M' => equal (comp_LTE N' M')

Running the code leads to the following misleading error message:

tactic 'cases' failed, nested error:
dependent elimination failed, failed to solve equation
  0 = n✝.add l✝
at case @equal after processing
  _, _, _, base, _
the dependent pattern matcher can solve the following kinds of equations
- <var> = <term> and <term> = <var>
- <term> = <term> where the terms are definitionally equal
- <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil

Notice the code does not use cases, or any tactics.

Context

I raised this issue on a Discord server (Lean 4 anarchy); the description above summarises the issue fairly well.

Steps to Reproduce

You can reproduce the error by running the code.

Expected behavior: match is a commonly used construct, and related error messages should refer to the surface language rather than the internals (e.g., cases)

Actual behavior: match leads to an error about cases

Versions

[4.12.0-nightly-2024-10-22]

Impact

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