GADTs and Close Type Families

GadtsAndClosedTypeFamilies.hs

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

module GadtClosedFamilyTest where

-- -------------------------------------------------------------------------- --
-- type level peano numbers

data Nat = Z | S Nat

data SNat (n :: Nat) :: * where
    SZ :: SNat 'Z
    SS :: SNat n -> SNat ('S n)

-- -------------------------------------------------------------------------- --
-- parity

type family Parity (n :: Nat) :: Nat where
    Parity 'Z = 'Z
    Parity ('S 'Z) = 'S 'Z
    Parity ('S ('S n)) = Parity n

data EvenNat (n :: Nat) where
    EvenNat :: Parity n ~ 'Z => EvenNat n

evenNat :: Parity n ~ 'Z => SNat n -> EvenNat n
evenNat SZ = EvenNat
evenNat (SS (SS n)) = case evenNat n of EvenNat -> EvenNat

-- Results in:
-- 
-- @
-- GadtsClosedFamilies.hs:40:1: warning:
--    Pattern match(es) are non-exhaustive
--    In an equation for ‘evenNat'’: Patterns not matched: (SS SZ)
-- @
--
-- The constraint @Parity n ~ 'Z@ is brought into scope only when pattern
-- matching on the result @EventNat n@. It's possible to add a case
-- @evenNat' (SS SZ) = undefined@. However what is the type of @undefined@
-- here? Is it possible to add a type annotation that GHC accepts? Is there
-- a bottom type that could be used a type parameter for @SNat@?
--
evenNat' :: SNat n -> EvenNat n
evenNat' SZ = EvenNat
evenNat' (SS (SS n)) = case evenNat' n of EvenNat -> EvenNat