diff --git a/attic/Data.purs b/attic/Data.purs
new file mode 100644
index 0000000..8ab3903
--- /dev/null
+++ b/attic/Data.purs
@@ -0,0 +1,279 @@
+module Data.Data where
+
+import Control.Alt ((<|>))
+import Control.Alternative (empty)
+import Control.Applicative (pure)
+import Control.Bind (bind, (>>=))
+import Control.Category (identity, (<<<))
+import Control.Monad (class Monad)
+import Control.MonadPlus (class MonadPlus)
+import Data.Array as A
+import Data.CommutativeRing ((+))
+import Data.Const (Const(..))
+import Data.Either (Either(..))
+import Data.Eq ((==))
+import Data.Foldable (foldl)
+import Data.Function (const, ($))
+import Data.Identity (Identity(..))
+import Data.Maybe (Maybe(..), fromMaybe, maybe)
+import Data.Newtype (unwrap)
+import Data.Ordering (Ordering)
+import Data.Tuple (Tuple(..))
+import Data.Typeable (class Tag0, class Tag1, class Typeable, cast)
+import Data.Unit (Unit)
+import Unsafe.Coerce (unsafeCoerce)
+
+mkT :: forall a b. Typeable a => Typeable b => (b -> b) -> a -> a
+mkT f = fromMaybe identity (cast f)
+
+mkQ :: forall a b r. Typeable a => Typeable b => r -> (b -> r) -> a -> r
+mkQ r q a = maybe r q (cast a)
+
+mkM :: forall a b m. Typeable a => Typeable b => Monad m => Tag1 m => (b -> m b) -> a -> m a
+mkM f = fromMaybe pure (cast f)
+
+-- Purescript can't have cycles in typeclasses
+-- So we manually reify the dictionary into the DataDict datatype
+-- Not using wrapped records here because Purescript can't handle constraints inside records
+newtype DataDict a = DataDict
+  (forall c. (forall d b. Data d => c (d -> b) -> d -> c b)
+      -- ^ defines how nonempty constructor applications are
+      -- folded.  It takes the folded tail of the constructor
+      -- application and its head, i.e., an immediate subterm,
+      -- and combines them in some way.
+  -> (forall g. g -> c g)
+      -- ^ defines how the empty constructor application is
+      -- folded, like the neutral \/ start element for list
+      -- folding.
+  -> a
+      -- ^ structure to be folded.
+  -> c a
+      -- ^ result, with a type defined in terms of @a@, but
+      -- variability is achieved by means of type constructor
+      -- @c@ for the construction of the actual result type.
+  )
+
+gfoldl  :: forall a c. Data a => (forall d b. Data d => c (d -> b) -> d -> c b)
+                -- ^ defines how nonempty constructor applications are
+                -- folded.  It takes the folded tail of the constructor
+                -- application and its head, i.e., an immediate subterm,
+                -- and combines them in some way.
+          -> (forall g. g -> c g)
+                -- ^ defines how the empty constructor application is
+                -- folded, like the neutral \/ start element for list
+                -- folding.
+          -> a
+                -- ^ structure to be folded.
+          -> c a
+                -- ^ result, with a type defined in terms of @a@, but
+                -- variability is achieved by means of type constructor
+                -- @c@ for the construction of the actual result type.
+gfoldl = let DataDict f = dataDict in f
+
+class Typeable a <= Data a where
+  dataDict :: DataDict a
+
+-- | A generic transformation that maps over the immediate subterms
+--
+-- The default definition instantiates the type constructor @c@ in the
+-- type of 'gfoldl' to an identity datatype constructor, using the
+-- isomorphism pair as injection and projection.
+gmapT :: forall a. Data a => (forall b. Data b => b -> b) -> a -> a
+
+-- Use the Identity datatype constructor
+-- to instantiate the type constructor c in the type of gfoldl,
+-- and perform injections Identity and projections runIdentity accordingly.
+--
+gmapT f x0 = unwrap (gfoldl k Identity x0)
+  where
+    k :: forall d b. Data d => Identity (d->b) -> d -> Identity b
+    k (Identity c) x = Identity (c (f x))
+
+
+-- | A generic query with a left-associative binary operator
+gmapQl :: forall a r r'. Data a => (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r
+gmapQl o r f = unwrap <<< gfoldl k z
+  where
+    k :: forall d b. Data d => Const r (d->b) -> d -> Const r b
+    k c x = Const $ (unwrap c) `o` f x
+    z :: forall g. g -> Const r g
+    z _   = Const r
+
+-- | A generic query with a right-associative binary operator
+gmapQr :: forall a r r'. Data a => (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r
+gmapQr o r0 f x0 = unQr (gfoldl k (const (Qr identity)) x0) r0
+  where
+    k :: forall d b. Data d => Qr r (d->b) -> d -> Qr r b
+    k (Qr c) x = Qr (\r -> c (f x `o` r))
+
+
+-- | A generic query that processes the immediate subterms and returns a list
+-- of results.  The list is given in the same order as originally specified
+-- in the declaration of the data constructors.
+gmapQ :: forall a u. Data a => (forall d. Data d => d -> u) -> a -> Array u
+gmapQ f = gmapQr (A.cons) [] f
+
+
+-- | A generic query that processes one child by index (zero-based)
+gmapQi :: forall u a. Data a => Int -> (forall d. Data d => d -> u) -> a -> u
+gmapQi i f x = case gfoldl k z x of Qi _ q -> case q of
+                                                   Nothing -> unsafeCoerce "UNEXPECTED NOTHING"
+                                                   Just q' -> q'
+  where
+    k :: forall d b. Data d => Qi u (d -> b) -> d -> Qi u b
+    k (Qi i' q) a = Qi (i'+1) (if i==i' then Just (f a) else q)
+    z :: forall g q. g -> Qi q g
+    z _           = Qi 0 Nothing
+
+
+-- | A generic monadic transformation that maps over the immediate subterms
+--
+-- The default definition instantiates the type constructor @c@ in
+-- the type of 'gfoldl' to the monad datatype constructor, defining
+-- injection and projection using 'return' and '>>='.
+gmapM :: forall m a. Data a => Monad m => (forall d. Data d => d -> m d) -> a -> m a
+
+-- Use immediately the monad datatype constructor
+-- to instantiate the type constructor c in the type of gfoldl,
+-- so injection and projection is done by return and >>=.
+--
+gmapM f = gfoldl k pure
+  where
+    k :: forall b d. Data d => m (d -> b) -> d -> m b
+    k c x = do c' <- c
+               x' <- f x
+               pure (c' x')
+
+
+-- | Transformation of at least one immediate subterm does not fail
+gmapMp :: forall m a. Data a => MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a
+
+{-
+
+The type constructor that we use here simply keeps track of the fact
+if we already succeeded for an immediate subterm; see Mp below. To
+this end, we couple the monadic computation with a Boolean.
+
+-}
+
+gmapMp f x = unMp (gfoldl k z x) >>= \(Tuple x' b) ->
+              if b then pure x' else empty
+  where
+    z :: forall g. g -> Mp m g
+    z g = Mp (pure (Tuple g false))
+    k :: forall d b. Data d => Mp m (d -> b) -> d -> Mp m b
+    k (Mp c) y
+      = Mp ( c >>= \(Tuple h b) ->
+               (f y >>= \y' -> pure (Tuple (h y') true))
+               <|> pure (Tuple (h y) b)
+           )
+
+-- | Transformation of one immediate subterm with success
+gmapMo :: forall m a. Data a => MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a
+
+{-
+
+We use the same pairing trick as for gmapMp,
+i.e., we use an extra Boolean component to keep track of the
+fact whether an immediate subterm was processed successfully.
+However, we cut of mapping over subterms once a first subterm
+was transformed successfully.
+
+-}
+
+gmapMo f x = unMp (gfoldl k z x) >>= \(Tuple x' b) ->
+              if b then pure x' else empty
+  where
+    z :: forall g. g -> Mp m g
+    z g = Mp (pure (Tuple g false))
+    k :: forall d b. Data d => Mp m (d -> b) -> d -> Mp m b
+    k (Mp c) y
+      = Mp ( c >>= \(Tuple h b) -> if b
+                      then pure (Tuple (h y) b)
+                      else (f y >>= \y' -> pure (Tuple (h y') true))
+                           <|> pure (Tuple (h y) b)
+           )
+
+
+
+-- | Type constructor for adding counters to queries
+data Qi q a = Qi Int (Maybe q)
+
+
+-- | The type constructor used in definition of gmapQr
+newtype Qr r a = Qr (r -> r)
+
+unQr :: forall r a. Qr r a -> r -> r
+unQr (Qr f) = f
+
+-- | The type constructor used in definition of gmapMp
+newtype Mp m x = Mp (m (Tuple x Boolean))
+
+unMp :: forall m x. Mp m x -> m (Tuple x Boolean)
+unMp (Mp f) = f
+
+
+-- | Left-associative fold operation for constructor applications.
+--
+-- The type of 'gfoldl' is a headache, but operationally it is a simple
+-- generalisation of a list fold.
+--
+-- The default definition for 'gfoldl' is @'const' 'id'@, which is
+-- suitable for abstract datatypes with no substructures.
+-- gfoldl
+
+
+-- TODO: Why do we need `Tag0` here? Instead of `Typeable`.
+instance dataArray :: (Tag0 a, Data a) => Data (Array a) where
+  dataDict = DataDict \k z arr -> case A.uncons arr of
+    Nothing -> z []
+    Just x -> (z A.cons `k` x.head) `k` x.tail
+
+instance dataMaybe :: (Tag0 a, Data a) => Data (Maybe a) where
+  dataDict = DataDict \k z e -> case e of
+    Nothing -> z Nothing
+    Just a -> z Just `k` a
+
+instance dataEither :: (Tag0 a, Tag0 b, Data a, Data b) => Data (Either a b) where
+  dataDict = DataDict \k z e -> case e of
+    Left a -> z Left `k` a
+    Right b -> z Right `k` b
+
+instance dataBoolean :: Data Boolean where
+  dataDict = DataDict \k z x -> z x
+
+instance dataInt :: Data Int where
+  dataDict = DataDict \k z x -> z x
+
+instance dataNumber :: Data Number where
+  dataDict = DataDict \k z x -> z x
+
+instance dataChar :: Data Char where
+  dataDict = DataDict \k z x -> z x
+
+instance dataString :: Data String where
+  dataDict = DataDict \k z x -> z x
+
+instance dataUnit :: Data Unit where
+  dataDict = DataDict \k z x -> z x
+
+instance dataOrdering :: Data Ordering where
+  dataDict = DataDict \k z x -> z x
+
+-- Combinators
+
+-- | Apply a transformation everywhere, bottom-up
+everywhere :: forall a. Data a => (forall b. Data b => b -> b) -> a -> a
+everywhere f x = f (gmapT (everywhere f) x)
+
+-- | Apply a transformation everywhere, top-down
+everywhere' :: forall a. Data a => (forall b. Data b => b -> b) -> a -> a
+everywhere' f x = gmapT (everywhere' f) (f x)
+
+-- | Summarise all nodes in top-down, left-to-right
+everything :: forall a r. Data a => (r -> r -> r) -> (forall b. Data b => b -> r) -> a -> r
+everything k f x = foldl k (f x) (gmapQ (everything k f) x)
+
+-- | Apply a monadic transformation everywhere, bottom-up
+everywhereM :: forall m a. Monad m => Data a => (forall b. Data b => b -> m b) -> a -> m a
+everywhereM f x = gmapM (everywhereM f) x >>= f
diff --git a/attic/Dynamic.purs b/attic/Dynamic.purs
new file mode 100644
index 0000000..4b70156
--- /dev/null
+++ b/attic/Dynamic.purs
@@ -0,0 +1,21 @@
+module Data.Dynamic where
+
+import Data.Exists (Exists, mkExists, runExists)
+import Data.Function ((#))
+import Data.Functor (map)
+import Data.Leibniz (runLeibniz)
+import Data.Maybe (Maybe)
+import Data.Typeable (class Typeable, TypeRep, eqT, typeRep)
+
+-- | A `Dynamic` holds a value `a` in a context `t`
+-- | and forgets the type of `a`
+data Dynamic' t a = Dynamic' (TypeRep a) (t a)
+data Dynamic t = Dynamic (Exists (Dynamic' t))
+
+-- | Wrap a value into a dynamic
+dynamic :: forall t a. Typeable a => t a -> Dynamic t
+dynamic a = Dynamic (mkExists (Dynamic' typeRep a))
+
+-- | Extract a value from a dynamic
+unwrapDynamic :: forall t a. TypeRep a -> Dynamic t -> Maybe (t a)
+unwrapDynamic ta (Dynamic e) = e # runExists \(Dynamic' ti v) -> map (\w -> runLeibniz w v) (eqT ti ta)
diff --git a/src/Data/Data.purs b/src/Data/Data.purs
index 8ab3903..4854626 100644
--- a/src/Data/Data.purs
+++ b/src/Data/Data.purs
@@ -19,7 +19,7 @@ import Data.Maybe (Maybe(..), fromMaybe, maybe)
 import Data.Newtype (unwrap)
 import Data.Ordering (Ordering)
 import Data.Tuple (Tuple(..))
-import Data.Typeable (class Tag0, class Tag1, class Typeable, cast)
+import Data.Typeable (class TagT, class Typeable, cast)
 import Data.Unit (Unit)
 import Unsafe.Coerce (unsafeCoerce)
 
@@ -29,7 +29,7 @@ mkT f = fromMaybe identity (cast f)
 mkQ :: forall a b r. Typeable a => Typeable b => r -> (b -> r) -> a -> r
 mkQ r q a = maybe r q (cast a)
 
-mkM :: forall a b m. Typeable a => Typeable b => Monad m => Tag1 m => (b -> m b) -> a -> m a
+mkM :: forall a b m. Typeable a => Typeable b => Monad m => TagT m => (b -> m b) -> a -> m a
 mkM f = fromMaybe pure (cast f)
 
 -- Purescript can't have cycles in typeclasses
@@ -197,10 +197,12 @@ gmapMo f x = unMp (gfoldl k z x) >>= \(Tuple x' b) ->
 
 
 -- | Type constructor for adding counters to queries
+data Qi :: forall k. Type -> k -> Type
 data Qi q a = Qi Int (Maybe q)
 
 
 -- | The type constructor used in definition of gmapQr
+newtype Qr :: forall k. Type -> k -> Type
 newtype Qr r a = Qr (r -> r)
 
 unQr :: forall r a. Qr r a -> r -> r
@@ -223,42 +225,42 @@ unMp (Mp f) = f
 -- gfoldl
 
 
--- TODO: Why do we need `Tag0` here? Instead of `Typeable`.
-instance dataArray :: (Tag0 a, Data a) => Data (Array a) where
+-- TODO: Why do we need `TagT` here? Instead of `Typeable`.
+instance dataArray :: (TagT a, Data a) => Data (Array a) where
   dataDict = DataDict \k z arr -> case A.uncons arr of
     Nothing -> z []
     Just x -> (z A.cons `k` x.head) `k` x.tail
 
-instance dataMaybe :: (Tag0 a, Data a) => Data (Maybe a) where
+instance dataMaybe :: (TagT a, Data a) => Data (Maybe a) where
   dataDict = DataDict \k z e -> case e of
     Nothing -> z Nothing
     Just a -> z Just `k` a
 
-instance dataEither :: (Tag0 a, Tag0 b, Data a, Data b) => Data (Either a b) where
+instance dataEither :: (TagT a, TagT b, Data a, Data b) => Data (Either a b) where
   dataDict = DataDict \k z e -> case e of
     Left a -> z Left `k` a
     Right b -> z Right `k` b
 
 instance dataBoolean :: Data Boolean where
-  dataDict = DataDict \k z x -> z x
+  dataDict = DataDict \_ z x -> z x
 
 instance dataInt :: Data Int where
-  dataDict = DataDict \k z x -> z x
+  dataDict = DataDict \_ z x -> z x
 
 instance dataNumber :: Data Number where
-  dataDict = DataDict \k z x -> z x
+  dataDict = DataDict \_ z x -> z x
 
 instance dataChar :: Data Char where
-  dataDict = DataDict \k z x -> z x
+  dataDict = DataDict \_ z x -> z x
 
 instance dataString :: Data String where
-  dataDict = DataDict \k z x -> z x
+  dataDict = DataDict \_ z x -> z x
 
 instance dataUnit :: Data Unit where
-  dataDict = DataDict \k z x -> z x
+  dataDict = DataDict \_ z x -> z x
 
 instance dataOrdering :: Data Ordering where
-  dataDict = DataDict \k z x -> z x
+  dataDict = DataDict \_ z x -> z x
 
 -- Combinators
 
diff --git a/src/Data/Dynamic.purs b/src/Data/Dynamic.purs
index 4b70156..149042b 100644
--- a/src/Data/Dynamic.purs
+++ b/src/Data/Dynamic.purs
@@ -9,6 +9,7 @@ import Data.Typeable (class Typeable, TypeRep, eqT, typeRep)
 
 -- | A `Dynamic` holds a value `a` in a context `t`
 -- | and forgets the type of `a`
+data Dynamic' :: forall k. (k -> Type) -> k -> Type
 data Dynamic' t a = Dynamic' (TypeRep a) (t a)
 data Dynamic t = Dynamic (Exists (Dynamic' t))
 
diff --git a/src/Data/Typeable.js b/src/Data/Typeable.js
index c756f3e..8abcb06 100644
--- a/src/Data/Typeable.js
+++ b/src/Data/Typeable.js
@@ -5,39 +5,18 @@ exports.typeRepDefault0 = function(t) {
     return t;
 };
 
-exports.typeRepFromTag1 = pack('tag1');
+exports.typeRepFromTag1 = pack('tagT');
 
 exports.showTypeRep = function(t) {
     return "" + t;
 };
 
-exports.proxy0 = tag;
-exports.proxy1 = tag;
-exports.proxy2 = tag;
-exports.proxy3 = tag;
-exports.proxy4 = tag;
-exports.proxy5 = tag;
-exports.proxy6 = tag;
-exports.proxy7 = tag;
-exports.proxy8 = tag;
-exports.proxy9 = tag;
-exports.proxy10 = tag;
-exports.proxy11 = tag;
+exports.proxyT = tag;
 
 // Just a JS class, instances of which can be tested for equality
 function tag() {}
 
-// exports.proxy0FromTag1 = pack('tag1');
-exports.proxy1FromTag2 = pack('tag2');
-exports.proxy2FromTag3 = pack('tag3');
-exports.proxy3FromTag4 = pack('tag4');
-exports.proxy4FromTag5 = pack('tag5');
-exports.proxy5FromTag6 = pack('tag6');
-exports.proxy6FromTag7 = pack('tag7');
-exports.proxy7FromTag8 = pack('tag8');
-exports.proxy8FromTag9 = pack('tag9');
-exports.proxy9FromTag10 = pack('tag10');
-exports.proxy10FromTag11 = pack('tag11');
+exports.proxyTFromTagT = pack('tagT');
 
 function pack(tagName) {
     return function(origTag) {
@@ -77,7 +56,7 @@ exports.typeRowCons = function(_) {
 exports.typeRowNil = {record: []};
 
 function eqTypeRepHelper(t1,t2) {
-    if(t1.tag0) return t1 === t2;
+    if(t1.tagT) return t1 === t2;
     if(t1.tag !== t2.tag) return false;
     if(t1.record) {
         if(!t2.record) return false;
diff --git a/src/Data/Typeable.purs b/src/Data/Typeable.purs
index f5955f7..d0f081e 100644
--- a/src/Data/Typeable.purs
+++ b/src/Data/Typeable.purs
@@ -15,10 +15,8 @@ module Data.Typeable
 , SomeTypeRep(..)
 , wrapSomeTypeRep
 , unwrapSomeTypeRep
-, Proxy0, Proxy1, Proxy2, Proxy3, Proxy4, Proxy5, Proxy6, Proxy7, Proxy8, Proxy9, Proxy10, Proxy11
-, proxy0, proxy1, proxy2, proxy3, proxy4, proxy5, proxy6, proxy7, proxy8, proxy9, proxy10, proxy11
-, class Tag0, class Tag1, class Tag2, class Tag3, class Tag4, class Tag5, class Tag6, class Tag7, class Tag8, class Tag9, class Tag10, class Tag11
-, tag0, tag1, tag2, tag3, tag4, tag5, tag6, tag7, tag8, tag9, tag10, tag11
+, ProxyT, proxyT
+, class TagT, tagT
 ) where
 
 import Control.Category (identity)
@@ -65,12 +63,12 @@ gcast a = m # map \f -> runLeibniz f a
   where
   m = eqT (typeRep :: _ a) (typeRep :: _ b)
 
-gcast1 :: forall s t a c. Typeable a => Tag1 c => Tag1 s => Tag1 t => c (s a) -> Maybe (c (t a))
+gcast1 :: forall s t a c. Typeable a => TagT c => TagT s => TagT t => c (s a) -> Maybe (c (t a))
 gcast1 a = m # map \f -> runLeibniz f a
   where
   m = eqT (typeRep :: _ (s a)) (typeRep :: _ (t a))
 
-gcast2 :: forall s t a b c. Typeable a => Typeable b => Tag1 c => Tag2 s => Tag2 t => c (s a b) -> Maybe (c (t a b))
+gcast2 :: forall s t a b c. Typeable a => Typeable b => TagT c => TagT s => TagT t => c (s a b) -> Maybe (c (t a b))
 gcast2 a = m # map \f -> runLeibniz f a
   where
   m = eqT (typeRep :: _ (s a b)) (typeRep :: _ (t a b))
@@ -94,101 +92,33 @@ unwrapSomeTypeRep (SomeTypeRep e) f = e # runExists f
 
 -- MACHINERY + INSTANCES
 
-foreign import typeRepDefault0 :: forall a. Tag0 a => TypeRep a
-foreign import typeRepFromTag1 :: forall a b. Tag1 a => Typeable b => TypeRep (a b)
+foreign import typeRepDefault0 :: forall a. TagT a => TypeRep a
+foreign import typeRepFromTag1 :: forall a b. TagT a => Typeable b => TypeRep (a b)
 foreign import showTypeRep :: forall a. TypeRep a -> String
 
--- Tagging types
--- These would be a lot simpler after PolyKinds
-data Proxy0  (t :: Type)
-data Proxy1  (t :: Type -> Type)
-data Proxy2  (t :: Type -> Type -> Type)
-data Proxy3  (t :: Type -> Type -> Type -> Type)
-data Proxy4  (t :: Type -> Type -> Type -> Type -> Type)
-data Proxy5  (t :: Type -> Type -> Type -> Type -> Type -> Type)
-data Proxy6  (t :: Type -> Type -> Type -> Type -> Type -> Type -> Type)
-data Proxy7  (t :: Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type)
-data Proxy8  (t :: Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type)
-data Proxy9  (t :: Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type)
-data Proxy10 (t :: Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type)
-data Proxy11 (t :: Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type)
+-- Tagging types, this is basically the same as `Type.Proxy`
+-- but we don't want to export any constructors
+data ProxyT :: forall k. k -> Type
+data ProxyT t
 
-foreign import proxy0  :: forall t. Proxy0 t
-foreign import proxy1  :: forall t. Proxy1 t
-foreign import proxy2  :: forall t. Proxy2 t
-foreign import proxy3  :: forall t. Proxy3 t
-foreign import proxy4  :: forall t. Proxy4 t
-foreign import proxy5  :: forall t. Proxy5 t
-foreign import proxy6  :: forall t. Proxy6 t
-foreign import proxy7  :: forall t. Proxy7 t
-foreign import proxy8  :: forall t. Proxy8 t
-foreign import proxy9  :: forall t. Proxy9 t
-foreign import proxy10 :: forall t. Proxy10 t
-foreign import proxy11 :: forall t. Proxy11 t
+foreign import proxyT  :: forall t. ProxyT t
 
-class Tag0  a where tag0 :: Proxy0 a
-class Tag1  (a :: Type -> Type) where tag1 :: Proxy1 a
-class Tag2  (a :: Type -> Type -> Type) where tag2 :: Proxy2 a
-class Tag3  (a :: Type -> Type -> Type -> Type) where tag3 :: Proxy3 a
-class Tag4  (a :: Type -> Type -> Type -> Type -> Type) where tag4 :: Proxy4 a
-class Tag5  (a :: Type -> Type -> Type -> Type -> Type -> Type) where tag5 :: Proxy5 a
-class Tag6  (a :: Type -> Type -> Type -> Type -> Type -> Type -> Type) where tag6 :: Proxy6 a
-class Tag7  (a :: Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type) where tag7 :: Proxy7 a
-class Tag8  (a :: Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type) where tag8 :: Proxy8 a
-class Tag9  (a :: Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type) where tag9 :: Proxy9 a
-class Tag10 (a :: Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type) where tag10 :: Proxy10 a
-class Tag11 (a :: Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type) where tag11 :: Proxy11 a
+class TagT :: forall k. k -> Constraint
+class TagT  a where tagT :: ProxyT a
 
--- foreign import proxy0FromTag1 :: forall t a. Tag1 t => Typeable a => Proxy0 (t a)
-foreign import proxy1FromTag2 :: forall t a. Tag2 t => Typeable a => Proxy1 (t a)
-foreign import proxy2FromTag3 :: forall t a. Tag3 t => Typeable a => Proxy2 (t a)
-foreign import proxy3FromTag4 :: forall t a. Tag4 t => Typeable a => Proxy3 (t a)
-foreign import proxy4FromTag5 :: forall t a. Tag5 t => Typeable a => Proxy4 (t a)
-foreign import proxy5FromTag6 :: forall t a. Tag6 t => Typeable a => Proxy5 (t a)
-foreign import proxy6FromTag7 :: forall t a. Tag7 t => Typeable a => Proxy6 (t a)
-foreign import proxy7FromTag8 :: forall t a. Tag8 t => Typeable a => Proxy7 (t a)
-foreign import proxy8FromTag9 :: forall t a. Tag9 t => Typeable a => Proxy8 (t a)
-foreign import proxy9FromTag10 :: forall t a. Tag10 t => Typeable a => Proxy9 (t a)
-foreign import proxy10FromTag11 :: forall t a. Tag11 t => Typeable a => Proxy10 (t a)
+foreign import proxyTFromTagT :: forall t a. TagT t => Typeable a => ProxyT (t a)
 
 instance typeableRecord :: (RL.RowToList rs ls, TypeableRecordFields ls) => Typeable (Record rs) where
   typeRep = typeRowToTypeRep (typeableRecordFields (RLProxy :: _ ls))
 else
-instance tag0FromTag1 :: (Tag1 t, Typeable a) => Typeable (t a) where
+instance tagTFromTag1 :: (TagT t, Typeable a) => Typeable (t a) where
   typeRep = typeRepFromTag1
 else
-instance typeableTag0 :: Tag0 t => Typeable t where
+instance typeableTagT :: TagT t => Typeable t where
   typeRep = typeRepDefault0
 
-instance tag1FromTag2 :: (Tag2 t, Typeable a) => Tag1 (t a) where
-  tag1 = proxy1FromTag2
-
-instance tag2FromTag3 :: (Tag3 t, Typeable a) => Tag2 (t a) where
-  tag2 = proxy2FromTag3
-
-instance tag3FromTag4 :: (Tag4 t, Typeable a) => Tag3 (t a) where
-  tag3 = proxy3FromTag4
-
-instance tag4FromTag5 :: (Tag5 t, Typeable a) => Tag4 (t a) where
-  tag4 = proxy4FromTag5
-
-instance tag5FromTag6 :: (Tag6 t, Typeable a) => Tag5 (t a) where
-  tag5 = proxy5FromTag6
-
-instance tag6FromTag7 :: (Tag7 t, Typeable a) => Tag6 (t a) where
-  tag6 = proxy6FromTag7
-
-instance tag7FromTag8 :: (Tag8 t, Typeable a) => Tag7 (t a) where
-  tag7 = proxy7FromTag8
-
-instance tag8FromTag9 :: (Tag9 t, Typeable a) => Tag8 (t a) where
-  tag8 = proxy8FromTag9
-
-instance tag9FromTag10 :: (Tag10 t, Typeable a) => Tag9 (t a) where
-  tag9 = proxy9FromTag10
-
-instance tag10FromTag11 :: (Tag11 t, Typeable a) => Tag10 (t a) where
-  tag10 = proxy10FromTag11
+instance tagTFromTagT :: (TagT t, Typeable a) => TagT (t a) where
+  tagT = proxyTFromTagT
 
 -- COMMON INSTANCES
 
@@ -220,35 +150,35 @@ instance typeableRecordFieldsCons
       key = SProxy :: _ key
       tail = typeableRecordFields (RLProxy :: _ rowlistTail)
 
-instance taggedInt :: Tag0 Int where
-  tag0 = proxy0
+instance taggedInt :: TagT Int where
+  tagT = proxyT
 
-instance tag0Boolean :: Tag0 Boolean where
-  tag0 = proxy0
+instance tagTBoolean :: TagT Boolean where
+  tagT = proxyT
 
-instance tag0Number :: Tag0 Number where
-  tag0 = proxy0
+instance tagTNumber :: TagT Number where
+  tagT = proxyT
 
-instance tag0Char :: Tag0 Char where
-  tag0 = proxy0
+instance tagTChar :: TagT Char where
+  tagT = proxyT
 
-instance tag0String :: Tag0 String where
-  tag0 = proxy0
+instance tagTString :: TagT String where
+  tagT = proxyT
 
-instance tag0Unit :: Tag0 Unit where
-  tag0 = proxy0
+instance tagTUnit :: TagT Unit where
+  tagT = proxyT
 
-instance taggedArray :: Tag1 Array where
-  tag1 = proxy1
+instance taggedArray :: TagT Array where
+  tagT = proxyT
 
-instance taggedMaybe :: Tag1 Maybe where
-  tag1 = proxy1
+instance taggedMaybe :: TagT Maybe where
+  tagT = proxyT
 
-instance tag2Func :: Tag2 (->) where
-  tag2 = proxy2
+instance tag2Func :: TagT (->) where
+  tagT = proxyT
 
-instance tag2Either :: Tag2 Either where
-  tag2 = proxy2
+instance tag2Either :: TagT Either where
+  tagT = proxyT
 
-instance tag0Ordering :: Tag0 Ordering where
-  tag0 = proxy0
+instance tagTOrdering :: TagT Ordering where
+  tagT = proxyT
diff --git a/test/Main.purs b/test/Main.purs
index e6d00e9..3d34bf8 100644
--- a/test/Main.purs
+++ b/test/Main.purs
@@ -3,26 +3,34 @@ module Test.Main where
 import Prelude
 
 import Data.Either (Either)
-import Data.Typeable (class Tag0, class Tag1, class Tag3, TypeRep, eqTypeRep, proxy0, proxy1, proxy3, typeRep, typeRepFromVal)
+import Data.Typeable (class TagT, TypeRep, eqTypeRep, proxyT, typeRep, typeRepFromVal)
 import Effect (Effect)
 
 foreign import clog :: forall a. a -> Effect Unit
 
 main :: Effect Unit
 main = do
+  clog (eqTypeRep (typeRep :: _ Int) (typeRep :: _ Char))
+  clog (eqTypeRep (typeRep :: _ Int) (typeRep :: _ Int))
+  clog (typeRep :: _ Char)
+  clog (typeRep :: _ Int)
+
+  clog (typeRep :: _ Array)
   clog (typeRep :: _ {name::String, age::Int})
-  clog (eqTypeRep typeRecord (typeRep :: _ {name::String, age::Int}))
-  clog (eqTypeRep (typeRep :: _ Person) typePerson)
-  clog (eqTypeRep (typeRep :: _ (Array Person)) typeArrPerson)
-  clog (eqTypeRep (typeRep :: _ (Array Person2)) typeArrPerson)
-  clog (eqTypeRep (typeRep :: _ (Optional Int)) (typeRepFromVal (Some 1)))
-  clog (eqTypeRep (typeRep :: _ (Optional Person)) (typeRepFromVal (Some 1)))
-  clog (eqTypeRep (typeRep :: _ (Either Int Person)) (typeRep :: _ (Either Int Person)))
   clog (typeRep :: _ (Int -> Either (Either Int Int) (Optional (Array (Person)))))
   clog (typeRep :: _ (Either (Either Int Int) (Optional (Array (Person)))))
   clog (typeRep :: _ (Either Int Int))
-  clog (typeRep :: _ Int)
   clog (typeRep :: _ (Foo Int Int Int))
+
+  clog (eqTypeRep (typeRep :: _ Array) (typeRep :: _ Array))
+  clog (eqTypeRep (typeRep :: _ Person) typePerson)
+  clog (eqTypeRep (typeRep :: _ (Array Person)) typeArrPerson)
+  clog (eqTypeRep (typeRep :: _ (Array Person2)) typeArrPerson)
+  clog (eqTypeRep typeRecord (typeRep :: _ {name::String, age::Int}))
+  clog (eqTypeRep (typeRep :: _ (Optional Int)) (typeRepFromVal (Some 1)))
+  clog (eqTypeRep (typeRep :: _ (Optional Person)) (typeRepFromVal (Some 1)))
+  clog (eqTypeRep (typeRep :: _ (Either Int Person)) (typeRep :: _ (Either Int Person)))
+
   where
     typeRecord :: TypeRep {age::Int, name::String}
     typeRecord = typeRep
@@ -37,14 +45,15 @@ main = do
 -- A data type without a typeable instance
 data Break
 
+data Foo :: forall k1 k2 k3. k1 -> k2 -> k3 -> Type
 data Foo a b c = Foo
-instance tag3Foo :: Tag3 Foo where tag3 = proxy3
+instance tagFoo :: TagT Foo where tagT = proxyT
 
 newtype Person = Person { name :: String, location :: String }
-instance tag0Person :: Tag0 Person where tag0 = proxy0
+instance tagTPerson :: TagT Person where tagT = proxyT
 
 newtype Person2 = Person2 { name :: String, location :: String }
-instance tag0Person2 :: Tag0 Person2 where tag0 = proxy0
+instance tagTPerson2 :: TagT Person2 where tagT = proxyT
 
 data Optional a = None | Some a
-instance tag1Optional :: Tag1 Optional where tag1 = proxy1
+instance tagOptional :: TagT Optional where tagT = proxyT