Singleton type example

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

type family Cond (b :: Bool) (t :: k) (e :: k) :: k where
    Cond 'True t e = t
    Cond 'False t e = e

data Booly :: Bool -> * where
    Truey :: Booly 'True
    Falsey :: Booly 'False

item :: forall b . Booly b -> Cond b Int [Int]
item Truey = 42
item Falsey = [1, 2, 3]

main :: IO ()
main = putStrLn $ show $ item Falsey