{-# LANGUAGE GADTs, DataKinds, NoStarIsType, KindSignatures #-} import Data.Kind data Nat where Zero :: Nat Succ :: Nat -> Nat data Vec :: Type -> Nat -> Type where Nil :: Vec a Zero Cons :: a -> Vec a n -> Vec a (Succ n) -- a :: Type; n :: Nat vTail :: Vec a (Succ n) -> Vec a n vTail (Cons _ xs) = xs vTail Nil = Nil -- error, Could not deduce ‘n ~ Zero’