Equality constraints
Overview
One of the extensions that GHC’s Core language has over System F are equality constraints.
Equality constraints also appear in the surface language (i.e., in Haskell itself):
code:equality.hs
a ~ b
is a constraint that requires a and b to be equal.
Class constraints are translated to dictionary arguments in Core (and at run-time), whereas equality constraints appear in Core, but are not present at run-time.
code:example.hs
data Vec :: Nat -> * -> * where
Nil :: Vec Zero a
(:*) :: a -> Vec n a -> Vec (Suc n) a
-- can also be written as
data Vec :: Nat -> * -> * where
Nil :: (n ~ Zero ) => Vec n a
(:*) :: (n ~ Suc n') => a -> Vec n' a -> Vec n a
Useful links