https://gmalecha.github.io/reflections/2017/pattern-matching-on-data-kinds

ShapeIndexed.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE LambdaCase #-}
module ShapeIndexed where
import Data.Constraint


-- | The type of unary natural numbers (repeated here so the file is
-- self-contained).
data Nat = O | S Nat

-- | A dependent eliminator for @Nat@.
class KnownNat (l :: Nat) where
  elimNat :: f 'O -- ^ the 0 case
          -> (forall n. KnownNat n => f ('S n)) -- ^ the successor case
          -> f l

-- | Instances for the constructors
instance KnownNat 'O where
  elimNat f _ = f
instance KnownNat n => KnownNat ('S n) where
  elimNat _ f = f

-- | The type of length-indexed vectors.
data Vector (l :: Nat) τ where
  Vnil :: Vector O τ
  Vcons :: forall l τ. τ -> Vector l τ -> Vector ('S l) τ

instance Functor (Vector l) where
    fmap f Vnil = Vnil
    fmap f (Vcons x xs) = Vcons (f x) (fmap f xs)

-- | Implementation of @<*>@ for length-indexed vectors.
apVector :: Vector l (α -> β) -> Vector l α -> Vector l β
apVector Vnil Vnil = Vnil
apVector (Vcons f fs) (Vcons x xs) = Vcons (f x) (apVector fs xs)

-- | Implementation of @pure@ for length-indexed vectors.
pureVector :: forall α l. KnownNat l => α -> Vector l α
pureVector a = getPureVector $ elimNat (PureVector Vnil) mkCons
  where mkCons :: forall l. KnownNat l => PureVector α ('S l)
        mkCons = PureVector $ Vcons a (pureVector a)

-- Local type necessary to get around GHC's lack of type-level lambdas.
newtype PureVector α l = PureVector
  { getPureVector :: Vector l α }


instance KnownNat l => Applicative (Vector l) where
    pure = pureVector
    (<*>) = apVector

-- | Convert a list into a length-indexed vector.
-- Returns @Nothing@ if the length is not long enough.
fromList :: forall l α. KnownNat l => [α] -> Maybe (Vector l α)
fromList = getFromList $ elimNat (FromList $ const $ Just Vnil) mkCons
  where mkCons :: forall l. KnownNat l => FromList α ('S l)
        mkCons = FromList $ \ case
                                [] -> Nothing
                                (x:xs) -> Vcons x <$> fromList xs

-- Local type to get around GHC's lack of type-level lambdas.
newtype FromList α l = FromList
  { getFromList :: [α] -> Maybe (Vector l α) }

vtail :: Vector ('S l) t -> Vector l t
vtail (Vcons _ xs) = xs

-- | Monadic bind on vectors.
bindVector :: Vector l t -> (t -> Vector l u) -> Vector l u
bindVector Vnil _ = Vnil
bindVector (Vcons x xs) f = case f x of
                              Vcons z _ -> Vcons z (bindVector xs $ vtail . f)

-- | A @Monad@ instance.
instance KnownNat l => Monad (Vector l) where
  return = pure
  (>>=) = bindVector

-- | We can learn the structure of a @Nat@ if we have a vector.
learnLength :: Vector l τ -> Dict (KnownNat l)
learnLength Vnil = Dict
learnLength (Vcons _ xs) = case learnLength xs of
                             Dict -> Dict

An alternative method for allowing pattern matching is to use a singleton version of Nat, which is indexed by the kind Nat and where every type is inhabited by exactly one value.

For example like this

data SNat n where
  O' :: SNat 'O
  S' :: SNat n -> SNat ('S n)

To create a value, we still need the type class

class KnownNat (l :: Nat) where
  natValue :: SNat n

instance KnownNat 'O where
  natValue = O'
instance KnownNat n => KnownNat ('S n) where
  natValue = S' getSNat

Now we can create a value and pattern match on it like any other value whenever we need. The constraints (n ~ 'S m) or (n ~ 'Z) will automatically come into scope from the pattern matching.

fromList :: forall l α. KnownNat l => [α] -> Maybe (Vector l α)
fromList = fromList' (natVal @l)
  where
    fromList' :: forall l α. SNat l -> [α] -> Maybe (Vector l α)
    fromList' Z' _ = Just Vnil
    fromList' (S' l) [] = Nothing
    fromList' (S' l) (x:xs) = Vcons x <$> fromList' l xs

Another option is to use non-recursive (implicitly recursive) singletons with a dictionary in them instead

data SNat n where
   O' :: SNat 'O
   S' :: KnownNat n => SNat ('S n)

which means that pattern matching will bring the relevant constraints into scope and you won't need to pass around the value n explicitly.

You can also combine the methods for maximum flexibility

data SNat n where
   O' :: SNat 'O
   S' :: KnownNat n => SNat n -> SNat ('S n)