diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2014, Emil Axelsson
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Emil Axelsson nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/benchmarks/Dynamic.hs b/benchmarks/Dynamic.hs
new file mode 100644
--- /dev/null
+++ b/benchmarks/Dynamic.hs
@@ -0,0 +1,57 @@
+{-# OPTIONS_GHC -fcontext-stack=100 #-}
+
+import Criterion.Main
+import Criterion.Config
+import Data.Monoid
+
+import Data.TypeRep
+
+import qualified Data.Dynamic as Base  -- For comparison
+
+
+
+type Types  = BoolType :+: IntType :+: ListType
+
+type Types2 = CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: BoolType :+: IntType
+  -- 30 terms
+
+dynList :: Int -> [Dynamic Types]
+dynList n = concat [[toDyn i, toDyn (even i)] | i <- [0..n]]
+
+dynList2 :: Int -> [Dynamic Types2]
+dynList2 n = concat [[toDyn i, toDyn (even i)] | i <- [0..n]]
+
+dynListBase :: Int -> [Base.Dynamic]
+dynListBase n = concat [[Base.toDyn i, Base.toDyn (even i)] | i <- [0..n]]
+
+dynSum :: [Dynamic Types] -> Int
+dynSum ds = sum [i | d <- ds, Just i <- [fromDyn d]]
+
+dynSum2 :: [Dynamic Types2] -> Int
+dynSum2 ds = sum [i | d <- ds, Just i <- [fromDyn d]]
+
+dynSumBase :: [Base.Dynamic] -> Int
+dynSumBase ds = sum [i | d <- ds, Just i <- [Base.fromDynamic d]]
+
+testDyn :: Int -> Int
+testDyn = dynSum . dynList
+
+testDyn2 :: Int -> Int
+testDyn2 = dynSum2 . dynList2
+
+testDynBase :: Int -> Int
+testDynBase = dynSumBase . dynListBase
+
+main :: IO ()
+main = defaultMainWith (defaultConfig {cfgSummaryFile = Last $ Just "bench-results/dynamic.csv"}) (return ())
+    [ bgroup "size=1000"
+       [ bench "testDyn"     $ nf testDyn     1000
+       , bench "testDyn2"    $ nf testDyn2    1000
+       , bench "testDynBase" $ nf testDynBase 1000
+       ]
+    , bgroup "size=2000"
+       [ bench "testDyn"     $ nf testDyn     2000
+       , bench "testDyn2"    $ nf testDyn2    2000
+       , bench "testDynBase" $ nf testDynBase 2000
+       ]
+    ]
diff --git a/examples/Simple.hs b/examples/Simple.hs
new file mode 100644
--- /dev/null
+++ b/examples/Simple.hs
@@ -0,0 +1,28 @@
+import Control.Monad
+
+import Data.TypeRep
+
+type MyUniverse = IntType :+: BoolType
+
+hlist :: [Dynamic MyUniverse]
+hlist = [toDyn True, toDyn (1 :: Int)]
+  -- Prints: [True,1]
+
+addDyn :: (TypeEq ts ts, PWitness Num ts ts) => Dynamic ts -> Dynamic ts -> Maybe (Dynamic ts)
+addDyn (Dyn ta a) (Dyn tb b) = do
+    Dict <- typeEq ta tb
+    Dict <- pwit pNum ta
+    return (Dyn ta (a+b))
+
+
+test1 = toDyn (1 :: Int) `addDyn` toDyn (2 :: Int)
+  -- Prints: Just 3
+
+main = do
+    unless t1 $ fail "Test 1 failed"
+    unless t2 $ fail "Test 2 failed"
+    putStrLn "All tests passed"
+  where
+    t1 = show hlist == "[True,1]"
+    t2 = show (test1 :: Maybe (Dynamic MyUniverse)) == "Just 3"
+
diff --git a/open-typerep.cabal b/open-typerep.cabal
new file mode 100644
--- /dev/null
+++ b/open-typerep.cabal
@@ -0,0 +1,123 @@
+name:                open-typerep
+version:             0.1
+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.
+                     .
+                     Example 1 (dynamic types):
+                     .
+                     > type MyUniverse = IntType :+: BoolType
+                     >
+                     > hlist :: [Dynamic MyUniverse]
+                     > hlist = [toDyn True, toDyn (1 :: Int)]
+                     .
+                     > *Main> hlist
+                     > [True,1]
+                     .
+                     Note that if we were using "Data.Dynamic", it would just print
+                     .
+                     > [<<Bool>>,<<Int>>]
+                     .
+                     Example 2 (dynamically typed addition):
+                     .
+                     > addDyn :: (TypeEq ts ts, PWitness Num ts ts) => Dynamic ts -> Dynamic ts -> Maybe (Dynamic ts)
+                     > addDyn (Dyn ta a) (Dyn tb b) = do
+                     >     Dict <- typeEq ta tb
+                     >     Dict <- pwit pNum ta
+                     >     return (Dyn ta (a+b))
+                     .
+                     "Data.Dynamic" could only do this monomorphically, for one 'Num' type at a
+                     time.
+author:              Emil Axelsson
+maintainer:          emax@chalmers.se
+copyright:           Copyright (c) 2014, Emil Axelsson
+license:             BSD3
+license-file:        LICENSE
+homepage:            https://github.com/emilaxelsson/open-typerep
+bug-reports:         https://github.com/emilaxelsson/open-typerep/issues
+category:            Dependent Types
+stability:           experimental
+build-type:          Simple
+cabal-version:       >=1.10
+tested-with:         GHC==7.6.2, GHC==7.8.2
+
+extra-source-files:
+  examples/*.hs
+
+source-repository head
+  type:     git
+  location: https://github.com/emilaxelsson/open-typerep
+
+library
+  hs-source-dirs: src
+
+  exposed-modules:
+    Data.TypeRep
+    Data.TypeRep.Internal
+
+  other-modules:
+    Data.TypeRep.Sub
+
+  build-depends:
+    base        >=4 && <5,
+    constraints >=0.3,
+    syntactic   >=2.0,
+    tagged      >=0.4
+
+  default-language: Haskell2010
+
+  default-extensions:
+    FlexibleContexts
+    FlexibleInstances
+    GADTs
+    MultiParamTypeClasses
+    ScopedTypeVariables
+    TypeFamilies
+    TypeOperators
+
+  other-extensions:
+    UndecidableInstances,
+    OverlappingInstances
+
+test-suite examples
+  type: exitcode-stdio-1.0
+
+  hs-source-dirs: examples
+
+  main-is: Simple.hs
+
+  default-language: Haskell2010
+
+  build-depends:
+    open-typerep,
+    base
+
+  default-language: Haskell2010
+
+  default-extensions:
+    FlexibleContexts
+    GADTs
+    TypeOperators
+
+benchmark dynamic-bench
+  type: exitcode-stdio-1.0
+
+  hs-source-dirs: benchmarks
+
+  main-is: Dynamic.hs
+
+  build-depends:
+    base,
+    criterion,
+    open-typerep
+
+  default-language: Haskell2010
+
+  default-extensions:
+    FlexibleInstances
+    GADTs
+    MultiParamTypeClasses
+    TypeOperators
+
+  other-extensions:
+    TemplateHaskell
diff --git a/src/Data/TypeRep.hs b/src/Data/TypeRep.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/TypeRep.hs
@@ -0,0 +1,61 @@
+-- | Open type representations and dynamic types
+
+module Data.TypeRep
+    ( -- * Helper types
+      module Data.Constraint
+    , module Data.Proxy
+    , module Data.Syntactic
+      -- * Type representations
+    , Typeable
+    , TypeRep
+    , TypeEq
+    , typeEq
+    , matchCon
+    , matchConM
+    , Witness
+    , PWitness
+    , wit
+    , pwit
+      -- * Dynamic types
+    , cast
+    , gcast
+    , Dynamic (..)
+    , toDyn
+    , fromDyn
+    , dynToInteger
+      -- * Type class witnessing
+    , Any
+    , witTypeable
+    , pwitTypeable
+    , pAny
+    , pEq
+    , pOrd
+    , pShow
+    , pNum
+    , pIntegral
+    , BoolType
+    , CharType
+    , IntType
+    , FloatType
+    , ListType
+    , FunType
+    , boolType
+    , charType
+    , intType
+    , floatType
+    , listType
+    , funType
+      -- * Sub-universes
+    , module Data.TypeRep.Sub
+    ) where
+
+
+
+import Data.Constraint (Dict (..))
+import Data.Proxy (Proxy (..))
+
+import Data.Syntactic ((:+:), Project (..), (:<:) (..), E (..))
+
+import Data.TypeRep.Internal
+import Data.TypeRep.Sub
+
diff --git a/src/Data/TypeRep/Internal.hs b/src/Data/TypeRep/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/TypeRep/Internal.hs
@@ -0,0 +1,414 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | Open type representations and dynamic types
+
+module Data.TypeRep.Internal where
+
+
+
+import Data.Constraint (Dict (..))
+import Data.Proxy (Proxy (..))
+
+import Data.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 TypeEq t u
+  where
+    typeEqSym
+        :: (t sig1, Args (AST u) sig1)
+        -> (t sig2, Args (AST u) sig2)
+        -> Maybe (Dict (DenResult sig1 ~ DenResult sig2))
+
+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 _ _ = Nothing
+
+instance TypeEq t t => TypeEq (AST t) t
+  where
+    typeEqSym (Sym t1, as1)   (Sym t2, as2)   = typeEqSym (t1,as1) (t2,as2)
+    typeEqSym (s1 :$ a1, as1) (s2 :$ a2, as2) = typeEqSym (s1, a1 :* as1) (s2, a2 :* as2)
+
+instance TypeEq Empty t
+  where
+    typeEqSym = error "typeEqSym: Empty"
+
+-- | Equality on type representations
+typeEq :: forall t a b . TypeEq t t => TypeRep t a -> TypeRep t b -> Maybe (Dict (a ~ b))
+typeEq (TypeRep s1) (TypeRep s2) = typeEqSym (s1, Nil :: Args (AST t) (Full a)) (s2, Nil)
+
+-- | 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 PWitness p t u
+  where
+    pwitSym :: t sig -> Args (AST u) sig -> Maybe (Dict (p (DenResult sig)))
+    pwitSym _ _ = Nothing
+
+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
+
+instance PWitness p t t => PWitness p (AST t) t
+  where
+    pwitSym (Sym s)  as = pwitSym s as
+    pwitSym (s :$ a) as = pwitSym s (a :* as)
+
+-- | Default implementation of 'pwitSym' for types that have a 'Witness' instance
+pwitSymDefault :: Witness p t u => t sig -> Args (AST u) sig -> Maybe (Dict (p (DenResult sig)))
+pwitSymDefault t = Just . 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 a . PWitness p t t => Proxy p -> TypeRep t a -> Maybe (Dict (p a))
+pwit _ (TypeRep a) = pwitSym a (Nil :: Args (AST t) (Full a))
+
+
+
+----------------------------------------------------------------------------------------------------
+-- * 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 -> Maybe 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 -> Maybe (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 -> Maybe 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
+        | Just 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
+
+-- | 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 -> Maybe (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)  = Just Dict
+instance TypeEq CharType  t where typeEqSym (CharType, Nil)  (CharType, Nil)  = Just Dict
+instance TypeEq IntType   t where typeEqSym (IntType, Nil)   (IntType, Nil)   = Just Dict
+instance TypeEq FloatType t where typeEqSym (FloatType, Nil) (FloatType, Nil) = Just 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 _ _ = Just Dict
+instance PWitness Any CharType  t where pwitSym _ _ = Just Dict
+instance PWitness Any IntType   t where pwitSym _ _ = Just Dict
+instance PWitness Any FloatType t where pwitSym _ _ = Just Dict
+instance PWitness Any ListType  t where pwitSym _ _ = Just Dict
+instance PWitness Any FunType   t where pwitSym _ _ = Just 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 -> Maybe Integer
+dynToInteger (Dyn tr a)
+    | Just Dict <- pwit pIntegral tr = Just (toInteger a)
+dynToInteger _ = Nothing
+
diff --git a/src/Data/TypeRep/Sub.hs b/src/Data/TypeRep/Sub.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/TypeRep/Sub.hs
@@ -0,0 +1,33 @@
+{-# LANGUAGE OverlappingInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | This module is only to limit the scope of the @OverlappingInstances@ flag
+
+module Data.TypeRep.Sub where
+
+
+
+import Data.Syntactic
+
+import Data.TypeRep.Internal
+
+
+
+-- | Sub-universe relation
+--
+-- In general, a universe @t@ is a sub-universe of @u@ if @u@ has the form
+--
+-- > t1 :+: t2 :+: ... :+: t
+class SubUniverse sub sup
+  where
+    -- | Cast a type representation to a larger universe
+    weakenUniverse :: TypeRep sub a -> TypeRep sup a
+
+instance SubUniverse t t
+  where
+    weakenUniverse = id
+
+instance (SubUniverse sub sup', sup ~ (t :+: sup')) => SubUniverse sub sup
+  where
+    weakenUniverse = sugar . mapAST InjR . desugar . weakenUniverse
+