Crazy rcases success

Stream: mathlib4

[Patrick Massot]

@Mario Carneiro is there any way we could get rcases to fail in:

import Mathlib

example (n p q : ℕ) (h : n ≥ max p q) : True := by
  rcases h with ⟨h₁ : n ≥ p, h₂ : n ≥ q⟩
  all_goals trivial

I understand that Nat.le is indeed an inductive predicate, but the type ascriptions in the above example are completely wrong.

[Mario Carneiro]

would a linter warning suffice? The rcases pattern ignoring behavior is necessary to write some dependent patterns, but a pattern that is never used seems like a lint candidate

[Patrick Massot]

It wouldn't suffice for my purpose but I can work around that. For general use a linter would be better than nothing.

[Kevin Buzzard]

I've always been surprised that things like

import Mathlib.Tactic

example (h : 37 = 37) : True := by
  rcases h with ⟨⟨⟨⟩⟩⟩
  sorry

work (I sometimes find myself scrambling around trying to name variables which have come out as inaccessible, and start tinkering with pointy brackets to sort things out). Is this the same phenomenon?

[Mario Carneiro]

I think it could be a (default-disabled) option rcases.allowUnusedPatterns, since I think the cases where this is needed are rare and the cases where it is confusing are less rare