module Data.HList where

infixr 5 :.
data List as where
    Nil :: List '[]
    (:.) :: a -> List as -> List (a ': as)

instance Eq (List '[]) where
    Nil == Nil = True

instance (Eq a, Eq (List as)) => Eq (List (a ': as)) where
    x:.xs == y:.ys = x == y && xs == ys

instance Ord (List '[]) where
    Nil `compare` Nil = EQ

instance (Ord a, Ord (List as)) => Ord (List (a ': as)) where
    (x:.xs) `compare` (y:.ys) = x `compare` y <> xs `compare` ys