{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}

import Language.Syntactic

data T ctx o where
  Only :: Sat ctx o  => o -> T ctx o
  TT   :: Sat ctx o1 => T ctx o1 -> (o1 -> o2) -> T ctx o2

-- | Representation of a 'Show' constraint
data ShowCtx

instance Show a => Sat ShowCtx a
  where
    data Witness ShowCtx a = Show a => ShowWit
    witness = ShowWit

show' :: forall a . Sat ShowCtx a => a -> String
show' a = case witness :: Witness ShowCtx a of
    ShowWit -> show a

instance Show (T ShowCtx o) where
  show (Only o)  = "Only " ++ (show' o)
  show (TT t1 f) = "TT (" ++ (show' t1) ++ ")"

t :: Sat ctx Int => T ctx Bool
t = TT (Only (3 :: Int)) even

test = show (t :: T ShowCtx Bool)