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

MiddleAdjunction commented 1 week ago

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.

MiddleAdjunction commented 2 days ago

The following is potentially another manifestation of this issue (misleading error message):

inductive C0  : Prop  where
| mkC0 (p : Prop) : C0

def C0.p (c0 : C0) : Prop := 
  match c0 with 
  | mkC0 p => p

leads to

 tactic 'cases' failed, nested error:
tactic 'induction' failed, recursor 'C0.casesOn' can only eliminate into Prop
motive : C0 → Sort ?u.26
h_1 : (p : Prop) → motive ⋯
c0✝ : C0
⊢ motive c0✝
 after processing

nomeata commented 2 days ago

Thanks for the report. Note that match and cases are very related. It’s certainly possible to fix this message, by passing down the “user-visible name”, but given the relatively minor impact, we probably won’t complicate the code this way for now.

leanprover / lean4