The Coq mailing list

[Sylvain Salvati <sylvain.salvati AT univ-lille.fr>]

Dear Coq-Club,

Can anyone explain why the following term defined in the standard
library (c.f. Coq.Vectors.VectorDef) does type-check:

Definition case0 {A} (P:Vector.t A 0 -> Type) (H:P (Vector.nil A)) v:P v :=
match v with
|[] => H
|_ => fun devil => False_ind (@IDProp) devil
end.

I moreover checked that the following term also type-check:

Definition my_case0 {A} (P:Vector.t A 0 -> Type) (H:P (Vector.nil A)) v:P v :=
match v with
|[] => H
end.

So it seems to me that in the first term coq is able to see that the
second branch of the match cannot be executed and thus one can put any
phony term. Is it correct? If so why does the standard library use the
first term instead of the second one?

I checked the mailing list and found that a similar question has been
asked 7 years ago but did not receive any answer.

Thanks for your help,

S.