gistfile1.hs

{-# LANGUAGE GADTs          #-}
{-# LANGUAGE DataKinds      #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies   #-}
{-# LANGUAGE RankNTypes     #-}

data N = Z | S N

data Vector :: * -> N -> * where
  Nil  :: Vector a 'Z
  Cons :: a -> Vector a n -> Vector a ('S n)

type family LT (m :: N) (n :: N) :: Bool
type instance LT m 'Z          = 'False
type instance LT 'Z ('S m)     = 'True
type instance LT ('S m) ('S n) = LT m n

data SN :: N -> * where
  SZ :: SN 'Z
  SS :: forall (n::N). SN n -> SN ('S n)

nth :: (LT m n) ~ 'True => SN m -> Vector a n -> a
nth SZ (Cons a _) = a
nth (SS s') (Cons _ as) = nth s' as