Dear Coq Enthusiasts,

during a discussion meandering a bot off topic at Adding more trigonometry in Reals I found that one is forced to supply patterns to a match which don’t type check. A piece from the linked discussion demonstrating this is:

```
Require Import Vector.
Import VectorNotations.
Import Fin.
Inductive sumn (n : nat) (P : Vector.t Prop n) : Set :=
sumi (i : Fin.t n) (p : Vector.nth P i) : sumn n P.
Lemma lt_eq_lt_dec_1: forall n m : nat, sumn 3 [ n < m; n = m; m < n ].
Proof.
intros n m.
pose proof Compare_dec.lt_eq_lt_dec n m as H.
destruct H as [[H|H]|H].
apply (sumi _ _ F1); assumption.
apply (sumi _ _ (FS F1)); assumption.
apply (sumi _ _ (FS (FS F1))); assumption.
Qed.
Definition match_typechecktest (n m : nat) : nat :=
match lt_eq_lt_dec_1 n m with
| sumi _ _ (FS (FS (FS F1))) _ => 1
| sumi _ _ _ _ => 0
end.
```

Obviously the type of `lt_eq_lt_dec_1 n m`

is `sumn 3 ...`

while the first pattern would only typecheck against a `sumn n ...`

for `n>=4`

.

Looking at the typing rule for match at The match … with … end construction I must admit I didn’t see where the type of the constructor arguments is defined - as physicist I find this still a bit hard to read. But I guess for correctness it is not required that the match pattern arguments have the correct type - the match patterns just need to be structurally complete.

But I wonder if there is a dependent match which would allow to discard all patterns which don’t type check and if this doesn’t exist, what it would take to implement it. I could imagine that there are no other places in the kernel where the type checking of a term depends on that a certain term does *not* type check. On the other hand the `dependent destruction`

tactic gets this right and ends up (applied repeatedly) with the 3 possibilities one would expect for a `sumn 3`

(see the first link for an example).

Best regards,

Michael