HList in Idris

HList.idr

using (x : Type, P : x -> Type)
    data HList : (P : x -> Type) -> List x -> Type where
        Nil : HList P []
        (::) : {head : x} -> {tail : List x} -> P head -> HList P tail -> HList P (head :: tail)

head : {h : ty} -> {t : List ty} -> {P : ty -> Type} -> HList P (h :: t) -> P h
head (h :: _) = h

tail : {h : ty} -> {t : List ty} -> {P : ty -> Type} -> HList P (h :: t) -> HList P t
tail (_ :: t) = t

tupleHList : HList (\x : Type => (x, x)) [Nat]
tupleHList = (1,1) :: Nil

example : (Nat, Nat)
example = head tupleHList