inductive I : Type :=
| K : list (pair Type I) -> I
let rec f t on t : I -> bool :=
match t with
| k ((nat, x)::_) -> f x
| k _ -> true
is now accepted. the arg of k used to be recursive but not the head of the list
(only its tail) since constructors types were not specialized on actual left
arguments (and the information that the type of the head contains I was lost).