Explicitly mark match case as impossible

Stream: new members

[aron]

In my function f is there a way to explicitly mark the .e cases as impossible?

inductive A : (things : List Nat) → Type where
  | a : A []
  | b : A []
  | c : A []
  | d : A []
  | e : A [1]

def f (x : A []) (y : A []) :=
  match x, y with
  | .a, .a => true
  | .b, .b => true
  | .c, .c => true
  | .d, .d => true
  | .e, _ => nomatch x -- type mismatch
  | _, .e => nomatch y -- type mismatch
  | _, _ => false

The type checker (correctly) doesn't let me match on them because

type mismatch
  A.e
has type
  A [1] : Type
but is expected to have type
  A [] : Type

but since my final pattern is the fallback _, _I want to make it explicit that the .e pattern should be impossible. So that if I make any change to my code which will make it not impossible that I'll be warned about that and not let it silently fall through. Is there a way to do this?

[Eric Wieser]

Can you just drop the final fall through case entirely?

[aron]

My actual type has a large number of variants and I don't want to have to enumerate every permutation of them in the last case because that would be n^2 patterns, so not really no :(

Enumerating all variants would go from n^2 to n if Lean allowed for inner pattern matching like OCaml does:

type a = A | B | C | D | E

let f x y =
  match x, y with
  | A, A -> true
  | B, B -> true
  | C, C -> true
  | D, D -> true
  | (A | B | C | D), (A | B | C | D) -> false
  | E, _
  | _, E -> ...

but it doesn't look like Lean supports that

def f (x : A []) (y : A []) :=
  match x, y with
  | .a, .a => true
  | .b, .b => true
  | .c, .c => true
  | .d, .d => true
  | (.a | .b | .c | .d), (.a | .b | .c | .d) => false
--     ^^ unexpected token '|'; expected ')', ',' or ':'
  | .e, _ => nomatch x
  | _, .e => nomatch y

[Eric Wieser]

That might be worth a feature request, though I don't imagine it will be prioritized