diff --git a/benchmarks/Dynamic.hs b/benchmarks/Dynamic.hs
--- a/benchmarks/Dynamic.hs
+++ b/benchmarks/Dynamic.hs
@@ -5,6 +5,8 @@
 import Data.Monoid
 
 import Data.TypeRep
+import Data.TypeRep.Types.Basic
+import Data.TypeRep.Types.Basic.Typeable ()
 
 import qualified Data.Dynamic as Base  -- For comparison
 
diff --git a/examples/Custom.hs b/examples/Custom.hs
new file mode 100644
--- /dev/null
+++ b/examples/Custom.hs
@@ -0,0 +1,49 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- This file demonstrates how to create one's own type universe
+
+module Custom where
+
+
+
+import Control.Monad
+
+
+
+import Language.Syntactic
+
+import Data.TypeRep.Representation
+import Data.TypeRep.TH
+
+
+
+-- Universe of types built using 'Bool', 'Int' and '[]'
+data Type sig
+  where
+    Bool_t :: Type (Full Bool)
+    Int_t  :: Type (Full Int)
+    List_t :: Type (a :-> Full [a])
+
+instance (Type :<: t) => Typeable t Bool where typeRep' = sugarSym Bool_t
+instance (Type :<: t) => Typeable t Int  where typeRep' = sugarSym Int_t
+
+instance (Type :<: t, Typeable t a) => Typeable t [a] where typeRep' = sugarSym List_t typeRep'
+
+deriveRender_forType ''Type
+deriveTypeEq ''Type
+deriveWitness ''Eq ''Type
+derivePWitness ''Eq ''Type
+deriveWitness ''Show ''Type
+derivePWitness ''Show ''Type
+deriveWitnessTypeable ''Type
+
+hlist :: [Dynamic Type]
+hlist = [toDyn True, toDyn (1 :: Int), toDyn [1,2,3,4 :: Int]]
+
+main = do
+    unless test $ fail "Test failed"
+    putStrLn "Test passed"
+  where
+    test = show hlist == "[True,1,[1,2,3,4]]"
+
diff --git a/examples/Simple.hs b/examples/Simple.hs
--- a/examples/Simple.hs
+++ b/examples/Simple.hs
@@ -1,30 +1,40 @@
+module Simple where
+
+
+
 import Control.Monad
 
 import Data.TypeRep
+import Data.TypeRep.Types.Basic
+import Data.TypeRep.Types.Basic.Typeable ()
 
-type MyUniverse = IntType :+: BoolType
 
+
+-- A universe of three types
+type MyUniverse = IntType :+: FloatType :+: BoolType
+
+-- A list with dynamically typed elements
 hlist :: [Dynamic MyUniverse]
 hlist = [toDyn True, toDyn (1 :: Int)]
-  -- Prints: [True,1]
 
+-- Dynamically typed addition for any numeric type
 addDyn :: (TypeEq ts ts, PWitness Num ts ts) =>
     Dynamic ts -> Dynamic ts -> Either String (Dynamic ts)
 addDyn (Dyn ta a) (Dyn tb b) = do
-    Dict <- typeEq ta tb
+    Dict <- typeEqM ta tb
     Dict <- pwit pNum ta
     return (Dyn ta (a+b))
 
-
-
-test1 = toDyn (1 :: Int) `addDyn` toDyn (2 :: Int)
-  -- Prints: Just 3
+test2 = toDyn (1 :: Int)   `addDyn` toDyn (2 :: Int)
+test3 = toDyn (3 :: Float) `addDyn` toDyn (4 :: Float)
 
 main = do
     unless t1 $ fail "Test 1 failed"
     unless t2 $ fail "Test 2 failed"
+    unless t3 $ fail "Test 3 failed"
     putStrLn "All tests passed"
   where
     t1 = show hlist == "[True,1]"
-    t2 = show (test1 :: Either String (Dynamic MyUniverse)) == "Right 3"
+    t2 = show (test2 :: Either String (Dynamic MyUniverse)) == "Right 3"
+    t3 = show (test3 :: Either String (Dynamic MyUniverse)) == "Right 7.0"
 
diff --git a/open-typerep.cabal b/open-typerep.cabal
--- a/open-typerep.cabal
+++ b/open-typerep.cabal
@@ -1,5 +1,5 @@
 name:                open-typerep
-version:             0.3.3
+version:             0.4
 synopsis:            Open type representations and dynamic types
 description:         This package uses Data Types à la Carte to provide open type representations
                      and dynamic types/coercions for open type universes.
@@ -51,20 +51,34 @@
   hs-source-dirs: src
 
   exposed-modules:
-    Data.TypeRep.Internal
-    Data.TypeRep
+    Data.TypeRep.Representation
+    Data.TypeRep.TH
+    Data.TypeRep.Types.Basic
+    Data.TypeRep.Types.Basic.Typeable
+    Data.TypeRep.Types.Tuple
+    Data.TypeRep.Types.Tuple.Typeable
+    Data.TypeRep.Types.IntWord
+    Data.TypeRep.Types.IntWord.Typeable
     Data.TypeRep.VarArg
+    Data.TypeRep
+    Language.Syntactic.TypeRep
+    Language.Syntactic.TypeRep.Sugar.BindingTR
+    Language.Syntactic.TypeRep.Sugar.TupleTR
+    Language.Syntactic.TypeRep.TupleConversion
 
   other-modules:
     Data.TypeRep.Sub
 
   build-depends:
     base        >=4 && <5,
+    base-orphans,
+      -- Only needed for GHC < 7.10
     constraints >=0.3,
     mtl         >=2.2.1,
       -- Smallest version that has Control.Monad.Except
-    syntactic   >=3,
-    tagged      >=0.4
+    syntactic   >=3.2,
+    tagged      >=0.4,
+    template-haskell
 
   default-language: Haskell2010
 
@@ -86,21 +100,25 @@
 test-suite examples
   type: exitcode-stdio-1.0
 
-  hs-source-dirs: examples
+  hs-source-dirs: examples tests
 
-  main-is: Simple.hs
+  main-is: Tests.hs
 
   default-language: Haskell2010
 
   build-depends:
+    base,
     open-typerep,
-    base
+    syntactic
 
   default-language: Haskell2010
 
   default-extensions:
     FlexibleContexts
+    FlexibleInstances
     GADTs
+    MultiParamTypeClasses
+    ScopedTypeVariables
     TypeOperators
 
 benchmark dynamic-bench
diff --git a/src/Data/TypeRep.hs b/src/Data/TypeRep.hs
--- a/src/Data/TypeRep.hs
+++ b/src/Data/TypeRep.hs
@@ -10,6 +10,7 @@
     , TypeRep
     , typeRep
     , TypeEq
+    , typeEqM
     , typeEq
     , matchCon
     , matchConM
@@ -17,35 +18,24 @@
     , PWitness
     , wit
     , pwit
+    , witTypeable
+    , pwitTypeable
       -- * Dynamic types
     , cast
     , gcast
     , Dynamic (..)
     , toDyn
     , fromDyn
-    , dynToInteger
-      -- * Type class witnessing
+      -- * Misc.
     , Any
-    , witTypeable
-    , pwitTypeable
+    , ShowClass (..)
     , pAny
+    , pDataTypeable
     , pEq
     , pOrd
     , pShow
     , pNum
     , pIntegral
-    , BoolType
-    , CharType
-    , IntType
-    , FloatType
-    , ListType
-    , FunType
-    , boolType
-    , charType
-    , intType
-    , floatType
-    , listType
-    , funType
       -- * Sub-universes
     , module Data.TypeRep.Sub
     ) where
@@ -57,6 +47,6 @@
 
 import Language.Syntactic ((:+:), Project (..), (:<:) (..), E (..))
 
-import Data.TypeRep.Internal
+import Data.TypeRep.Representation
 import Data.TypeRep.Sub
 
diff --git a/src/Data/TypeRep/Internal.hs b/src/Data/TypeRep/Internal.hs
deleted file mode 100644
--- a/src/Data/TypeRep/Internal.hs
+++ /dev/null
@@ -1,448 +0,0 @@
-{-# LANGUAGE UndecidableInstances #-}
-
--- | Open type representations and dynamic types
-
-module Data.TypeRep.Internal where
-
-
-
-import Control.Monad.Except
-import Data.Char (isAlphaNum)
-
-import Data.Constraint (Constraint, Dict (..))
-import Data.Proxy (Proxy (..))
-
-import Language.Syntactic
-
-
-
-----------------------------------------------------------------------------------------------------
--- * Type representations
-----------------------------------------------------------------------------------------------------
-
--- | 'Full'-indexed type representation
-type TR = AST
-
--- | This class provides reification of type @a@ in a universe @t@. @`Typeable` t a@ means that @a@
--- is in the type universe represented by @t@.
-class Typeable t a
-  where
-    typeRep' :: TR t (Full a)
-
--- | Representation of type @a@ in a type universe @t@
---
--- This type can also be seen as a witness that @a@ is a member of @t@ (i.e. @`Typeable` t a@); see
--- 'witTypeable'.
-newtype TypeRep t a = TypeRep { unTypeRep :: TR t (Full a) }
-  -- The newtype is mainly because 'TR' cannot be partially applied
-
-instance Render t => Show (TypeRep t a)
-  where
-    show = render . desugar
-
-instance Syntactic (TypeRep t a)
-  where
-    type Domain (TypeRep t a)   = t
-    type Internal (TypeRep t a) = a
-    desugar = unTypeRep
-    sugar   = TypeRep
-
--- | Reification of type @a@ in a type universe @t@
-typeRep :: Typeable t a => TypeRep t a
-typeRep = TypeRep typeRep'
-
--- | Equality on type representations
-class Render t => TypeEq t u
-  where
-    typeEqSym
-        :: (t sig1, Args (AST u) sig1)
-        -> (t sig2, Args (AST u) sig2)
-        -> Either String (Dict (DenResult sig1 ~ DenResult sig2))
-  -- The reason to have `Render` as a super class is not to leak unnecessary stuff in the type of
-  -- `typeEq`.
-
-instance (TypeEq t1 t, TypeEq t2 t) => TypeEq (t1 :+: t2) t
-  where
-    typeEqSym (InjL t1, as1) (InjL t2, as2) = typeEqSym (t1,as1) (t2,as2)
-    typeEqSym (InjR t1, as1) (InjR t2, as2) = typeEqSym (t1,as1) (t2,as2)
-    typeEqSym _ _ = throwError ""
-
-instance TypeEq Empty t
-  where
-    typeEqSym = error "typeEqSym: Empty"
-
--- | Equality on type representations
-typeEq :: (TypeEq t t, MonadError String m) => TypeRep t a -> TypeRep t b -> m (Dict (a ~ b))
-typeEq t1@(TypeRep s1) t2@(TypeRep s2) = case go (s1, Nil) (s2, Nil) of
-    Left _     -> throwError $ "type mismatch: " ++ show t1 ++ " /= " ++ show t2
-    Right Dict -> return Dict
-  where
-    go :: TypeEq t t
-      => (AST t sig1, Args (AST t) sig1)
-      -> (AST t sig2, Args (AST t) sig2)
-      -> Either String (Dict ((DenResult sig1 ~ DenResult sig2)))
-    go (Sym t1, as1)   (Sym t2, as2)   = typeEqSym (t1,as1) (t2,as2)
-    go (s1 :$ a1, as1) (s2 :$ a2, as2) = go (s1, a1 :* as1) (s2, a2 :* as2)
-    go _ _ = throwError ""
-
--- | Type constructor matching. This function makes it possible to match on type representations
--- without dealing with the underlying 'AST' representation.
---
--- For example, to check that a 'TypeRep' represents the type @a -> Int@ for some @a@:
---
--- > is_atoi :: (TypeEq t t, IntType :<: t) => TypeRep t a -> Bool
--- > is_atoi t
--- >     | [E ta, E tb] <- matchCon t
--- >     , Just _       <- typeEq ta intType = True
--- >     | otherwise                         = False
-matchCon :: TypeRep t c -> [E (TypeRep t)]
-matchCon = simpleMatch (\_ -> foldrArgs (\t -> (E (TypeRep t) :)) []) . unTypeRep
-
--- | Monadic version of 'matchCon'
---
--- > matchConM = return . matchCon
---
--- 'matchConM' is convenient when matching types in a monad, e.g.:
---
--- > do ...
--- >    [E ta, E tb] <- matchConM t
--- >    Dict         <- typeEq ta tb
--- >    ...
-matchConM :: Monad m => TypeRep t c -> m [E (TypeRep t)]
-matchConM = return . matchCon
-
--- | Show the name of type classes
-class ShowClass (p :: * -> Constraint)
-  where
-    -- | Show the name of a type class
-    showClass :: Proxy p -> String
-
--- | Witness a type constraint for a reified type
-class Witness p t u
-  where
-    witSym :: t sig -> Args (AST u) sig -> Dict (p (DenResult sig))
-
-instance (Witness p t1 t, Witness p t2 t) => Witness p (t1 :+: t2) t
-  where
-    witSym (InjL s) as = witSym s as
-    witSym (InjR s) as = witSym s as
-
-instance Witness p t t => Witness p (AST t) t
-  where
-    witSym (Sym s)  as = witSym s as
-    witSym (s :$ a) as = witSym s (a :* as)
-
--- | Partially witness a type constraint for a reified type
-class (ShowClass p, Render t) => PWitness p t u
-  where
-    pwitSym :: t sig -> Args (AST u) sig -> Either String (Dict (p (DenResult sig)))
-    pwitSym _ _ = throwError ""
-  -- The reason to have `Render` as a super class is not to leak unnecessary stuff in the type of
-  -- `pwit`.
-
-instance (PWitness p t1 t, PWitness p t2 t) => PWitness p (t1 :+: t2) t
-  where
-    pwitSym (InjL s) as = pwitSym s as
-    pwitSym (InjR s) as = pwitSym s as
-
--- | Default implementation of 'pwitSym' for types that have a 'Witness' instance
-pwitSymDefault :: Witness p t u =>
-    t sig -> Args (AST u) sig -> Either String (Dict (p (DenResult sig)))
-pwitSymDefault t = return . witSym t
-
--- | Witness a type constraint for a reified type
-wit :: forall p t a . Witness p t t => Proxy p -> TypeRep t a -> Dict (p a)
-wit _ (TypeRep a) = witSym a (Nil :: Args (AST t) (Full a))
-
--- | Partially witness a type constraint for a reified type
-pwit :: forall p t m a . (PWitness p t t, MonadError String m) =>
-    Proxy p -> TypeRep t a -> m (Dict (p a))
-pwit p t@(TypeRep a) = case go a Nil of
-    Left _  -> throwError $ unwords ["cannot deduce", showClass p, classArg]
-    Right a -> return a
-  where
-    st       = show t
-    classArg = if all isAlphaNum st then st else "(" ++ st ++ ")"
-
-    go :: AST t sig -> Args (AST t) sig -> Either String (Dict (p (DenResult sig)))
-    go (Sym s)  as = pwitSym s as
-    go (s :$ a) as = go s (a :* as)
-
-
-
-----------------------------------------------------------------------------------------------------
--- * Dynamic types
-----------------------------------------------------------------------------------------------------
-
--- | Safe cast (does not use @unsafeCoerce@)
-cast :: forall t a b . (Typeable t a, Typeable t b, TypeEq t t) =>
-    Proxy t -> a -> Either String b
-cast _ a = do
-    Dict <- typeEq (typeRep :: TypeRep t a) (typeRep :: TypeRep t b)
-    return a
-
--- | Safe generalized cast (does not use @unsafeCoerce@)
-gcast :: forall t a b c . (Typeable t a, Typeable t b, TypeEq t t) =>
-    Proxy t -> c a -> Either String (c b)
-gcast _ a = do
-    Dict <- typeEq (typeRep :: TypeRep t a) (typeRep :: TypeRep t b)
-    return a
-
--- | Dynamic type parameterized on a type universe
-data Dynamic t
-  where
-    Dyn :: TypeRep t a -> a -> Dynamic t
-
-toDyn :: Typeable t a => a -> Dynamic t
-toDyn = Dyn typeRep
-
-fromDyn :: forall t a . (Typeable t a, TypeEq t t) => Dynamic t -> Either String a
-fromDyn (Dyn t a) = do
-    Dict <- typeEq t (typeRep :: TypeRep t a)
-    return a
-
-instance (TypeEq t t, Witness Eq t t) => Eq (Dynamic t)
-  where
-    Dyn ta a == Dyn tb b
-        | Right Dict <- typeEq ta tb
-        , Dict       <- wit pEq ta
-        = a == b
-    _ == _ = False
-
-instance Witness Show t t => Show (Dynamic t)
-  where
-    show (Dyn t a) | Dict <- wit pShow t = show a
-
-
-
-----------------------------------------------------------------------------------------------------
--- * Specific types/classes
-----------------------------------------------------------------------------------------------------
-
--- | The universal class
-class    Any a
-instance Any a
-
-instance ShowClass Any          where showClass _ = "Any"
-instance ShowClass Eq           where showClass _ = "Eq"
-instance ShowClass Ord          where showClass _ = "Ord"
-instance ShowClass Show         where showClass _ = "Show"
-instance ShowClass Num          where showClass _ = "Num"
-instance ShowClass Integral     where showClass _ = "Integral"
-instance ShowClass (Typeable t) where showClass _ = "Typeable ..."
-
--- | Witness a 'Typeable' constraint for a reified type
-witTypeable :: Witness (Typeable t) t t => TypeRep t a -> Dict (Typeable t a)
-witTypeable = wit Proxy
-
--- | Partially witness a 'Typeable' constraint for a reified type
-pwitTypeable :: PWitness (Typeable t) t t => TypeRep t a -> Either String (Dict (Typeable t a))
-pwitTypeable = pwit Proxy
-
-pAny :: Proxy Any
-pAny = Proxy
-
-pEq :: Proxy Eq
-pEq = Proxy
-
-pOrd :: Proxy Ord
-pOrd = Proxy
-
-pShow :: Proxy Show
-pShow = Proxy
-
-pNum :: Proxy Num
-pNum = Proxy
-
-pIntegral :: Proxy Integral
-pIntegral = Proxy
-
-data BoolType  a where BoolType  :: BoolType  (Full Bool)
-data CharType  a where CharType  :: CharType  (Full Char)
-data IntType   a where IntType   :: IntType   (Full Int)
-data FloatType a where FloatType :: FloatType (Full Float)
-data ListType  a where ListType  :: ListType  (a :-> Full [a])
-data FunType   a where FunType   :: FunType   (a :-> b :-> Full (a -> b))
-
-instance Render BoolType  where renderSym BoolType  = "Bool"
-instance Render CharType  where renderSym CharType  = "Char"
-instance Render IntType   where renderSym IntType   = "Int"
-instance Render FloatType where renderSym FloatType = "Float"
-
-instance Render ListType
-  where
-    renderSym ListType = "[]"
-    renderArgs [a] ListType = "[" ++ a ++ "]"
-
-instance Render FunType
-  where
-    renderSym FunType = "(->)"
-    renderArgs [a,b] FunType = a ++ " -> " ++ b
-
-boolType :: (Syntactic a, BoolType :<: Domain a, Internal a ~ Bool) => a
-boolType = sugarSym BoolType
-
-charType :: (Syntactic a, CharType :<: Domain a, Internal a ~ Char) => a
-charType = sugarSym CharType
-
-intType :: (Syntactic a, IntType :<: Domain a, Internal a ~ Int) => a
-intType = sugarSym IntType
-
-floatType :: (Syntactic a, FloatType :<: Domain a, Internal a ~ Float) => a
-floatType = sugarSym FloatType
-
-listType
-    :: ( Syntactic list
-       , Syntactic elem
-       , Domain list ~ Domain elem
-       , ListType :<: Domain list
-       , Internal list ~ [Internal elem]
-       , elem ~ c e
-       , list ~ c l
-           -- These last equalities are used to help type inference by forcing the representations
-           -- to use the same type constructor (e.g. 'TR' or 'TypeRep')
-       )
-    => elem -> list
-listType = sugarSym ListType
-
-funType
-    :: ( Syntactic fun
-       , Syntactic a
-       , Syntactic b
-       , Domain fun ~ Domain a
-       , Domain fun ~ Domain b
-       , FunType :<: Domain fun
-       , Internal fun ~ (Internal a -> Internal b)
-       , a   ~ c x
-       , b   ~ c y
-       , fun ~ c z
-       )
-    => a -> b -> fun
-funType = sugarSym FunType
-
-instance (BoolType  :<: t)                             => Typeable t Bool     where typeRep' = boolType
-instance (CharType  :<: t)                             => Typeable t Char     where typeRep' = charType
-instance (IntType   :<: t)                             => Typeable t Int      where typeRep' = intType
-instance (FloatType :<: t)                             => Typeable t Float    where typeRep' = floatType
-instance (ListType  :<: t, Typeable t a)               => Typeable t [a]      where typeRep' = listType typeRep'
-instance (FunType   :<: t, Typeable t a, Typeable t b) => Typeable t (a -> b) where typeRep' = funType typeRep' typeRep'
-
-instance TypeEq BoolType  t where typeEqSym (BoolType, Nil)  (BoolType, Nil)  = return Dict
-instance TypeEq CharType  t where typeEqSym (CharType, Nil)  (CharType, Nil)  = return Dict
-instance TypeEq IntType   t where typeEqSym (IntType, Nil)   (IntType, Nil)   = return Dict
-instance TypeEq FloatType t where typeEqSym (FloatType, Nil) (FloatType, Nil) = return Dict
-
-instance TypeEq t t => TypeEq ListType t
-  where
-    typeEqSym (ListType, a :* Nil) (ListType, b :* Nil) = do
-        Dict <- typeEq (TypeRep a) (TypeRep b)
-        return Dict
-
-instance TypeEq t t => TypeEq FunType t
-  where
-    typeEqSym (FunType, a1 :* b1 :* Nil) (FunType, a2 :* b2 :* Nil) = do
-        Dict <- typeEq (TypeRep a1) (TypeRep a2)
-        Dict <- typeEq (TypeRep b1) (TypeRep b2)
-        return Dict
-
-instance (BoolType  :<: t) => Witness (Typeable t) BoolType  t where witSym BoolType  Nil = Dict
-instance (CharType  :<: t) => Witness (Typeable t) CharType  t where witSym CharType  Nil = Dict
-instance (IntType   :<: t) => Witness (Typeable t) IntType   t where witSym IntType   Nil = Dict
-instance (FloatType :<: t) => Witness (Typeable t) FloatType t where witSym FloatType Nil = Dict
-
-instance (ListType :<: t, Witness (Typeable t) t t) => Witness (Typeable t) ListType t
-  where
-    witSym ListType (a :* Nil)
-        | Dict <- witTypeable (TypeRep a) = Dict
-
-instance (FunType :<: t, Witness (Typeable t) t t) => Witness (Typeable t) FunType t
-  where
-    witSym FunType (a :* b :* Nil)
-        | Dict <- witTypeable (TypeRep a)
-        , Dict <- witTypeable (TypeRep b)
-        = Dict
-
-instance (BoolType  :<: t)                            => PWitness (Typeable t) BoolType  t where pwitSym = pwitSymDefault
-instance (CharType  :<: t)                            => PWitness (Typeable t) CharType  t where pwitSym = pwitSymDefault
-instance (IntType   :<: t)                            => PWitness (Typeable t) IntType   t where pwitSym = pwitSymDefault
-instance (FloatType :<: t)                            => PWitness (Typeable t) FloatType t where pwitSym = pwitSymDefault
-instance (ListType  :<: t, PWitness (Typeable t) t t) => PWitness (Typeable t) ListType  t where pwitSym ListType (a :* Nil) = do Dict <- pwitTypeable (TypeRep a); return Dict
-instance (FunType   :<: t, PWitness (Typeable t) t t) => PWitness (Typeable t) FunType   t where pwitSym FunType (a :* b :* Nil) = do Dict <- pwitTypeable (TypeRep a); Dict <- pwitTypeable (TypeRep b); return Dict
-
-instance Witness Any BoolType  t where witSym _ _ = Dict
-instance Witness Any CharType  t where witSym _ _ = Dict
-instance Witness Any IntType   t where witSym _ _ = Dict
-instance Witness Any FloatType t where witSym _ _ = Dict
-instance Witness Any ListType  t where witSym _ _ = Dict
-instance Witness Any FunType   t where witSym _ _ = Dict
-
-instance PWitness Any BoolType  t where pwitSym _ _ = return Dict
-instance PWitness Any CharType  t where pwitSym _ _ = return Dict
-instance PWitness Any IntType   t where pwitSym _ _ = return Dict
-instance PWitness Any FloatType t where pwitSym _ _ = return Dict
-instance PWitness Any ListType  t where pwitSym _ _ = return Dict
-instance PWitness Any FunType   t where pwitSym _ _ = return Dict
-
-instance                   Witness Eq BoolType  t where witSym BoolType  Nil = Dict
-instance                   Witness Eq CharType  t where witSym CharType  Nil = Dict
-instance                   Witness Eq IntType   t where witSym IntType   Nil = Dict
-instance                   Witness Eq FloatType t where witSym FloatType Nil = Dict
-instance Witness Eq t t => Witness Eq ListType  t where witSym ListType (a :* Nil) | Dict <- wit pEq (TypeRep a) = Dict
-
-instance                    PWitness Eq BoolType  t where pwitSym = pwitSymDefault
-instance                    PWitness Eq CharType  t where pwitSym = pwitSymDefault
-instance                    PWitness Eq IntType   t where pwitSym = pwitSymDefault
-instance                    PWitness Eq FloatType t where pwitSym = pwitSymDefault
-instance PWitness Eq t t => PWitness Eq ListType  t where pwitSym ListType (a :* Nil) = do Dict <- pwit pEq (TypeRep a); return Dict
-instance PWitness Eq FunType t
-
-instance                    Witness Ord BoolType  t where witSym BoolType  Nil = Dict
-instance                    Witness Ord CharType  t where witSym CharType  Nil = Dict
-instance                    Witness Ord IntType   t where witSym IntType   Nil = Dict
-instance                    Witness Ord FloatType t where witSym FloatType Nil = Dict
-instance Witness Ord t t => Witness Ord ListType  t where witSym ListType (a :* Nil) | Dict <- wit pOrd (TypeRep a) = Dict
-
-instance                     PWitness Ord BoolType  t where pwitSym = pwitSymDefault
-instance                     PWitness Ord CharType  t where pwitSym = pwitSymDefault
-instance                     PWitness Ord IntType   t where pwitSym = pwitSymDefault
-instance                     PWitness Ord FloatType t where pwitSym = pwitSymDefault
-instance PWitness Ord t t => PWitness Ord ListType  t where pwitSym ListType (a :* Nil) = do Dict <- pwit pOrd (TypeRep a); return Dict
-instance PWitness Ord FunType t
-
-instance                     Witness Show BoolType  t where witSym BoolType  Nil = Dict
-instance                     Witness Show CharType  t where witSym CharType  Nil = Dict
-instance                     Witness Show IntType   t where witSym IntType   Nil = Dict
-instance                     Witness Show FloatType t where witSym FloatType Nil = Dict
-instance Witness Show t t => Witness Show ListType  t where witSym ListType (a :* Nil) | Dict <- wit pShow (TypeRep a) = Dict
-
-instance                      PWitness Show BoolType  t where pwitSym = pwitSymDefault
-instance                      PWitness Show CharType  t where pwitSym = pwitSymDefault
-instance                      PWitness Show IntType   t where pwitSym = pwitSymDefault
-instance                      PWitness Show FloatType t where pwitSym = pwitSymDefault
-instance PWitness Show t t => PWitness Show ListType  t where pwitSym ListType (a :* Nil) = do Dict <- pwit pShow (TypeRep a); return Dict
-instance PWitness Show FunType t
-
-instance Witness Num IntType   t where witSym IntType   Nil = Dict
-instance Witness Num FloatType t where witSym FloatType Nil = Dict
-
-instance PWitness Num BoolType  t
-instance PWitness Num CharType  t
-instance PWitness Num IntType   t where pwitSym = pwitSymDefault
-instance PWitness Num FloatType t where pwitSym = pwitSymDefault
-instance PWitness Num ListType  t
-instance PWitness Num FunType   t
-
-instance Witness Integral IntType t where witSym IntType Nil = Dict
-
-instance PWitness Integral BoolType  t
-instance PWitness Integral CharType  t
-instance PWitness Integral IntType   t where pwitSym = pwitSymDefault
-instance PWitness Integral FloatType t
-instance PWitness Integral ListType  t
-instance PWitness Integral FunType   t
-
-dynToInteger :: PWitness Integral t t => Dynamic t -> Either String Integer
-dynToInteger (Dyn tr a) = do
-    Dict <- pwit pIntegral tr
-    return (toInteger a)
-
diff --git a/src/Data/TypeRep/Representation.hs b/src/Data/TypeRep/Representation.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/TypeRep/Representation.hs
@@ -0,0 +1,277 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | Open type representations and dynamic types
+
+module Data.TypeRep.Representation where
+
+
+
+import Control.Monad.Except
+import Data.Char (isAlphaNum)
+import qualified Data.Typeable as Typeable
+
+import Data.Constraint (Constraint, Dict (..))
+import Data.Proxy (Proxy (..))
+
+import Language.Syntactic
+
+
+
+----------------------------------------------------------------------------------------------------
+-- * Type representations
+----------------------------------------------------------------------------------------------------
+
+-- | 'Full'-indexed type representation
+type TR = AST
+
+-- | This class provides reification of type @a@ in a universe @t@. @`Typeable` t a@ means that @a@
+-- is in the type universe represented by @t@.
+class Typeable t a
+  where
+    typeRep' :: TR t (Full a)
+
+-- | Representation of type @a@ in a type universe @t@
+--
+-- This type can also be seen as a witness that @a@ is a member of @t@ (i.e. @`Typeable` t a@); see
+-- 'witTypeable'.
+newtype TypeRep t a = TypeRep { unTypeRep :: TR t (Full a) }
+  -- The newtype is mainly because 'TR' cannot be partially applied
+
+instance Render t => Show (TypeRep t a)
+  where
+    show = render . desugar
+
+instance Syntactic (TypeRep t a)
+  where
+    type Domain (TypeRep t a)   = t
+    type Internal (TypeRep t a) = a
+    desugar = unTypeRep
+    sugar   = TypeRep
+
+-- | Reification of type @a@ in a type universe @t@
+typeRep :: Typeable t a => TypeRep t a
+typeRep = TypeRep typeRep'
+
+-- | Equality on type representations
+class Render t => TypeEq t u
+  where
+    typeEqSym
+        :: (t sig1, Args (AST u) sig1)
+        -> (t sig2, Args (AST u) sig2)
+        -> Either String (Dict (DenResult sig1 ~ DenResult sig2))
+  -- The reason to have `Render` as a super class is not to leak unnecessary stuff in the type of
+  -- `typeEqM`/`typeEq`.
+
+instance (TypeEq t1 t, TypeEq t2 t) => TypeEq (t1 :+: t2) t
+  where
+    typeEqSym (InjL t1, as1) (InjL t2, as2) = typeEqSym (t1,as1) (t2,as2)
+    typeEqSym (InjR t1, as1) (InjR t2, as2) = typeEqSym (t1,as1) (t2,as2)
+    typeEqSym (t1,_) (t2,_) = throwError ""
+
+instance TypeEq Empty t
+  where
+    typeEqSym = error "typeEqSym: Empty"
+
+-- | Equality on type representations
+typeEqM :: (TypeEq t t, MonadError String m) => TypeRep t a -> TypeRep t b -> m (Dict (a ~ b))
+typeEqM t1@(TypeRep s1) t2@(TypeRep s2) = case go (s1, Nil) (s2, Nil) of
+    Left _     -> throwError $ "type mismatch: " ++ show t1 ++ " /= " ++ show t2
+    Right Dict -> return Dict
+  where
+    go :: TypeEq t t
+      => (AST t sig1, Args (AST t) sig1)
+      -> (AST t sig2, Args (AST t) sig2)
+      -> Either String (Dict ((DenResult sig1 ~ DenResult sig2)))
+    go (Sym t1, as1)   (Sym t2, as2)   = typeEqSym (t1,as1) (t2,as2)
+    go (s1 :$ a1, as1) (s2 :$ a2, as2) = go (s1, a1 :* as1) (s2, a2 :* as2)
+    go _ _ = throwError ""
+
+-- | Equality on type representations
+typeEq :: TypeEq t t => TypeRep t a -> TypeRep t b -> Maybe (Dict (a ~ b))
+typeEq t1 t2 = either (const Nothing) Just $ typeEqM t1 t2
+
+-- | Type constructor matching. This function makes it possible to match on type representations
+-- without dealing with the underlying 'AST' representation.
+--
+-- For example, to check that a 'TypeRep' represents the type @a -> Int@ for some @a@:
+--
+-- > is_atoi :: (TypeEq t t, IntType :<: t) => TypeRep t a -> Bool
+-- > is_atoi t
+-- >     | [E ta, E tb] <- matchCon t
+-- >     , Just _       <- typeEq ta intType = True
+-- >     | otherwise                         = False
+matchCon :: TypeRep t c -> [E (TypeRep t)]
+matchCon = simpleMatch (\_ -> foldrArgs (\t -> (E (TypeRep t) :)) []) . unTypeRep
+
+-- | Monadic version of 'matchCon'
+--
+-- > matchConM = return . matchCon
+--
+-- 'matchConM' is convenient when matching types in a monad, e.g.:
+--
+-- > do ...
+-- >    [E ta, E tb] <- matchConM t
+-- >    Dict         <- typeEq ta tb
+-- >    ...
+matchConM :: Monad m => TypeRep t c -> m [E (TypeRep t)]
+matchConM = return . matchCon
+
+-- | Witness a type constraint for a reified type
+class Witness p t u
+  where
+    witSym :: t sig -> Args (AST u) sig -> Dict (p (DenResult sig))
+
+instance (Witness p t1 t, Witness p t2 t) => Witness p (t1 :+: t2) t
+  where
+    witSym (InjL s) as = witSym s as
+    witSym (InjR s) as = witSym s as
+
+instance Witness p t t => Witness p (AST t) t
+  where
+    witSym (Sym s)  as = witSym s as
+    witSym (s :$ a) as = witSym s (a :* as)
+
+-- | Partially witness a type constraint for a reified type
+class (ShowClass p, Render t) => PWitness p t u
+  where
+    pwitSym :: t sig -> Args (AST u) sig -> Either String (Dict (p (DenResult sig)))
+    pwitSym _ _ = throwError ""
+  -- The reason to have `Render` as a super class is not to leak unnecessary stuff in the type of
+  -- `pwit`.
+
+instance (PWitness p t1 t, PWitness p t2 t) => PWitness p (t1 :+: t2) t
+  where
+    pwitSym (InjL s) as = pwitSym s as
+    pwitSym (InjR s) as = pwitSym s as
+
+-- | Default implementation of 'pwitSym' for types that have a 'Witness' instance
+pwitSymDefault :: Witness p t u =>
+    t sig -> Args (AST u) sig -> Either String (Dict (p (DenResult sig)))
+pwitSymDefault t = return . witSym t
+
+-- | Witness a type constraint for a reified type
+wit :: forall p t a . Witness p t t => Proxy p -> TypeRep t a -> Dict (p a)
+wit _ (TypeRep a) = witSym a (Nil :: Args (AST t) (Full a))
+
+-- | Partially witness a type constraint for a reified type
+pwit :: forall p t m a . (PWitness p t t, MonadError String m) =>
+    Proxy p -> TypeRep t a -> m (Dict (p a))
+pwit p t@(TypeRep a) = case go a Nil of
+    Left _  -> throwError $ unwords ["cannot deduce", showClass p, classArg]
+    Right a -> return a
+  where
+    st       = show t
+    classArg = if all isAlphaNum st then st else "(" ++ st ++ ")"
+
+    go :: AST t sig -> Args (AST t) sig -> Either String (Dict (p (DenResult sig)))
+    go (Sym s)  as = pwitSym s as
+    go (s :$ a) as = go s (a :* as)
+
+-- | Witness a 'Typeable' constraint for a reified type
+witTypeable :: Witness (Typeable t) t t => TypeRep t a -> Dict (Typeable t a)
+witTypeable = wit Proxy
+
+-- | Partially witness a 'Typeable' constraint for a reified type
+pwitTypeable :: PWitness (Typeable t) t t =>
+    TypeRep t a -> Either String (Dict (Typeable t a))
+pwitTypeable = pwit Proxy
+
+
+
+----------------------------------------------------------------------------------------------------
+-- * Dynamic types
+----------------------------------------------------------------------------------------------------
+
+-- | Safe cast (does not use @unsafeCoerce@)
+cast :: forall t a b . (Typeable t a, Typeable t b, TypeEq t t) =>
+    Proxy t -> a -> Either String b
+cast _ a = do
+    Dict <- typeEqM (typeRep :: TypeRep t a) (typeRep :: TypeRep t b)
+    return a
+
+-- | Safe generalized cast (does not use @unsafeCoerce@)
+gcast :: forall t a b c . (Typeable t a, Typeable t b, TypeEq t t) =>
+    Proxy t -> c a -> Either String (c b)
+gcast _ a = do
+    Dict <- typeEqM (typeRep :: TypeRep t a) (typeRep :: TypeRep t b)
+    return a
+
+-- | Dynamic type parameterized on a type universe
+data Dynamic t
+  where
+    Dyn :: TypeRep t a -> a -> Dynamic t
+
+toDyn :: Typeable t a => a -> Dynamic t
+toDyn = Dyn typeRep
+
+fromDyn :: forall t a . (Typeable t a, TypeEq t t) => Dynamic t -> Either String a
+fromDyn (Dyn t a) = do
+    Dict <- typeEqM t (typeRep :: TypeRep t a)
+    return a
+
+instance (TypeEq t t, Witness Eq t t) => Eq (Dynamic t)
+  where
+    Dyn ta a == Dyn tb b
+        | Just Dict <- typeEq ta tb
+        , Dict      <- wit (Proxy :: Proxy Eq) ta
+        = a == b
+    _ == _ = False
+
+instance Witness Show t t => Show (Dynamic t)
+  where
+    show (Dyn t a) | Dict <- wit (Proxy :: Proxy Show) t = show a
+
+
+
+----------------------------------------------------------------------------------------------------
+-- * Misc.
+----------------------------------------------------------------------------------------------------
+
+-- | The universal class
+class    Any a
+instance Any a
+
+-- | Show the name of type classes
+class ShowClass (p :: * -> Constraint)
+  where
+    -- | Show the name of a type class
+    showClass :: Proxy p -> String
+
+instance ShowClass Any               where showClass _ = "Any"
+instance ShowClass Typeable.Typeable where showClass _ = "Data.Typeable"
+instance ShowClass Eq                where showClass _ = "Eq"
+instance ShowClass Ord               where showClass _ = "Ord"
+instance ShowClass Show              where showClass _ = "Show"
+instance ShowClass Num               where showClass _ = "Num"
+instance ShowClass Integral          where showClass _ = "Integral"
+instance ShowClass (Typeable t)      where showClass _ = "Typeable t"
+
+-- | Proxy of 'Any' class. Can be passed to 'wit' and 'pwit'.
+pAny :: Proxy Any
+pAny = Proxy
+
+-- | Proxy of 'Typeable.Typeable' class (from the base library). Can be passed
+-- to 'wit' and 'pwit'.
+pDataTypeable :: Proxy Typeable.Typeable
+pDataTypeable = Proxy
+
+-- | Proxy of 'Eq' class. Can be passed to 'wit' and 'pwit'.
+pEq :: Proxy Eq
+pEq = Proxy
+
+-- | Proxy of 'Ord' class. Can be passed to 'wit' and 'pwit'.
+pOrd :: Proxy Ord
+pOrd = Proxy
+
+-- | Proxy of 'Show' class. Can be passed to 'wit' and 'pwit'.
+pShow :: Proxy Show
+pShow = Proxy
+
+-- | Proxy of 'Num' class. Can be passed to 'wit' and 'pwit'.
+pNum :: Proxy Num
+pNum = Proxy
+
+-- | Proxy of 'Integral' class. Can be passed to 'wit' and 'pwit'.
+pIntegral :: Proxy Integral
+pIntegral = Proxy
+
diff --git a/src/Data/TypeRep/Sub.hs b/src/Data/TypeRep/Sub.hs
--- a/src/Data/TypeRep/Sub.hs
+++ b/src/Data/TypeRep/Sub.hs
@@ -15,13 +15,13 @@
 
 module Data.TypeRep.Sub where
 
--- TODO Merge this module with `Data.TypeRep.Internal` when support for < 7.10 is dropped
+-- TODO Merge this module with `Data.TypeRep.Representation` when support for < 7.10 is dropped
 
 
 
 import Language.Syntactic
 
-import Data.TypeRep.Internal
+import Data.TypeRep.Representation
 
 
 
diff --git a/src/Data/TypeRep/TH.hs b/src/Data/TypeRep/TH.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/TypeRep/TH.hs
@@ -0,0 +1,398 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+module Data.TypeRep.TH
+  ( deriveRender_forType
+  , deriveTypeEq
+  , deriveWitness
+  , derivePWitness
+  , deriveWitnessAny
+  , derivePWitnessAny
+  , deriveWitnessTypeable
+  , derivePWitnessTypeable
+  ) where
+
+
+
+import Data.Proxy
+import Language.Haskell.TH
+
+import Control.Monad.Except
+import Data.Constraint (Dict (..))
+
+import Language.Syntactic
+import Language.Syntactic.TH
+
+import Data.TypeRep.Representation
+
+
+
+-- | Match on a 'Pred' of the form @(t1 ~ t2)@
+viewEqPred :: Pred -> Maybe (Type,Type)
+#if MIN_VERSION_template_haskell(2,10,0)
+viewEqPred (AppT (AppT EqualityT t1) t2) = Just (t1,t2)
+#else
+viewEqPred (EqualP t1 t2) = Just (t1,t2)
+#endif
+viewEqPred _ = Nothing
+  -- This function is just here to provide compatibility with
+  -- template-haskell < 2.10
+
+-- | Construct a 'Pred' of the form @(Cl t1 t2 ...)@
+mkClassPred :: Name -> [Type] -> Pred
+#if MIN_VERSION_template_haskell(2,10,0)
+mkClassPred cl ts = foldl1 AppT (ConT cl : ts)
+#else
+mkClassPred cl ts = ClassP cl ts
+#endif
+  -- This function is just here to provide compatibility with
+  -- template-haskell < 2.10
+
+tyVarName :: TyVarBndr -> Name
+tyVarName (PlainTV v)    = v  -- Only needed on GHC < 7.10
+tyVarName (KindedTV v _) = v
+
+
+
+indent :: Int -> String -> String
+indent n = unlines . map (replicate n ' ' ++) . lines
+
+-- | Throw an error stating that the given type wasn't declared on the form
+--
+-- > data SymType sig where
+-- >   ...
+-- >   ThisSym :: SymType (a :-> ... :-> Full x)
+-- >   ...
+errorDerive
+    :: String  -- ^ Function where error occurred
+    -> Info    -- ^ Info about type
+    -> a
+errorDerive fun info = error $ unlines
+    [ "------ " ++ fun ++ ": can only handle types declared on the form ----"
+    , ""
+    , "        data SymType sig where"
+    , "          ..."
+    , "          ThisSym :: SymType (a :-> ... :-> Full x)"
+    , "          ..."
+    , ""
+    , "      ------ This is what I got: ------"
+    , ""
+    , indent 8 $ pprint info
+    ]
+
+-- | Get the arity of a symbol. If the type is not declared according to what
+-- is stated for 'errorDerive', 'Nothing' is returned.
+symArity
+    :: Name  -- ^ Type parameter
+    -> Con   -- ^ Symbol
+    -> Maybe Int
+symArity sigVar (ForallC _ [cxt] (NormalC _ []))
+    | Just (VarT sigVar', sig) <- viewEqPred cxt
+    , sigVar == sigVar'
+    = count sig
+  where
+    count :: Type -> Maybe Int
+    count (AppT (AppT arrow _) res)
+        | arrow == ConT ''(:->) = fmap (+1) $ count res
+    count (AppT (ConT full) _)
+        | full == ''Full        = Just 0
+    count _ = Nothing
+symArity _ _ = Nothing
+
+-- | Construct a pattern @v `:*` pat@
+argConsP :: Name -> Pat -> Pat
+argConsP v rest = InfixP (VarP v) '(:*) rest
+
+-- | Construct a predicate proxy @`Proxy` :: `Proxy` Pred@
+mkPredProxy :: Type -> Exp
+mkPredProxy pred = SigE (ConE 'Proxy) (AppT (ConT ''Proxy) pred)
+
+-- Generate an expression of the form
+--
+-- > case wit (Proxy :: Proxy Pred) (TypeRep v) of Dict -> result
+--
+-- The class is given as a 'Type' because
+support
+    :: Type  -- ^ Type predicate (e.g. 'Eq' or @(`Typeable` t)@)
+    -> Name  -- ^ Variable for type representation
+    -> Exp   -- ^ Result
+    -> Exp
+support pred v res = CaseE
+    (foldl1 AppE [VarE 'wit, mkPredProxy pred, AppE (ConE 'TypeRep) (VarE v)])
+    [Match (ConP 'Dict []) (NormalB res) []]
+
+-- | A type variable named @t@
+tVar :: Type
+tVar = VarT $ mkName "t"
+
+-- | "abc_dfg" -> "abc"
+typeName :: String -> String
+typeName = takeWhile (/='_')
+
+
+
+--------------------------------------------------------------------------------
+-- * Derivers
+--------------------------------------------------------------------------------
+
+-- | A version of 'deriveRender' that applies 'typeName' to each constructor
+-- name. That is, e.g. the constructor @Int_t :: IntType (Full Int)@ will be
+-- rendered as \"Int\".
+deriveRender_forType
+    :: Name  -- ^ Type name
+    -> DecsQ
+deriveRender_forType = deriveRender typeName
+
+-- | Derive 'TypeEq' instance for a type representation
+deriveTypeEq
+    :: Name  -- ^ Type name
+    -> DecsQ
+deriveTypeEq ty = do
+    info <- reify ty
+    case info of
+        TyConI (DataD _ _ [sigVarTV] cs _) -> do
+            throwErrExp <- [| throwError "" |]
+              -- `typeEq` will turn this into a proper error message
+            let sigVar = tyVarName sigVarTV
+            let maxArity = case mapM (symArity sigVar) cs of
+                  Just as -> maximum (0:as)
+                  Nothing -> errorDerive "deriveTypeEq" info
+            let classCxt = if maxArity == 0
+                  then []
+                  else [mkClassPred ''TypeEq [tVar, tVar]]
+            let typeEqSymFallThrough = if length cs > 1
+                  then [Clause [WildP, WildP] (NormalB throwErrExp) []]
+                  else []
+            let mkClause c i n a = case typeEqSymClause sigVar c i n a of
+                  Just clause -> clause
+                  Nothing -> errorDerive "deriveTypeEq" info
+            deriveClass classCxt ty
+                (foldl1 AppT [ConT ''TypeEq, ConT ty, tVar])
+                [MatchingMethod 'typeEqSym mkClause typeEqSymFallThrough]
+        _ -> errorDerive "deriveTypeEq" info
+  where
+    typeEqSymClause sigVar con _ name 0 = do
+        arity <- symArity sigVar con
+        let vs1    = take arity varSupply
+            vs2    = take arity $ drop arity varSupply
+            argsP1 = foldr argConsP (ConP 'Nil []) vs1
+            argsP2 = foldr argConsP (ConP 'Nil []) vs2
+            checkArgs v1 v2 = foldl1 AppE
+                  [ VarE 'typeEqM
+                  , AppE (ConE 'TypeRep) (VarE v1), AppE (ConE 'TypeRep) (VarE v2)
+                  ]
+              -- typeEq (TypeRep v1) (TypeRep v2)
+            eqArgs  = [BindS (ConP 'Dict []) $ checkArgs v1 v2 | (v1,v2) <- zip vs1 vs2]
+            retStmt = NoBindS $ AppE (VarE 'return) (ConE 'Dict)
+        return $ Clause
+          [ TupP [ConP name [], argsP1]
+          , TupP [ConP name [], argsP2]
+          ]
+          (NormalB $ DoE (eqArgs ++ [retStmt]))
+          []
+    typeEqSymClause _ _ _ _ _ = Nothing
+
+-- | Derive 'Witness' instance for a type representation
+--
+-- > instance Witness Cl t t => Witness Cl Ty t where
+-- >   witSym Con1 Nil = Dict
+-- >   witSym Con2 (a :* b :* Nil) =
+-- >       case wit (Proxy :: Proxy Cl) (TypeRep a) of
+-- >         Dict -> case wit (Proxy :: Proxy Cl) (TypeRep b) of
+-- >           Dict -> Dict
+deriveWitness
+    :: Name  -- ^ Class name
+    -> Name  -- ^ Type name
+    -> DecsQ
+deriveWitness cl ty = do
+    info <- reify ty
+    case info of
+        TyConI (DataD _ _ [sigVarTV] cs _) -> do
+            let sigVar = tyVarName sigVarTV
+            let maxArity = case mapM (symArity sigVar) cs of
+                  Just as -> maximum (0:as)
+                  Nothing -> errorDerive "deriveWitness" info
+            let classCxt = if maxArity == 0
+                  then []
+                  else [mkClassPred ''Witness [ConT cl, tVar, tVar]]
+            let mkClause c i n a = case witSymClause sigVar c i n a of
+                  Just clause -> clause
+                  Nothing -> errorDerive "deriveWitness" info
+            deriveClass classCxt ty
+              (foldl1 AppT [ConT ''Witness, ConT cl, ConT ty, tVar])
+              [MatchingMethod 'witSym mkClause []]
+  where
+    pred = ConT cl
+    witSymClause sigVar con _ name 0 = do
+        arity <- symArity sigVar con
+        let vs    = take arity varSupply
+            argsP = foldr argConsP (ConP 'Nil []) vs
+        return $ Clause
+          [ConP name [], argsP]
+          (NormalB $ foldr (support pred) (ConE 'Dict) vs)
+          []
+
+-- | Derive 'PWitness' instance for a type representation
+--
+-- > instance PWitness Cl t t => PWitness Cl Ty t where
+-- >   pwitSym Con1 Nil = return Dict
+-- >   pwitSym Con2 (a :* b :* Nil) = do
+-- >       Dict <- pwit (Proxy :: Proxy Cl) (TypeRep a)
+-- >       Dict <- pwit (Proxy :: Proxy Cl) (TypeRep b)
+-- >       return Dict
+derivePWitness
+    :: Name  -- ^ Class name
+    -> Name  -- ^ Type name
+    -> DecsQ
+derivePWitness cl ty = do
+    info <- reify ty
+    case info of
+        TyConI (DataD _ _ [sigVarTV] cs _) -> do
+            let sigVar = tyVarName sigVarTV
+            let maxArity = case mapM (symArity sigVar) cs of
+                  Just as -> maximum (0:as)
+                  Nothing -> errorDerive "derivePWitness" info
+            let classCxt = if maxArity == 0
+                  then []
+                  else [mkClassPred ''PWitness [ConT cl, tVar, tVar]]
+            let mkClause c i n a = case pwitSymClause sigVar c i n a of
+                  Just clause -> clause
+                  Nothing -> errorDerive "derivePWitness" info
+            deriveClass classCxt ty
+              (foldl1 AppT [ConT ''PWitness, ConT cl, ConT ty, tVar])
+              [MatchingMethod 'pwitSym mkClause []]
+  where
+    pred = ConT cl
+    pwitSymClause sigVar con _ name 0 = do
+        arity <- symArity sigVar con
+        let vs        = take arity varSupply
+            argsP     = foldr argConsP (ConP 'Nil []) vs
+            pwitArg v = foldl1 AppE [VarE 'pwit, mkPredProxy pred, AppE (ConE 'TypeRep) (VarE v)]
+            pwitArgs  = [BindS (ConP 'Dict []) $ pwitArg v | v <- vs]
+            retStmt   = NoBindS $ AppE (VarE 'return) (ConE 'Dict)
+        return $ Clause
+          [ConP name [], argsP]
+          (NormalB $ DoE (pwitArgs ++ [retStmt]))
+          []
+
+-- | Derive @`Witness` `Any`@ instance for a type representation
+--
+-- > instance Witness Any Ty t where
+-- >   witSym _ _ = Dict
+-- >   witSym _ _ = Dict
+deriveWitnessAny
+    :: Name  -- ^ Type name
+    -> DecsQ
+deriveWitnessAny ty = do
+    deriveClass [] ty
+      (foldl1 AppT [ConT ''Witness, ConT ''Any, ConT ty, tVar])
+      [MatchingMethod 'witSym witSymClause []]
+  where
+    witSymClause _ _ con 0 = Clause
+        [WildP, WildP]
+        (NormalB $ ConE 'Dict)
+        []
+
+-- | Derive @`PWitness` `Any`@ instance for a type representation
+--
+-- > instance PWitness Any Ty t where
+-- >   pwitSym _ _ = return Dict
+-- >   pwitSym _ _ = return Dict
+derivePWitnessAny
+    :: Name  -- ^ Type name
+    -> DecsQ
+derivePWitnessAny ty = do
+    deriveClass [] ty
+      (foldl1 AppT [ConT ''PWitness, ConT ''Any, ConT ty, tVar])
+      [MatchingMethod 'pwitSym witSymClause []]
+  where
+    witSymClause _ _ con 0 = Clause
+        [WildP, WildP]
+        (NormalB $ AppE (VarE 'return) (ConE 'Dict))
+        []
+
+-- | Derive @`Witness` (`Typeable` Ty)@ instance for a type representation
+--
+-- > instance (Ty :<: t) => Witness (Typeable t) Ty t where
+-- >   witSym Con1 Nil = Dict
+-- >   witSym Con2 (a :* b :* Nil) =
+-- >       case wit (Proxy :: Proxy (Typeable t)) (TypeRep a) of
+-- >         Dict -> case wit (Proxy :: Proxy (Typeable t)) (TypeRep b) of
+-- >           Dict -> Dict
+deriveWitnessTypeable
+    :: Name  -- ^ Type name
+    -> DecsQ
+deriveWitnessTypeable ty = do
+    info <- reify ty
+    case info of
+        TyConI (DataD _ _ [sigVarTV] cs _) -> do
+            let sigVar = tyVarName sigVarTV
+            let maxArity = case mapM (symArity sigVar) cs of
+                  Just as -> maximum (0:as)
+                  Nothing -> errorDerive "deriveWitnessTypeable" info
+            let sub = mkClassPred ''(:<:) [ConT ty, tVar]
+            let classCxt = if maxArity == 0
+                  then [sub]
+                  else [sub, mkClassPred ''Witness [AppT (ConT cl) tVar, tVar, tVar]]
+            let mkClause c i n a = case witSymClause sigVar c i n a of
+                  Just clause -> clause
+                  Nothing -> errorDerive "deriveWitnessTypeable" info
+            deriveClass classCxt ty
+              (foldl1 AppT [ConT ''Witness, AppT (ConT cl) tVar, ConT ty, tVar])
+              [MatchingMethod 'witSym mkClause []]
+  where
+    cl   = ''Typeable
+    pred = AppT (ConT cl) tVar
+    witSymClause sigVar con _ name 0 = do
+        arity <- symArity sigVar con
+        let vs    = take arity varSupply
+            argsP = foldr argConsP (ConP 'Nil []) vs
+        return $ Clause
+          [ConP name [], argsP]
+          (NormalB $ foldr (support pred) (ConE 'Dict) vs)
+          []
+
+-- | Derive @`PWitness` (`Typeable` Ty)@ instance for a type representation
+--
+-- > instance (Ty :<: t) => PWitness (Typeable t) Ty t where
+-- >   pwitSym Con1 Nil = return Dict
+-- >   pwitSym Con2 (a :* b :* Nil) = do
+-- >       Dict <- pwit (Proxy :: Proxy (Typeable t)) (TypeRep a)
+-- >       Dict <- pwit (Proxy :: Proxy (Typeable t)) (TypeRep b)
+-- >       return Dict
+derivePWitnessTypeable
+    :: Name  -- ^ Type name
+    -> DecsQ
+derivePWitnessTypeable ty = do
+    info <- reify ty
+    case info of
+        TyConI (DataD _ _ [sigVarTV] cs _) -> do
+            let sigVar = tyVarName sigVarTV
+            let maxArity = case mapM (symArity sigVar) cs of
+                  Just as -> maximum (0:as)
+                  Nothing -> errorDerive "derivePWitnessTypeable" info
+            let sub = mkClassPred ''(:<:) [ConT ty, tVar]
+            let classCxt = if maxArity == 0
+                  then [sub]
+                  else [sub, mkClassPred ''PWitness [AppT (ConT cl) tVar, tVar, tVar]]
+            let mkClause c i n a = case pwitSymClause sigVar c i n a of
+                  Just clause -> clause
+                  Nothing -> errorDerive "derivePWitnessTypeable" info
+            deriveClass classCxt ty
+              (foldl1 AppT [ConT ''PWitness, AppT (ConT cl) tVar, ConT ty, tVar])
+              [MatchingMethod 'pwitSym mkClause []]
+  where
+    cl   = ''Typeable
+    pred = AppT (ConT cl) tVar
+    pwitSymClause sigVar con _ name 0 = do
+        arity <- symArity sigVar con
+        let vs        = take arity varSupply
+            argsP     = foldr argConsP (ConP 'Nil []) vs
+            pwitArg v = foldl1 AppE [VarE 'pwit, mkPredProxy pred, AppE (ConE 'TypeRep) (VarE v)]
+            pwitArgs  = [BindS (ConP 'Dict []) $ pwitArg v | v <- vs]
+            retStmt   = NoBindS $ AppE (VarE 'return) (ConE 'Dict)
+        return $ Clause
+          [ConP name [], argsP]
+          (NormalB $ DoE (pwitArgs ++ [retStmt]))
+          []
+
diff --git a/src/Data/TypeRep/Types/Basic.hs b/src/Data/TypeRep/Types/Basic.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/TypeRep/Types/Basic.hs
@@ -0,0 +1,205 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | Representations for specific types
+--
+-- The reason for using symbol names ending with @_t@ is that 'deriveRender'
+-- uses everything that comes before @_@ when rendering the constructor.
+
+module Data.TypeRep.Types.Basic where
+
+
+
+import qualified Data.Typeable as Typeable
+
+import Language.Syntactic
+
+import Data.TypeRep.Representation
+import Data.TypeRep.TH
+
+
+
+data BoolType   a where Bool_t   :: BoolType   (Full Bool)
+data CharType   a where Char_t   :: CharType   (Full Char)
+data IntType    a where Int_t    :: IntType    (Full Int)
+data FloatType  a where Float_t  :: FloatType  (Full Float)
+data DoubleType a where Double_t :: DoubleType (Full Double)
+data ListType   a where List_t   :: ListType (a :-> Full [a])
+data FunType    a where Fun_t    :: FunType  (a :-> b :-> Full (a -> b))
+
+boolType :: (Syntactic a, BoolType :<: Domain a, Internal a ~ Bool) => a
+boolType = sugarSym Bool_t
+
+charType :: (Syntactic a, CharType :<: Domain a, Internal a ~ Char) => a
+charType = sugarSym Char_t
+
+intType :: (Syntactic a, IntType :<: Domain a, Internal a ~ Int) => a
+intType = sugarSym Int_t
+
+floatType :: (Syntactic a, FloatType :<: Domain a, Internal a ~ Float) => a
+floatType = sugarSym Float_t
+
+doubleType :: (Syntactic a, DoubleType :<: Domain a, Internal a ~ Double) => a
+doubleType = sugarSym Double_t
+
+listType
+    :: ( Syntactic list
+       , Syntactic elem
+       , Domain list ~ Domain elem
+       , ListType :<: Domain list
+       , Internal list ~ [Internal elem]
+       , elem ~ c e
+       , list ~ c l
+           -- These last equalities are used to help type inference by forcing the representations
+           -- to use the same type constructor (e.g. 'TR' or 'TypeRep')
+       )
+    => elem -> list
+listType = sugarSym List_t
+
+funType
+    :: ( Syntactic fun
+       , Syntactic a
+       , Syntactic b
+       , Domain fun ~ Domain a
+       , Domain fun ~ Domain b
+       , FunType :<: Domain fun
+       , Internal fun ~ (Internal a -> Internal b)
+       , a   ~ c x
+       , b   ~ c y
+       , fun ~ c z
+       )
+    => a -> b -> fun
+funType = sugarSym Fun_t
+
+deriveRender_forType ''BoolType
+deriveRender_forType ''CharType
+deriveRender_forType ''IntType
+deriveRender_forType ''FloatType
+deriveRender_forType ''DoubleType
+
+instance Render ListType
+  where
+    renderSym List_t = "[]"
+    renderArgs [a] List_t = "[" ++ a ++ "]"
+
+instance Render FunType
+  where
+    renderSym Fun_t = "(->)"
+    renderArgs = renderArgsSmart
+
+deriveTypeEq ''BoolType
+deriveTypeEq ''CharType
+deriveTypeEq ''IntType
+deriveTypeEq ''FloatType
+deriveTypeEq ''DoubleType
+deriveTypeEq ''ListType
+deriveTypeEq ''FunType
+
+deriveWitnessAny ''BoolType
+deriveWitnessAny ''CharType
+deriveWitnessAny ''IntType
+deriveWitnessAny ''FloatType
+deriveWitnessAny ''DoubleType
+deriveWitnessAny ''ListType
+deriveWitnessAny ''FunType
+
+derivePWitnessAny ''BoolType
+derivePWitnessAny ''CharType
+derivePWitnessAny ''IntType
+derivePWitnessAny ''FloatType
+derivePWitnessAny ''DoubleType
+derivePWitnessAny ''ListType
+derivePWitnessAny ''FunType
+
+deriveWitness ''Typeable.Typeable ''BoolType
+deriveWitness ''Typeable.Typeable ''CharType
+deriveWitness ''Typeable.Typeable ''IntType
+deriveWitness ''Typeable.Typeable ''FloatType
+deriveWitness ''Typeable.Typeable ''DoubleType
+deriveWitness ''Typeable.Typeable ''ListType
+deriveWitness ''Typeable.Typeable ''FunType
+
+derivePWitness ''Typeable.Typeable ''BoolType
+derivePWitness ''Typeable.Typeable ''CharType
+derivePWitness ''Typeable.Typeable ''IntType
+derivePWitness ''Typeable.Typeable ''FloatType
+derivePWitness ''Typeable.Typeable ''DoubleType
+derivePWitness ''Typeable.Typeable ''ListType
+derivePWitness ''Typeable.Typeable ''FunType
+
+deriveWitness ''Eq ''BoolType
+deriveWitness ''Eq ''CharType
+deriveWitness ''Eq ''IntType
+deriveWitness ''Eq ''FloatType
+deriveWitness ''Eq ''DoubleType
+deriveWitness ''Eq ''ListType
+
+derivePWitness ''Eq ''BoolType
+derivePWitness ''Eq ''CharType
+derivePWitness ''Eq ''IntType
+derivePWitness ''Eq ''FloatType
+derivePWitness ''Eq ''DoubleType
+derivePWitness ''Eq ''ListType
+
+deriveWitness ''Ord ''BoolType
+deriveWitness ''Ord ''CharType
+deriveWitness ''Ord ''IntType
+deriveWitness ''Ord ''FloatType
+deriveWitness ''Ord ''DoubleType
+deriveWitness ''Ord ''ListType
+
+derivePWitness ''Ord ''BoolType
+derivePWitness ''Ord ''CharType
+derivePWitness ''Ord ''IntType
+derivePWitness ''Ord ''FloatType
+derivePWitness ''Ord ''DoubleType
+derivePWitness ''Ord ''ListType
+
+deriveWitness ''Show ''BoolType
+deriveWitness ''Show ''CharType
+deriveWitness ''Show ''IntType
+deriveWitness ''Show ''FloatType
+deriveWitness ''Show ''DoubleType
+deriveWitness ''Show ''ListType
+
+derivePWitness ''Show ''BoolType
+derivePWitness ''Show ''CharType
+derivePWitness ''Show ''IntType
+derivePWitness ''Show ''FloatType
+derivePWitness ''Show ''DoubleType
+derivePWitness ''Show ''ListType
+
+deriveWitness ''Num ''IntType
+deriveWitness ''Num ''FloatType
+deriveWitness ''Num ''DoubleType
+
+derivePWitness ''Num ''IntType
+derivePWitness ''Num ''FloatType
+derivePWitness ''Num ''DoubleType
+
+deriveWitness ''Integral ''IntType
+
+derivePWitness ''Integral ''IntType
+
+
+
+-- 'PWitness' instances for non-members
+
+instance PWitness Eq FunType t
+
+instance PWitness Ord FunType t
+
+instance PWitness Show FunType t
+
+instance PWitness Num BoolType   t
+instance PWitness Num CharType   t
+instance PWitness Num ListType   t
+instance PWitness Num FunType    t
+
+instance PWitness Integral BoolType   t
+instance PWitness Integral CharType   t
+instance PWitness Integral FloatType  t
+instance PWitness Integral DoubleType t
+instance PWitness Integral ListType   t
+instance PWitness Integral FunType    t
+
diff --git a/src/Data/TypeRep/Types/Basic/Typeable.hs b/src/Data/TypeRep/Types/Basic/Typeable.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/TypeRep/Types/Basic/Typeable.hs
@@ -0,0 +1,52 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | 'Typeable' instances for various types. The reason for having these in a
+-- separate module is that it might be desired to have these instances with
+-- other type representations.
+--
+-- For example, instead of the instance
+--
+-- > (BoolType :<: t) => Typeable t Bool
+--
+-- one might want to have
+--
+-- > Typeable MyTypeRep Bool
+
+module Data.TypeRep.Types.Basic.Typeable where
+
+
+
+import Language.Syntactic
+
+import Data.TypeRep.Representation
+import Data.TypeRep.TH
+import Data.TypeRep.Types.Basic
+
+
+
+instance (BoolType   :<: t) => Typeable t Bool   where typeRep' = boolType
+instance (CharType   :<: t) => Typeable t Char   where typeRep' = charType
+instance (IntType    :<: t) => Typeable t Int    where typeRep' = intType
+instance (FloatType  :<: t) => Typeable t Float  where typeRep' = floatType
+instance (DoubleType :<: t) => Typeable t Double where typeRep' = doubleType
+
+instance (ListType :<: t, Typeable t a)               => Typeable t [a]      where typeRep' = listType typeRep'
+instance (FunType  :<: t, Typeable t a, Typeable t b) => Typeable t (a -> b) where typeRep' = funType typeRep' typeRep'
+
+deriveWitnessTypeable ''BoolType
+deriveWitnessTypeable ''CharType
+deriveWitnessTypeable ''IntType
+deriveWitnessTypeable ''FloatType
+deriveWitnessTypeable ''DoubleType
+deriveWitnessTypeable ''ListType
+deriveWitnessTypeable ''FunType
+
+derivePWitnessTypeable ''BoolType
+derivePWitnessTypeable ''CharType
+derivePWitnessTypeable ''IntType
+derivePWitnessTypeable ''FloatType
+derivePWitnessTypeable ''DoubleType
+derivePWitnessTypeable ''ListType
+derivePWitnessTypeable ''FunType
+
diff --git a/src/Data/TypeRep/Types/IntWord.hs b/src/Data/TypeRep/Types/IntWord.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/TypeRep/Types/IntWord.hs
@@ -0,0 +1,76 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | Representations for signed and unsigned integer types
+--
+-- The reason for using symbol names ending with @_t@ is that 'deriveRender'
+-- uses everything that comes before @_@ when rendering the constructor.
+
+module Data.TypeRep.Types.IntWord where
+
+
+
+import Data.Int
+import qualified Data.Typeable as Typeable
+import Data.Word
+
+import Language.Syntactic
+
+import Data.TypeRep.TH
+
+
+
+data IntWordType a
+  where
+    Int8_t   :: IntWordType (Full Int8)
+    Int16_t  :: IntWordType (Full Int16)
+    Int32_t  :: IntWordType (Full Int32)
+    Int64_t  :: IntWordType (Full Int64)
+    Word8_t  :: IntWordType (Full Word8)
+    Word16_t :: IntWordType (Full Word16)
+    Word32_t :: IntWordType (Full Word32)
+    Word64_t :: IntWordType (Full Word64)
+
+int8Type :: (Syntactic a, IntWordType :<: Domain a, Internal a ~ Int8) => a
+int8Type = sugarSym Int8_t
+
+int16Type :: (Syntactic a, IntWordType :<: Domain a, Internal a ~ Int16) => a
+int16Type = sugarSym Int16_t
+
+int32Type :: (Syntactic a, IntWordType :<: Domain a, Internal a ~ Int32) => a
+int32Type = sugarSym Int32_t
+
+int64Type :: (Syntactic a, IntWordType :<: Domain a, Internal a ~ Int64) => a
+int64Type = sugarSym Int64_t
+
+word8Type :: (Syntactic a, IntWordType :<: Domain a, Internal a ~ Word8) => a
+word8Type = sugarSym Word8_t
+
+word16Type :: (Syntactic a, IntWordType :<: Domain a, Internal a ~ Word16) => a
+word16Type = sugarSym Word16_t
+
+word32Type :: (Syntactic a, IntWordType :<: Domain a, Internal a ~ Word32) => a
+word32Type = sugarSym Word32_t
+
+word64Type :: (Syntactic a, IntWordType :<: Domain a, Internal a ~ Word64) => a
+word64Type = sugarSym Word64_t
+
+deriveRender_forType ''IntWordType
+deriveTypeEq         ''IntWordType
+deriveWitnessAny     ''IntWordType
+derivePWitnessAny    ''IntWordType
+
+deriveWitness ''Typeable.Typeable ''IntWordType
+deriveWitness ''Eq       ''IntWordType
+deriveWitness ''Ord      ''IntWordType
+deriveWitness ''Show     ''IntWordType
+deriveWitness ''Num      ''IntWordType
+deriveWitness ''Integral ''IntWordType
+
+derivePWitness ''Typeable.Typeable ''IntWordType
+derivePWitness ''Eq       ''IntWordType
+derivePWitness ''Ord      ''IntWordType
+derivePWitness ''Show     ''IntWordType
+derivePWitness ''Num      ''IntWordType
+derivePWitness ''Integral ''IntWordType
+
diff --git a/src/Data/TypeRep/Types/IntWord/Typeable.hs b/src/Data/TypeRep/Types/IntWord/Typeable.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/TypeRep/Types/IntWord/Typeable.hs
@@ -0,0 +1,42 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | 'Typeable' instances for signed and unsigned integer types. The reason for
+-- having these in a separate module is that it might be desired to have these
+-- instances with other type representations.
+--
+-- For example, instead of the instance
+--
+-- > (IntWordType :<: t) => Typeable t Int8
+--
+-- one might want to have
+--
+-- > Typeable MyTypeRep Int8
+
+module Data.TypeRep.Types.IntWord.Typeable where
+
+
+
+import Data.Int
+import Data.Word
+
+import Language.Syntactic
+
+import Data.TypeRep.Representation
+import Data.TypeRep.TH
+import Data.TypeRep.Types.IntWord
+
+
+
+instance (IntWordType :<: t) => Typeable t Int8   where typeRep' = int8Type
+instance (IntWordType :<: t) => Typeable t Int16  where typeRep' = int16Type
+instance (IntWordType :<: t) => Typeable t Int32  where typeRep' = int32Type
+instance (IntWordType :<: t) => Typeable t Int64  where typeRep' = int64Type
+instance (IntWordType :<: t) => Typeable t Word8  where typeRep' = word8Type
+instance (IntWordType :<: t) => Typeable t Word16 where typeRep' = word16Type
+instance (IntWordType :<: t) => Typeable t Word32 where typeRep' = word32Type
+instance (IntWordType :<: t) => Typeable t Word64 where typeRep' = word64Type
+
+deriveWitnessTypeable  ''IntWordType
+derivePWitnessTypeable ''IntWordType
+
diff --git a/src/Data/TypeRep/Types/Tuple.hs b/src/Data/TypeRep/Types/Tuple.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/TypeRep/Types/Tuple.hs
@@ -0,0 +1,163 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | Representations for tuple types
+--
+-- The reason for using symbol names ending with @_t@ is that 'deriveRender'
+-- uses everything that comes before @_@ when rendering the constructor.
+
+module Data.TypeRep.Types.Tuple where
+
+
+
+import Data.List (intercalate)
+import qualified Data.Typeable as Typeable
+
+import Data.Orphans ()
+
+import Language.Syntactic
+
+import Data.TypeRep.Representation
+import Data.TypeRep.TH
+
+
+
+data TupleType a
+  where
+    Tup2_t  :: TupleType (a :-> b :-> Full (a,b))
+    Tup3_t  :: TupleType (a :-> b :-> c :-> Full (a,b,c))
+    Tup4_t  :: TupleType (a :-> b :-> c :-> d :-> Full (a,b,c,d))
+    Tup5_t  :: TupleType (a :-> b :-> c :-> d :-> e :-> Full (a,b,c,d,e))
+    Tup6_t  :: TupleType (a :-> b :-> c :-> d :-> e :-> f :-> Full (a,b,c,d,e,f))
+    Tup7_t  :: TupleType (a :-> b :-> c :-> d :-> e :-> f :-> g :-> Full (a,b,c,d,e,f,g))
+    Tup8_t  :: TupleType (a :-> b :-> c :-> d :-> e :-> f :-> g :-> h :-> Full (a,b,c,d,e,f,g,h))
+    Tup9_t  :: TupleType (a :-> b :-> c :-> d :-> e :-> f :-> g :-> h :-> i :-> Full (a,b,c,d,e,f,g,h,i))
+    Tup10_t :: TupleType (a :-> b :-> c :-> d :-> e :-> f :-> g :-> h :-> i :-> j :-> Full (a,b,c,d,e,f,g,h,i,j))
+    Tup11_t :: TupleType (a :-> b :-> c :-> d :-> e :-> f :-> g :-> h :-> i :-> j :-> k :-> Full (a,b,c,d,e,f,g,h,i,j,k))
+    Tup12_t :: TupleType (a :-> b :-> c :-> d :-> e :-> f :-> g :-> h :-> i :-> j :-> k :-> l :-> Full (a,b,c,d,e,f,g,h,i,j,k,l))
+    Tup13_t :: TupleType (a :-> b :-> c :-> d :-> e :-> f :-> g :-> h :-> i :-> j :-> k :-> l :-> m :-> Full (a,b,c,d,e,f,g,h,i,j,k,l,m))
+    Tup14_t :: TupleType (a :-> b :-> c :-> d :-> e :-> f :-> g :-> h :-> i :-> j :-> k :-> l :-> m :-> n :-> Full (a,b,c,d,e,f,g,h,i,j,k,l,m,n))
+    Tup15_t :: TupleType (a :-> b :-> c :-> d :-> e :-> f :-> g :-> h :-> i :-> j :-> k :-> l :-> m :-> n :-> o :-> Full (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o))
+
+
+
+-- The smart constructors are not overloaded using `Syntactic` as this would
+-- lead to gigantic type signatures.
+
+tup2Type :: (TupleType :<: t)
+    => TypeRep t a -> TypeRep t b -> TypeRep t (a,b)
+tup2Type = sugarSym Tup2_t
+
+tup3Type :: (TupleType :<: t)
+    => TypeRep t a -> TypeRep t b -> TypeRep t c -> TypeRep t (a,b,c)
+tup3Type = sugarSym Tup3_t
+
+tup4Type :: (TupleType :<: t)
+    => TypeRep t a -> TypeRep t b -> TypeRep t c -> TypeRep t d -> TypeRep t (a,b,c,d)
+tup4Type = sugarSym Tup4_t
+
+tup5Type :: (TupleType :<: t)
+    => TypeRep t a -> TypeRep t b -> TypeRep t c -> TypeRep t d -> TypeRep t e
+    -> TypeRep t (a,b,c,d,e)
+tup5Type = sugarSym Tup5_t
+
+tup6Type :: (TupleType :<: t)
+    => TypeRep t a -> TypeRep t b -> TypeRep t c -> TypeRep t d -> TypeRep t e
+    -> TypeRep t f-> TypeRep t (a,b,c,d,e,f)
+tup6Type = sugarSym Tup6_t
+
+tup7Type :: (TupleType :<: t)
+    => TypeRep t a -> TypeRep t b -> TypeRep t c -> TypeRep t d -> TypeRep t e
+    -> TypeRep t f -> TypeRep t g -> TypeRep t (a,b,c,d,e,f,g)
+tup7Type = sugarSym Tup7_t
+
+tup8Type :: (TupleType :<: t)
+    => TypeRep t a -> TypeRep t b -> TypeRep t c -> TypeRep t d -> TypeRep t e
+    -> TypeRep t f -> TypeRep t g -> TypeRep t h -> TypeRep t (a,b,c,d,e,f,g,h)
+tup8Type = sugarSym Tup8_t
+
+tup9Type :: (TupleType :<: t)
+    => TypeRep t a -> TypeRep t b -> TypeRep t c -> TypeRep t d -> TypeRep t e
+    -> TypeRep t f -> TypeRep t g -> TypeRep t h -> TypeRep t i -> TypeRep t (a,b,c,d,e,f,g,h,i)
+tup9Type = sugarSym Tup9_t
+
+tup10Type :: (TupleType :<: t)
+    => TypeRep t a -> TypeRep t b -> TypeRep t c -> TypeRep t d -> TypeRep t e
+    -> TypeRep t f -> TypeRep t g -> TypeRep t h -> TypeRep t i -> TypeRep t j
+    -> TypeRep t (a,b,c,d,e,f,g,h,i,j)
+tup10Type = sugarSym Tup10_t
+
+tup11Type :: (TupleType :<: t)
+    => TypeRep t a -> TypeRep t b -> TypeRep t c -> TypeRep t d -> TypeRep t e
+    -> TypeRep t f -> TypeRep t g -> TypeRep t h -> TypeRep t i -> TypeRep t j
+    -> TypeRep t k -> TypeRep t (a,b,c,d,e,f,g,h,i,j,k)
+tup11Type = sugarSym Tup11_t
+
+tup12Type :: (TupleType :<: t)
+    => TypeRep t a -> TypeRep t b -> TypeRep t c -> TypeRep t d -> TypeRep t e
+    -> TypeRep t f -> TypeRep t g -> TypeRep t h -> TypeRep t i -> TypeRep t j
+    -> TypeRep t k -> TypeRep t l -> TypeRep t (a,b,c,d,e,f,g,h,i,j,k,l)
+tup12Type = sugarSym Tup12_t
+
+tup13Type :: (TupleType :<: t)
+    => TypeRep t a -> TypeRep t b -> TypeRep t c -> TypeRep t d -> TypeRep t e
+    -> TypeRep t f -> TypeRep t g -> TypeRep t h -> TypeRep t i -> TypeRep t j
+    -> TypeRep t k -> TypeRep t l -> TypeRep t m -> TypeRep t (a,b,c,d,e,f,g,h,i,j,k,l,m)
+tup13Type = sugarSym Tup13_t
+
+tup14Type :: (TupleType :<: t)
+    => TypeRep t a -> TypeRep t b -> TypeRep t c -> TypeRep t d -> TypeRep t e
+    -> TypeRep t f -> TypeRep t g -> TypeRep t h -> TypeRep t i -> TypeRep t j
+    -> TypeRep t k -> TypeRep t l -> TypeRep t m -> TypeRep t n
+    -> TypeRep t (a,b,c,d,e,f,g,h,i,j,k,l,m,n)
+tup14Type = sugarSym Tup14_t
+
+tup15Type :: (TupleType :<: t)
+    => TypeRep t a -> TypeRep t b -> TypeRep t c -> TypeRep t d -> TypeRep t e
+    -> TypeRep t f -> TypeRep t g -> TypeRep t h -> TypeRep t i -> TypeRep t j
+    -> TypeRep t k -> TypeRep t l -> TypeRep t m -> TypeRep t n
+    -> TypeRep t o -> TypeRep t (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o)
+tup15Type = sugarSym Tup15_t
+
+tupWidth :: TupleType a -> Int
+tupWidth Tup2_t  = 2
+tupWidth Tup3_t  = 3
+tupWidth Tup4_t  = 4
+tupWidth Tup5_t  = 5
+tupWidth Tup6_t  = 6
+tupWidth Tup7_t  = 7
+tupWidth Tup8_t  = 8
+tupWidth Tup9_t  = 9
+tupWidth Tup10_t = 10
+tupWidth Tup11_t = 11
+tupWidth Tup12_t = 12
+tupWidth Tup13_t = 13
+tupWidth Tup14_t = 14
+tupWidth Tup15_t = 15
+
+instance Render TupleType
+  where
+    renderSym tup   = "(" ++ replicate (tupWidth tup - 1) ',' ++ ")"
+    renderArgs as _ = "(" ++ intercalate "," as ++ ")"
+
+deriveTypeEq ''TupleType
+
+deriveWitnessAny ''TupleType
+
+deriveWitness ''Typeable.Typeable ''TupleType
+
+deriveWitness ''Eq   ''TupleType
+deriveWitness ''Ord  ''TupleType
+deriveWitness ''Show ''TupleType
+
+derivePWitnessAny ''TupleType
+
+derivePWitness ''Typeable.Typeable ''TupleType
+
+derivePWitness ''Eq   ''TupleType
+derivePWitness ''Ord  ''TupleType
+derivePWitness ''Show ''TupleType
+
+instance PWitness Num TupleType t
+instance PWitness Integral TupleType t
+
diff --git a/src/Data/TypeRep/Types/Tuple/Typeable.hs b/src/Data/TypeRep/Types/Tuple/Typeable.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/TypeRep/Types/Tuple/Typeable.hs
@@ -0,0 +1,86 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | 'Typeable' instances for tuple types. The reason for having these in a
+-- separate module is that it might be desired to have these instances with
+-- other type representations.
+--
+-- For example, instead of the instance
+--
+-- > (BoolType :<: t) => Typeable t Bool
+--
+-- one might want to have
+--
+-- > Typeable MyTypeRep Bool
+
+module Data.TypeRep.Types.Tuple.Typeable where
+
+
+
+import Language.Syntactic
+
+import Data.TypeRep.Representation
+import Data.TypeRep.TH
+import Data.TypeRep.Types.Tuple
+
+
+
+instance (TupleType :<: t, Typeable t a, Typeable t b) =>
+    Typeable t (a,b)
+  where typeRep' = sugarSym Tup2_t typeRep' typeRep'
+
+instance (TupleType :<: t, Typeable t a, Typeable t b, Typeable t c) =>
+    Typeable t (a,b,c)
+  where typeRep' = sugarSym Tup3_t typeRep' typeRep' typeRep'
+
+instance (TupleType :<: t, Typeable t a, Typeable t b, Typeable t c, Typeable t d) =>
+    Typeable t (a,b,c,d)
+  where typeRep' = sugarSym Tup4_t typeRep' typeRep' typeRep' typeRep'
+
+instance (TupleType :<: t, Typeable t a, Typeable t b, Typeable t c, Typeable t d, Typeable t e) =>
+    Typeable t (a,b,c,d,e)
+  where typeRep' = sugarSym Tup5_t typeRep' typeRep' typeRep' typeRep' typeRep'
+
+instance (TupleType :<: t, Typeable t a, Typeable t b, Typeable t c, Typeable t d, Typeable t e, Typeable t f) =>
+    Typeable t (a,b,c,d,e,f)
+  where typeRep' = sugarSym Tup6_t typeRep' typeRep' typeRep' typeRep' typeRep' typeRep'
+
+instance (TupleType :<: t, Typeable t a, Typeable t b, Typeable t c, Typeable t d, Typeable t e, Typeable t f, Typeable t g) =>
+    Typeable t (a,b,c,d,e,f,g)
+  where typeRep' = sugarSym Tup7_t typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep'
+
+instance (TupleType :<: t, Typeable t a, Typeable t b, Typeable t c, Typeable t d, Typeable t e, Typeable t f, Typeable t g, Typeable t h) =>
+    Typeable t (a,b,c,d,e,f,g,h)
+  where typeRep' = sugarSym Tup8_t typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep'
+
+instance (TupleType :<: t, Typeable t a, Typeable t b, Typeable t c, Typeable t d, Typeable t e, Typeable t f, Typeable t g, Typeable t h, Typeable t i) =>
+    Typeable t (a,b,c,d,e,f,g,h,i)
+  where typeRep' = sugarSym Tup9_t typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep'
+
+instance (TupleType :<: t, Typeable t a, Typeable t b, Typeable t c, Typeable t d, Typeable t e, Typeable t f, Typeable t g, Typeable t h, Typeable t i, Typeable t j) =>
+    Typeable t (a,b,c,d,e,f,g,h,i,j)
+  where typeRep' = sugarSym Tup10_t typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep'
+
+instance (TupleType :<: t, Typeable t a, Typeable t b, Typeable t c, Typeable t d, Typeable t e, Typeable t f, Typeable t g, Typeable t h, Typeable t i, Typeable t j, Typeable t k) =>
+    Typeable t (a,b,c,d,e,f,g,h,i,j,k)
+  where typeRep' = sugarSym Tup11_t typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep'
+
+instance (TupleType :<: t, Typeable t a, Typeable t b, Typeable t c, Typeable t d, Typeable t e, Typeable t f, Typeable t g, Typeable t h, Typeable t i, Typeable t j, Typeable t k, Typeable t l) =>
+    Typeable t (a,b,c,d,e,f,g,h,i,j,k,l)
+  where typeRep' = sugarSym Tup12_t typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep'
+
+instance (TupleType :<: t, Typeable t a, Typeable t b, Typeable t c, Typeable t d, Typeable t e, Typeable t f, Typeable t g, Typeable t h, Typeable t i, Typeable t j, Typeable t k, Typeable t l, Typeable t m) =>
+    Typeable t (a,b,c,d,e,f,g,h,i,j,k,l,m)
+  where typeRep' = sugarSym Tup13_t typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep'
+
+instance (TupleType :<: t, Typeable t a, Typeable t b, Typeable t c, Typeable t d, Typeable t e, Typeable t f, Typeable t g, Typeable t h, Typeable t i, Typeable t j, Typeable t k, Typeable t l, Typeable t m, Typeable t n) =>
+    Typeable t (a,b,c,d,e,f,g,h,i,j,k,l,m,n)
+  where typeRep' = sugarSym Tup14_t typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep'
+
+instance (TupleType :<: t, Typeable t a, Typeable t b, Typeable t c, Typeable t d, Typeable t e, Typeable t f, Typeable t g, Typeable t h, Typeable t i, Typeable t j, Typeable t k, Typeable t l, Typeable t m, Typeable t n, Typeable t o) =>
+    Typeable t (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o)
+  where typeRep' = sugarSym Tup15_t typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep'
+
+deriveWitnessTypeable ''TupleType
+derivePWitnessTypeable ''TupleType
+
diff --git a/src/Data/TypeRep/VarArg.hs b/src/Data/TypeRep/VarArg.hs
--- a/src/Data/TypeRep/VarArg.hs
+++ b/src/Data/TypeRep/VarArg.hs
@@ -8,7 +8,8 @@
 
 import Language.Syntactic
 import Data.TypeRep
-import Data.TypeRep.Internal
+import Data.TypeRep.Representation
+import Data.TypeRep.Types.Basic
 
 
 
@@ -54,33 +55,33 @@
 
 instance VarArg BoolType
   where
-    aritySym BoolType Nil      = FunRes
-    fromResInvSym BoolType Nil = Dict
+    aritySym Bool_t Nil      = FunRes
+    fromResInvSym Bool_t Nil = Dict
 
 instance VarArg CharType
   where
-    aritySym CharType Nil      = FunRes
-    fromResInvSym CharType Nil = Dict
+    aritySym Char_t Nil      = FunRes
+    fromResInvSym Char_t Nil = Dict
 
 instance VarArg IntType
   where
-    aritySym IntType Nil      = FunRes
-    fromResInvSym IntType Nil = Dict
+    aritySym Int_t Nil      = FunRes
+    fromResInvSym Int_t Nil = Dict
 
 instance VarArg FloatType
   where
-    aritySym FloatType Nil      = FunRes
-    fromResInvSym FloatType Nil = Dict
+    aritySym Float_t Nil      = FunRes
+    fromResInvSym Float_t Nil = Dict
 
 instance VarArg ListType
   where
-    aritySym ListType _      = FunRes
-    fromResInvSym ListType _ = Dict
+    aritySym List_t _      = FunRes
+    fromResInvSym List_t _ = Dict
 
 instance VarArg FunType
   where
-    aritySym FunType (_ :* b :* Nil) = FunArg $ arity $ TypeRep b
-    fromResInvSym FunType (_ :* b :* Nil)
+    aritySym Fun_t (_ :* b :* Nil) = FunArg $ arity $ TypeRep b
+    fromResInvSym Fun_t (_ :* b :* Nil)
         | Dict <- fromResInv $ TypeRep b = Dict
 
 -- | Get the 'Arity' of a type. The purpose is to be able to distinguish between functions and
diff --git a/src/Language/Syntactic/TypeRep.hs b/src/Language/Syntactic/TypeRep.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Syntactic/TypeRep.hs
@@ -0,0 +1,94 @@
+-- | Utilities for working with ASTs of the form @`AST` (sym `:&:` `TypeRep` t)@
+
+module Language.Syntactic.TypeRep where
+
+
+
+import qualified Data.Typeable as Typeable
+
+import Language.Syntactic
+import Language.Syntactic.Functional
+import Language.Syntactic.Functional.Sharing
+
+import Data.TypeRep
+import Data.TypeRep.Types.Basic
+
+
+
+mkVarSym :: Witness Typeable.Typeable t t =>
+    TypeRep t a -> Name -> BindingT (Full a)
+mkVarSym t v | Dict <- wit pDataTypeable t = VarT v
+
+mkLamSym :: Witness Typeable.Typeable t t
+    => TypeRep t a -> TypeRep t b -> Name
+    -> BindingT (b :-> Full (a -> b))
+mkLamSym ta _ v | Dict <- wit pDataTypeable ta = LamT v
+
+-- | Inject a symbol in an 'AST' with a domain decorated by a type
+-- representation
+injTR :: (sub :<: sup, Typeable t (DenResult sig)) =>
+    sub sig -> AST (sup :&: TypeRep t) sig
+injTR s = Sym (inj s :&: typeRep)
+
+-- | Make a smart constructor of a symbol. 'smartSymT' has any type of the form:
+--
+-- > smartSymTR :: (sub :<: AST (sup :&: TypeRep t), Typeable t x)
+-- >     => sub (a :-> b :-> ... :-> Full x)
+-- >     -> (ASTF sup a -> ASTF sup b -> ... -> ASTF sup x)
+smartSymTR
+    :: ( Signature sig
+       , supT ~ (sup :&: TypeRep t)
+       , f    ~ SmartFun supT sig
+       , sig  ~ SmartSig f
+       , supT ~ SmartSym f
+       , sub :<: sup
+       , Typeable t (DenResult sig)
+       )
+    => sub sig -> f
+smartSymTR s = smartSym' (inj s :&: typeRep)
+
+-- | \"Sugared\" symbol application
+--
+-- 'sugarSymTR' has any type of the form:
+--
+-- > sugarSymTR ::
+-- >     ( sub :<: AST (sup :&: TypeRep t)
+-- >     , Syntactic a
+-- >     , Syntactic b
+-- >     , ...
+-- >     , Syntactic x
+-- >     , Domain a ~ Domain b ~ ... ~ Domain x
+-- >     , Typeable t (Internal x)
+-- >     ) => sub (Internal a :-> Internal b :-> ... :-> Full (Internal x))
+-- >       -> (a -> b -> ... -> x)
+sugarSymTR
+    :: ( Signature sig
+       , supT ~ (sup :&: TypeRep t)
+       , fi   ~ SmartFun supT sig
+       , sig  ~ SmartSig fi
+       , supT ~ SmartSym fi
+       , SyntacticN f fi
+       , sub :<: sup
+       , Typeable t (DenResult sig)
+       )
+    => sub sig -> f
+sugarSymTR = sugarN . smartSymTR
+
+-- | Default 'CodeMotionInterface' for domains of the form
+-- @((... `:+:` `BindingT` `:+:` ... ) `:&:` `TypeRep` t)@
+defaultInterfaceTypeRep :: forall binding sym symT t
+    .  ( BindingT :<: sym
+       , Let      :<: sym
+       , symT ~ (sym :&: TypeRep t)
+       , FunType :<: t
+       , TypeEq t t
+       , Witness Typeable.Typeable t t
+       )
+    => (forall a b . ASTF symT a -> ASTF symT b -> Bool)
+         -- ^ Can the expression represented by the first argument be shared in
+         -- the second argument?
+    -> (forall a . ASTF symT a -> Bool)
+         -- ^ Can we hoist over this expression?
+    -> CodeMotionInterface symT
+defaultInterfaceTypeRep = defaultInterfaceDecor typeEq funType mkVarSym mkLamSym
+
diff --git a/src/Language/Syntactic/TypeRep/Sugar/BindingTR.hs b/src/Language/Syntactic/TypeRep/Sugar/BindingTR.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Syntactic/TypeRep/Sugar/BindingTR.hs
@@ -0,0 +1,53 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | 'Syntactic' instance for functions
+--
+-- This module is based on domains of the form
+-- @((... `:+:` `BindingT` `:+:` ... ) `:&:` `TypeRep` t)@
+
+module Language.Syntactic.TypeRep.Sugar.BindingTR where
+
+
+
+import qualified Data.Typeable as Typeable
+
+import Language.Syntactic
+import Language.Syntactic.Functional
+
+import Data.TypeRep
+import Data.TypeRep.Types.Basic
+import Language.Syntactic.TypeRep
+
+
+
+instance
+    ( sym ~ (s :&: TypeRep t)
+    , Syntactic a, Domain a ~ sym
+    , Syntactic b, Domain b ~ sym
+    , BindingT :<: s
+    , Typeable t (Internal a)
+    , Typeable t (Internal b)
+    , Witness Typeable.Typeable t t
+    , FunType :<: t
+    ) =>
+      Syntactic (a -> b)
+  where
+    type Domain (a -> b)   = Domain a
+    type Internal (a -> b) = Internal a -> Internal b
+
+    desugar f = lamT_template mkVar mkLam (desugar . f . sugar)
+      where
+        ta :: TypeRep t (Internal a)
+        ta = typeRep
+
+        tb :: TypeRep t (Internal b)
+        tb = typeRep
+
+        mkVar :: Name -> sym (Full (Internal a))
+        mkVar v = inj (mkVarSym ta v) :&: ta
+
+        mkLam :: Name -> sym (Internal b :-> Full (Internal a -> Internal b))
+        mkLam v = inj (mkLamSym ta tb v) :&: funType ta tb
+
+    sugar = error "sugar not implemented for (a -> b)"
+
diff --git a/src/Language/Syntactic/TypeRep/Sugar/TupleTR.hs b/src/Language/Syntactic/TypeRep/Sugar/TupleTR.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Syntactic/TypeRep/Sugar/TupleTR.hs
@@ -0,0 +1,73 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | 'Syntactic' instances for tuples and symbol domains decorated with
+-- 'TypeRep'
+
+module Language.Syntactic.TypeRep.Sugar.TupleTR where
+
+
+
+import Language.Syntactic
+import Language.Syntactic.Functional.Tuple
+
+import Data.TypeRep
+import Data.TypeRep.Types.Tuple
+import Data.TypeRep.Types.Tuple.Typeable ()
+import Language.Syntactic.TypeRep
+
+
+
+instance
+    ( sym ~ (s :&: TypeRep t)
+    , Syntactic a, Domain a ~ sym
+    , Syntactic b, Domain b ~ sym
+    , Tuple :<: s
+    , Typeable t (Internal a)
+    , Typeable t (Internal b)
+    , TupleType :<: t
+    ) =>
+      Syntactic (a,b)
+  where
+    type Domain (a,b)   = Domain a
+    type Internal (a,b) = (Internal a, Internal b)
+    desugar (a,b) = sugarSymTR Tup2 a b
+    sugar ab      = (sugarSymTR Sel1 ab, sugarSymTR Sel2 ab)
+
+instance
+    ( sym ~ (s :&: TypeRep t)
+    , Syntactic a, Domain a ~ sym
+    , Syntactic b, Domain b ~ sym
+    , Syntactic c, Domain c ~ sym
+    , Tuple :<: s
+    , Typeable t (Internal a)
+    , Typeable t (Internal b)
+    , Typeable t (Internal c)
+    , TupleType :<: t
+    ) =>
+      Syntactic (a,b,c)
+  where
+    type Domain (a,b,c)   = Domain a
+    type Internal (a,b,c) = (Internal a, Internal b, Internal c)
+    desugar (a,b,c) = sugarSymTR Tup3 a b c
+    sugar abc       = (sugarSymTR Sel1 abc, sugarSymTR Sel2 abc, sugarSymTR Sel3 abc)
+
+instance
+    ( sym ~ (s :&: TypeRep t)
+    , Syntactic a, Domain a ~ sym
+    , Syntactic b, Domain b ~ sym
+    , Syntactic c, Domain c ~ sym
+    , Syntactic d, Domain d ~ sym
+    , Tuple :<: s
+    , Typeable t (Internal a)
+    , Typeable t (Internal b)
+    , Typeable t (Internal c)
+    , Typeable t (Internal d)
+    , TupleType :<: t
+    ) =>
+      Syntactic (a,b,c,d)
+  where
+    type Domain (a,b,c,d)   = Domain a
+    type Internal (a,b,c,d) = (Internal a, Internal b, Internal c, Internal d)
+    desugar (a,b,c,d) = sugarSymTR Tup4 a b c d
+    sugar abcd        = (sugarSymTR Sel1 abcd, sugarSymTR Sel2 abcd, sugarSymTR Sel3 abcd, sugarSymTR Sel4 abcd)
+
diff --git a/src/Language/Syntactic/TypeRep/TupleConversion.hs b/src/Language/Syntactic/TypeRep/TupleConversion.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Syntactic/TypeRep/TupleConversion.hs
@@ -0,0 +1,82 @@
+-- | Construction and elimination of tuples
+--
+-- Something similar can be achieved using the 'Syntactic' instances from
+-- "Language.Syntactic.TypeRep.Sugar.TupleTR", e.g:
+--
+-- > sel1' :: forall sym t a b
+-- >     .  ( Typeable t a
+-- >        , Typeable t b
+-- >        , Tuple     :<: sym
+-- >        , TupleType :<: t
+-- >        )
+-- >     => ASTF (sym :&: TypeRep t) (a,b) -> ASTF (sym :&: TypeRep t) a
+-- > sel1' ab = a
+-- >   where
+-- >     (a, _ :: ASTF (sym :&: TypeRep t) b) = sugar ab
+--
+-- But the point of this module is to do it without the 'Typeable' constraint.
+
+module Language.Syntactic.TypeRep.TupleConversion where
+
+
+
+import Language.Syntactic
+import Language.Syntactic.Functional.Tuple
+
+import Data.TypeRep.Representation
+import Data.TypeRep.Types.Tuple
+import Language.Syntactic.TypeRep.Sugar.TupleTR () -- For documentation
+
+
+
+sel1 :: (Tuple :<: sym, TupleType :<: t) =>
+    ASTF (sym :&: TypeRep t) tup -> ASTF (sym :&: TypeRep t) (Sel1 tup)
+sel1 a = case unTypeRep $ getDecor a of
+    tup :$ ta :$ tb             | Just Tup2_t <- prj tup -> Sym (inj Sel1 :&: TypeRep ta) :$ a
+    tup :$ ta :$ tb :$ tc       | Just Tup3_t <- prj tup -> Sym (inj Sel1 :&: TypeRep ta) :$ a
+    tup :$ ta :$ tb :$ tc :$ td | Just Tup4_t <- prj tup -> Sym (inj Sel1 :&: TypeRep ta) :$ a
+
+sel2 :: (Tuple :<: sym, TupleType :<: t) =>
+    ASTF (sym :&: TypeRep t) tup -> ASTF (sym :&: TypeRep t) (Sel2 tup)
+sel2 a = case unTypeRep $ getDecor a of
+    tup :$ ta :$ tb             | Just Tup2_t <- prj tup -> Sym (inj Sel2 :&: TypeRep tb) :$ a
+    tup :$ ta :$ tb :$ tc       | Just Tup3_t <- prj tup -> Sym (inj Sel2 :&: TypeRep tb) :$ a
+    tup :$ ta :$ tb :$ tc :$ td | Just Tup4_t <- prj tup -> Sym (inj Sel2 :&: TypeRep tb) :$ a
+
+sel3 :: (Tuple :<: sym, TupleType :<: t) =>
+    ASTF (sym :&: TypeRep t) tup -> ASTF (sym :&: TypeRep t) (Sel3 tup)
+sel3 a = case unTypeRep $ getDecor a of
+    tup :$ ta :$ tb :$ tc       | Just Tup3_t <- prj tup -> Sym (inj Sel3 :&: TypeRep tc) :$ a
+    tup :$ ta :$ tb :$ tc :$ td | Just Tup4_t <- prj tup -> Sym (inj Sel3 :&: TypeRep tc) :$ a
+
+sel4 :: (Tuple :<: sym, TupleType :<: t) =>
+    ASTF (sym :&: TypeRep t) tup -> ASTF (sym :&: TypeRep t) (Sel4 tup)
+sel4 a = case unTypeRep $ getDecor a of
+    tup :$ ta :$ tb :$ tc :$ td | Just Tup4_t <- prj tup -> Sym (inj Sel4 :&: TypeRep td) :$ a
+
+tup2
+    :: (Tuple :<: sym, TupleType :<: t)
+    => ASTF (sym :&: TypeRep t) a -> ASTF (sym :&: TypeRep t) b
+    -> ASTF (sym :&: TypeRep t) (a,b)
+tup2 a b =
+    Sym (inj Tup2 :&: tup2Type (getDecor a) (getDecor b))
+      :$ a :$ b
+
+tup3
+    :: (Tuple :<: sym, TupleType :<: t)
+    => ASTF (sym :&: TypeRep t) a -> ASTF (sym :&: TypeRep t) b
+    -> ASTF (sym :&: TypeRep t) c
+    -> ASTF (sym :&: TypeRep t) (a,b,c)
+tup3 a b c =
+    Sym (inj Tup3 :&: tup3Type (getDecor a) (getDecor b) (getDecor c))
+      :$ a :$ b :$ c
+
+tup4
+    :: (Tuple :<: sym, TupleType :<: t)
+    => ASTF (sym :&: TypeRep t) a -> ASTF (sym :&: TypeRep t) b
+    -> ASTF (sym :&: TypeRep t) c -> ASTF (sym :&: TypeRep t) d
+    -> ASTF (sym :&: TypeRep t) (a,b,c,d)
+tup4 a b c d =
+    Sym (inj Tup4 :&: tup4Type (getDecor a) (getDecor b) (getDecor c) (getDecor d))
+      :$ a :$ b :$ c :$ d
+
diff --git a/tests/Tests.hs b/tests/Tests.hs
new file mode 100644
--- /dev/null
+++ b/tests/Tests.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE CPP #-}
+
+import qualified Simple
+#if __GLASGOW_HASKELL__ >= 710
+import qualified Custom
+#endif
+
+
+
+main = do
+    Simple.main
+#if __GLASGOW_HASKELL__ >= 710
+    Custom.main
+#endif
+
+-- Importing both modules causes overlapping instances error on GHC < 7.10
+