{-# 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