content: {-# LANGUAGE GADTs, KindSignatures,
               MultiParamTypeClasses, FunctionalDependencies #-}
  
  -- Program from Josef Svenningsson
  
  -- Just a short explanation of the program. It contains
  -- some class declarations capturing some definitions from
  -- category theory. Further down he have a data type for well typed
  -- lambda expressions using GADTs. Finally we have a
  -- function defining the semantics for lambda terms called
  -- 'interp'.
  
  -- Made GHC 6.4 bleat
  --    Quantified type variable `t' is unified with
  --        another quantified type variable `terminal'
  --    When trying to generalise the type inferred for `interp'
  
  
  module Bug where
  
  import Data.Kind (Type)
  
  class Category arr where
    idA  :: arr a a
    comp :: arr a b -> arr b c -> arr a c
  
  class Category arr =>
     Terminal terminal arr | arr -> terminal where
    terminal :: arr a terminal
  
  class Category arr =>
        ProductCategory prod arr | arr -> prod  where
    first  :: arr (prod a b) a
    second :: arr (prod a b) b
    pair   :: arr a b -> arr a c -> arr a (prod b c)
  
  class Category arr =>
        CoproductCategory coprod arr | arr -> coprod where
    inLeft  :: arr a (coprod a b)
    inRight :: arr b (coprod a b)
    ccase   :: arr a c -> arr b c -> arr (coprod a b) c
  
  class ProductCategory prod arr =>
        Exponential exp prod arr | arr -> exp where
    eval   :: arr (prod (exp a b) a) b
    curryA :: arr (prod c a) b -> arr c (exp a b)
  
  
  class (Exponential exp prod arr, Terminal terminal arr) =>
    CartesianClosed terminal exp prod arr | arr -> terminal exp prod
  
  data V prod env t where
    Z :: V prod (prod env t) t
    S :: V prod env t -> V prod (prod env x) t
  
  data Lambda terminal (exp :: Type -> Type -> Type) prod env t where
      Unit :: Lambda foo exp prod env foo
      Var  :: V prod env t -> Lambda terminal exp prod env t
  {-    Lam  :: Lambda terminal exp prod (prod env a) t
           -> Lambda terminal exp prod env (exp a t)
      App  :: Lambda terminal exp prod env (exp t t')
           -> Lambda terminal exp prod env t -> Lambda terminal exp prod env t'
  -}
  
  interp :: CartesianClosed terminal exp prod arr =>
            Lambda terminal exp prod s t -> arr s t
  interp (Unit)       = terminal -- Terminal terminal arr => arr a terminal
  -- interp (Var Z)      = second
  -- interp (Var (S v))  = first `comp` interp (Var v)
  -- interp (Lam e)      = curryA (interp e)
  -- interp (App e1 e2)  = pair (interp e1) (interp e2) `comp` eval
  