GADTs, Constraints and type equality.

gadts_type_equality.hs

-- CONSTRAINT kind:
--  * fully-saturated typeclasses
--  * tuples of other CONSTRAINTS
--  * type equalities.

-- In regular haskell this is restricted:
-- 1. We can't mention type variables in the arguments unless they're also in
--   the result.
-- 2. We can't /constrain/ the values of the input using any typeclasses.

-- :set -XGADTs removes these restrictions

data List a = Nil | Cons a (List a)

-- is isomorphic

Nil  :: List a
Cons :: a -> List a -> List a

-- Type equality in GADTs:

data Expr a where
  LitInt :: Int -> Expr Int

-- desugared

data Expr_ a =
    (a ~ Int)  => LitInt' Int
-- When we pattern match on a data constructor which contains a constraint, this satisfied constraint comes back into scope. 
-- That is, a function of type Expr a -> a can return an Int when pattern matching on LitInt, but return a Bool when matching on LitBool. 
-- The type equality constraining a only comes back into scope after pattern matching on the data constructor that contains it.

-- Example

data ShowList where
  Nil  :: ShowList
  Cons :: Show a => a -> ShowList -> ShowList

-- Pattern-matching brings the constraint Show a into scope again:

instance Show ShowList where
  show  ShowNil             = "[]"
  show (ShowCons head tail) = show head ++ " : " ++ show tail
-- ^^^^ 'a' is an existential variable: it only exist on the scope of the constructor function