Type promotion was introduced in the same paper as kind polymorphism (Giving Haskell a Promotion, by Yorgey et al in 2012). This represented a major leap forward for Haskell's type-level programming capabilities.
Let's explore type promotion in the context of a type-level programming example. We want to create a list where the type itself contains information about the list size.
To represent numbers at type level, we use the age-old Peano numbering which describes the natural numbers (1,2,3, ...) in a recursive manner:
data Zero = Zero
deriving Show
data Succ n = Succ n
deriving Show
one = Succ Zero
two = Succ oneWe'll use this with the understanding that certain bad expressions are still allowed:
badSucc1 = Succ 10 -- :: Succ Int badSucc2 = Succ False -- :: Succ Bool
Our size-aware list type Vec is represented as a GADT:
-- requires
-- {-# LANGUAGE GADTs #-}
-- {-# LANGUAGE KindSignatures #-}
data Vec :: (* -> * -> *) where
Nil :: Vec a Zero
...