data UnitT        = Unit              deriving Show
data Sum aT bT    = Inl aT | Inr bT   deriving Show
data Prod aT bT   = Prod aT bT        deriving Show

data EP bT cT = EP {from :: (bT -> cT), to :: (cT -> bT)}

data Rep tT where
  RUnit  ::                      Rep UnitT
  RInt   ::                      Rep Int
  RChar  ::                      Rep Char
  RSum   :: Rep aT -> Rep bT ->  Rep (Sum aT bT)
  RProd  :: Rep aT -> Rep bT ->  Rep (Prod aT bT)
  RString ::                        Rep String
  RCon    ::  String -> Rep aT ->   Rep aT
  RType   ::  EP bT cT -> Rep cT ->  Rep bT

type RepAlgebra r  = (r
                      ,r
                      ,r
                      ,r
                      ,forall a b. a -> b -> r
                      ,forall a b. a -> b -> r
                      ,forall a  . String -> a -> r
                      ,forall a b. EP a b -> r -> r
                      )

-- This works, but is extremely bloated, ugly, and plain yuk
foldRep :: RepAlgebra r -> Rep a -> r
foldRep a@(unit, int, char, string, sum, prod, con, t) (RUnit)   = unit
foldRep a@(unit, int, char, string, sum, prod, con, t) (RInt)    = int
foldRep a@(unit, int, char, string, sum, prod, con, t) (RChar)   = char
foldRep a@(unit, int, char, string, sum, prod, con, t) (RString) = string
foldRep a@(unit, int, char, string, sum, prod, con, t) (RSum ra rb)  = sum (foldRep a ra) (foldRep a rb)
foldRep a@(unit, int, char, string, sum, prod, con, t) (RProd ra rb) = prod (foldRep a ra) (foldRep a rb)
foldRep a@(unit, int, char, string, sum, prod, con, t) (RCon  l  ra) = con  l (foldRep a ra)
foldRep a@(unit, int, char, string, sum, prod, con, t) (RType ep ra) = t ep (foldRep a ra)

-- This doesn't compile:
foldRep' :: RepAlgebra r -> Rep a -> r
foldRep' (unit, int, char, string, sum, prod, con, t) = f
  where
        f (RUnit)   = unit
        f (RInt)    = int
        f (RChar)   = char
        f (RString) = string
        f (RSum ra rb)  = sum (f ra) (f rb)
        f (RProd ra rb) = prod (f ra) (f rb)
        f (RCon  l  ra) = con  l (f ra)
        f (RType ep ra) = t ep (f ra)
{-

GADT pattern match in non-rigid context for `RUnit'
      Probable solution: add a type signature for `f'
    In the pattern: RUnit
    In the definition of `f': f (RUnit) = unit
    In the definition of `foldRep':
        foldRep (unit, int, char, string, sum, prod, con, t)
                  = f
                  where
                      f (RUnit) = unit
                      f (RInt) = int
                      f (RChar) = char
                      f (RString) = string
                      f (RSum ra rb) = sum (f ra) (f rb)
                      f (RProd ra rb) = prod (f ra) (f rb)
                      f (RCon l ra) = con l (f ra)
                      f (RType ep ra) = t ep (f ra)
-}

-- Adding the type doesn't help, how can I convince the compiler that r in the type of f is the same as in the type of foldRep'?

foldRep' :: RepAlgebra r -> Rep a -> r
foldRep' (unit, int, char, string, sum, prod, con, t) = f
  where f :: Rep a -> r
        f (RUnit)   = unit
        f (RInt)    = int
        f (RChar)   = char
        f (RString) = string
        f (RSum ra rb)  = sum (f ra) (f rb)
        f (RProd ra rb) = prod (f ra) (f rb)
        f (RCon  l  ra) = con  l (f ra)
        f (RType ep ra) = t ep (f ra)

{-
    Couldn't match expected type `r1' against inferred type `r'
      `r1' is a rigid type variable bound by
           the type signature for `f' at gadtalgebra.hs:67:22
      `r' is a rigid type variable bound by
          the type signature for `foldRep'' at gadtalgebra.hs:65:23
    In the expression: t ep (f ra)
    In the definition of `f': f (RType ep ra) = t ep (f ra)
    In the definition of `foldRep'':
        foldRep' (unit, int, char, string, sum, prod, con, t)
                   = f
                   where
                       f :: Rep a -> r
                       f (RUnit) = unit
                       f (RInt) = int
                       f (RChar) = char
                       f (RString) = string
                       f (RSum ra rb) = sum (f ra) (f rb)
                       f (RProd ra rb) = prod (f ra) (f rb)
                       f (RCon l ra) = con l (f ra)
                       f (RType ep ra) = t ep (f ra)
-}

-- And now with the ScopedTypeVariables extension:
foldRep' :: forall r a. RepAlgebra r -> Rep a -> r
foldRep' (unit, int, char, string, sum, prod, con, t) = f
  where f :: Rep a -> r
        f (RUnit)   = unit
        f (RInt)    = int
        f (RChar)   = char
        f (RString) = string
        f (RSum ra rb)  = sum (f ra) (f rb)
        f (RProd ra rb) = prod (f ra) (f rb)
        f (RCon  l  ra) = con  l (f ra)
        f (RType ep ra) = t ep (f ra)
{-
    Occurs check: cannot construct the infinite type: aT = Sum aT bT
    In the pattern: RSum ra rb
    In the definition of `f': f (RSum ra rb) = sum (f ra) (f rb)
    In the definition of `foldRep'':
        foldRep' (unit, int, char, string, sum, prod, con, t)
                   = f
                   where
                       f :: Rep a -> r
                       f (RUnit) = unit
                       f (RInt) = int
                       f (RChar) = char
                       f (RString) = string
                       f (RSum ra rb) = sum (f ra) (f rb)
                       f (RProd ra rb) = prod (f ra) (f rb)
                       f (RCon l ra) = con l (f ra)
                       f (RType ep ra) = t ep (f ra)
-}