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
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).