content: {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE ExistentialQuantification #-}
  {-# LANGUAGE TemplateHaskell #-}
  {-# LANGUAGE TypeFamilyDependencies #-}
  {-# LANGUAGE PolyKinds #-}
  module Main where
  
  import Data.Kind
  import Data.Proxy
  import Language.Haskell.TH hiding (Type)
  
  -- Anonymous tyvar binder example
  newtype Foo1 = Foo1 (Proxy '[False, True, False])
  
  -- Required (dependent) tyvar binder example
  type family Wurble k (a :: k) :: k
  newtype Foo2 a = Foo2 (Proxy (Wurble (Maybe a) Nothing))
  
  -- Non-injective type family example
  type family Foo3Fam1 (a :: Type) :: Type where
    Foo3Fam1 a = a
  type family Foo3Fam2 (a :: Foo3Fam1 b) :: b
  newtype Foo3 = Foo3 (Proxy (Foo3Fam2 Int))
  
  -- Injective type family example
  type family Foo4Fam1 (a :: Type) = (r :: Type) | r -> a where
    Foo4Fam1 a = a
  type family Foo4Fam2 (a :: Foo4Fam1 b) :: b
  newtype Foo4 = Foo4 (Proxy (Foo4Fam2 Int))
  
  $(return [])
  
  main :: IO ()
  main = do
    putStrLn $(reify ''Foo1 >>= stringE . pprint)
    putStrLn $(reify ''Foo2 >>= stringE . pprint)
    putStrLn $(reify ''Foo3 >>= stringE . pprint)
    putStrLn $(reify ''Foo4 >>= stringE . pprint)
  