test.v

Set Universe Polymorphism.
Set Printing Universes. Set Printing All.
Unset Strict Universe Declaration.

(**
A vector is a list of size n whose elements belong to a set A. *)

Inductive t A : nat -> Type :=
  |nil : t A 0
  |cons : forall (h:A) (n:nat), t A n -> t A (S n).

Local Notation "[ ]" := (nil _) (format "[ ]").
Local Notation "h :: t" := (cons _ h _ t) (at level 60, right associativity).

Definition cast: forall {A} {m} (v: t A m) {n}, m = n -> t A n.
Proof.
  refine (fix cast {A m} (v: t A m) {struct v} :=
            match v in t _ m' return forall n, m' = n -> t A n with
            |[] => fun n => match n with
                        | 0 => fun _ => []
                        | S _ => fun H => False_rect _ _
                        end
            |h :: w => fun n => match n with
                            | 0 => fun H => False_rect _ _
                            | S n' => fun H => h :: (cast w n' (f_equal pred H))
                            end
            end); discriminate.
Defined.

Check @cast@{Set Set}.

Definition cast': forall {A} {m} (v: t A m) {n}, m = n -> t A n
  := ltac:(
  refine (fix cast' {A m} (v: t A m) {struct v} :=
            match v in t _ m' return forall n, m' = n -> t A n with
            |[] => fun n => match n with
                        | 0 => fun _ => []
                        | S _ => fun H => False_rect _ _
                        end
            |h :: w => fun n => match n with
                            | 0 => fun H => False_rect _ _
                            | S n' => fun H => h :: (cast' w n' (f_equal pred H))
                            end
            end); discriminate
       ).

Check @cast'@{Set}.