<thirdofmay18081814goya> {-# 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’