diff --git a/README.md b/README.md
index 85d9460..bcbcbdc 100644
--- a/README.md
+++ b/README.md
@@ -3,7 +3,7 @@ Reified types for Purescript
 
 This is an implementation of indexed typereps for Purescript, similar to the [corresponding implementation in Haskell](https://hackage.haskell.org/package/base-4.10.0.0/docs/Type-Reflection.html#t:TypeRep).
 
-## API
+## Data.Typeable
 
 `TypeReps` are values that represent types (i.e. they reify types). When they are *indexed* they have the type itself as a parameter.
 
@@ -32,100 +32,56 @@ We can also test typereps for equality -
 eqTypeRep :: forall a b. TypeRep a -> TypeRep b -> Boolean
 ```
 
-## Mini tutorial on using Typeable and TypeReps
-
-As an example, with typereps we can have dynamic values which carry around the type information as a value -
-
-```purescript
-data Dynamic' a = Dynamic' (TypeRep a) a
-data Dynamic = Dynamic (Exists Dynamic')
-
--- Wrap a value into a dynamic
-dynamic :: forall a. 
-dynamic a = Dynamic (mkExists (Dynamic' typeRep a)) -- The compiler picks the appropriate typerep automatically
-```
-
-To get a value out of a dynamic, we must have a way to convert a `TypeRep` into typelevel information. We do this with *witnesses*.
-However witnesses require GADTs, and since Purescript does not have GADTs, we hack around it with Leibniz equality -
-
-```purescript
--- | Two types are equal if they are _equal in all contexts_.
-newtype Leibniz a b = Leibniz (forall f. f a -> f b)
-infix 4 type Leibniz as ~
-```
-
-Now we can compare two typereps and recover type information -
+We can compare two typeReps and extract a witness for type equality.
 
 ```purescript
 eqT :: forall a b. TypeRep a -> TypeRep b -> Maybe (a ~ b)
-eqT ta tb
-  | eqTypeRep ta tb = Just (unsafeCoerce identity)
-  | otherwise = Nothing
 ```
 
-And use this information to unwrap a dynamic value. We need to pass the type we expect to find in the dynamic -
+## Data.Dynamic
+
+We can have dynamic values which holds a value `a` in a context `t` and forgets the type of `a`
 
 ```purescript
-unwrapDynamic :: forall a. TypeRep a -> Dynamic -> Maybe a
-unwrapDynamic ta (Dynamic e) = runExists e \(Dynamic ta tb) -> case eqT ta tb of
-  Nothing -> Nothing
-  Just witness -> runLeibniz witness tb
+data Dynamic t
+```
+
+We can wrap a value into a dynamic
+
+```purescript
+-- Wrap a value into a dynamic
+dynamic :: forall a t. Typeable a => t a -> Dynamic t
+```
+
+We can recover a value out of a dynamics if supply the type we expect to find in the Dynamic
+
+```purescript
+unwrapDynamic :: forall a. TypeRep a -> Dynamic t -> Maybe a
 ```
 
 ## Deriving `Typeable` for custom data types
 
-### Create a `Tag` instance for your data type
+It's extremely easy. You just need to create a mechanical `Tag` class instance for your datatype. There are different `Tag` classes for types of different arity.
 
-First create a mechanical `Tag` class instance for your datatype. There are different `Tag` classes for types of different arity.
-
-For example, to derive an instance for a plain data type, use `Tag1` and `Proxy1` -
+For example, to derive an instance for a plain data type, use `Tag1` and `proxy1` -
 
 ```purescript
 data Person = Person {name::String, age::Int}
 
-instance tag1Person :: Tag1 Person where t1 = Proxy1
+instance tag1Person :: Tag1 Person where t1 = proxy1
 ```
 
-For a data type which takes one type parameter, use `Tag2` and `Proxy2`, and so on -
+For a data type which takes one type parameter, use `Tag2` and `proxy2`, and so on -
 
 ```purescript
 data Optional a = Some a | None
 
-instance tag2Optional :: Tag2 Optional where t2 = Proxy2
+instance tag2Optional :: Tag2 Optional where t2 = proxy2
 ```
 
-Don't worry about getting it wrong since the type system will prevent you from writing an invalid instance.
+**Don't worry about getting it wrong since the type system will prevent you from writing an invalid instance.**
 
-> #### CAVEATS
-> There are two cases where the compiler would not prevent you from writing an invalid instance. Without compiler support it's very hard to prevent these mistakes at compile time.
-> However the good thing is that these mistakes are hard to make unless you are actively looking to subvert the type system, and accidental mistakes will be caught at compile time.
-> 
-> 1. *Do not include type parameters in your instance*.
-> 
->     For example do not create an instance for `Tag1 (Optional a)`.
->     
->     That would give the same typerep to all `Optional`s, for example `Optional Int` and `Optional String` would have the same typerep.
-> 
->     The compiler would prevent you from including type params in your instance *accidentally*, for example you would get an error on defining an instance for `Tag2 (Optional a)`.
-> 
-> 2. *Do not add any extra constraints to the instances*. For example don't do `Foo => Tag1 Person`.
+> #### CAVEAT
+> *Do not add any extra constraints to the instances*. For example don't do `Foo => Tag1 Person`. This currently cannot be caught by the type checker, but will break typerep comparisons for your data type.
 
-### Then create a `Typeable` instance for your datatype
-
-Write a mechanical `Typeable` instance for your datatype -
-
-1. Use one of the baked in `typerepImpl` functions as the implementation for your instance. For example, use `typerepImpl1` for plain types which take no type arguments, use `typerepImpl2` for types that take one argument, and so on.
-2. Add constrinats to make sure that all type parameters are `Typeable` too.
-3. Add a constraint for appropriate tag instance as a constraint.
-
-Again, don't worry about getting it wrong since the type system will prevent you from writing an invalid instance.
-
-```purescript
-instance typeablePerson :: Typeable Person where typeRep = typerepImpl1
-```
-
-```purescript
-instance typeableOptional :: Typeable a => Typeable (Optional a) where typeRep = typerepImpl2
-```
-
-And that's it! You are done!
+And that's it! You are done! Now your datatype will have a `Typeable` instance.
diff --git a/spago.dhall b/spago.dhall
index 1c86410..f824aad 100644
--- a/spago.dhall
+++ b/spago.dhall
@@ -3,7 +3,15 @@ Welcome to a Spago project!
 You can edit this file as you like.
 -}
 { name = "typeable"
-, dependencies = [ "console", "effect", "psci-support", "either", "arrays" ]
+, dependencies =
+  [ "console"
+  , "effect"
+  , "psci-support"
+  , "either"
+  , "arrays"
+  , "exists"
+  , "leibniz"
+  ]
 , packages = ./packages.dhall
 , sources = [ "src/**/*.purs", "test/**/*.purs" ]
 }
diff --git a/src/Data/Dynamic.purs b/src/Data/Dynamic.purs
new file mode 100644
index 0000000..4b70156
--- /dev/null
+++ b/src/Data/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/Typeable.js b/src/Data/Typeable.js
new file mode 100644
index 0000000..c5c3f36
--- /dev/null
+++ b/src/Data/Typeable.js
@@ -0,0 +1,64 @@
+exports.typeRepDefault0 = function(t) {
+    return t;
+};
+
+exports.typeRepFromTag1 = pack('tag1');
+
+exports.showTypeRep = function(t) {
+    console.log(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;
+
+// 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');
+
+function pack(tagName) {
+    return function(origTag) {
+        let unwrappedTag = origTag[tagName];
+        return function(dict) {
+            if(unwrappedTag.tag) return {tag:unwrappedTag.tag, args:unwrappedTag.args.concat(dict)};
+            return {tag: origTag, args: [dict]};
+        };
+    };
+};
+
+exports.eqTypeRep = function(t1) {
+    return function(t2) {
+        return eqTypeRepHelper(t1,t2);
+    };
+};
+
+function eqTypeRepHelper(t1,t2) {
+    if(t1.tag0) return t1 === t2;
+    if(t1.tag !== t2.tag) return false;
+    if(t1.args.length !== t2.args.length) return false;
+    for (var i=0; i<t1.args.length;i++) {
+        if(!eqTypeRepHelper(t1.args[i].typeRep, t2.args[i].typeRep)) return false;
+    }
+    return true;
+}
diff --git a/src/Data/Typeable.purs b/src/Data/Typeable.purs
new file mode 100644
index 0000000..f241f7b
--- /dev/null
+++ b/src/Data/Typeable.purs
@@ -0,0 +1,180 @@
+module Data.Typeable
+( TypeRep
+, class Typeable
+, typeRep
+, eqT
+, eqTypeRep
+, typeRepFromVal
+, SomeTypeRep(..)
+, 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
+) where
+
+import Control.Category (identity)
+import Data.Boolean (otherwise)
+import Data.Either (Either)
+import Data.Exists (Exists, runExists)
+import Data.Function ((#))
+import Data.Leibniz (type (~), Leibniz)
+import Data.Maybe (Maybe(..))
+import Data.Ordering (Ordering)
+import Data.Show (class Show)
+import Data.Unit (Unit)
+import Unsafe.Coerce (unsafeCoerce)
+
+-- | Indexed TypeReps
+data TypeRep a
+
+-- | `Typeable` things have a `TypeRep`
+class Typeable a where
+  typeRep :: TypeRep a
+
+instance showTypeRepInstance :: Show (TypeRep a) where
+  show t = showTypeRep t
+
+-- | Compare two `TypeRep`, and potentially return a type witness for equality
+eqT :: forall a b. TypeRep a -> TypeRep b -> Maybe (a ~ b)
+eqT ta tb
+  | eqTypeRep ta tb = Just (unsafeCoerce (identity :: Leibniz a a))
+  | otherwise = Nothing
+
+-- | Compare two `TypeRep`, potentially of differing types, for equality
+foreign import eqTypeRep :: forall a b. TypeRep a -> TypeRep b -> Boolean
+
+-- | Get the `TypeRep` for a value
+typeRepFromVal :: forall a. Typeable a => a -> TypeRep a
+typeRepFromVal _ = typeRep
+
+-- | Unindexed typereps
+data SomeTypeRep = SomeTypeRep (Exists TypeRep)
+
+-- | Unwrap a TypeRep
+unwrapSomeTypeRep :: forall r. SomeTypeRep -> (forall a. TypeRep a -> r) -> r
+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 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)
+
+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
+
+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
+
+-- 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)
+
+instance tag0FromTag1 :: (Tag1 t, Typeable a) => Typeable (t a) where
+  typeRep = typeRepFromTag1
+else
+instance typeableTag0 :: Tag0 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
+
+-- COMMON INSTANCES
+
+instance taggedInt :: Tag0 Int where
+  tag0 = proxy0
+
+instance tag0Boolean :: Tag0 Boolean where
+  tag0 = proxy0
+
+instance tag0Number :: Tag0 Number where
+  tag0 = proxy0
+
+instance tag0String :: Tag0 String where
+  tag0 = proxy0
+
+instance tag0Unit :: Tag0 Unit where
+  tag0 = proxy0
+
+instance taggedArray :: Tag1 Array where
+  tag1 = proxy1
+
+instance tag2Func :: Tag2 (->) where
+  tag2 = proxy2
+
+instance tag2Either :: Tag2 Either where
+  tag2 = proxy2
+
+instance tag0Ordering :: Tag0 Ordering where
+  tag0 = proxy0
diff --git a/src/Typeable.js b/src/Typeable.js
deleted file mode 100644
index 15411b7..0000000
--- a/src/Typeable.js
+++ /dev/null
@@ -1,42 +0,0 @@
-exports.typerepImpl1 = function(t1) {
-  return t1;
-};
-
-exports.typerepImpl2 = function(t1) {
-  return function(t2) {
-    return [t1,t2];
-  };
-};
-
-exports.typerepImpl3 = function(t1) {
-    return function(t2) {
-        return function(t3) {
-            return [t1,t2,t3];
-        };
-    };
-};
-
-exports.eqTypeRep = function(t1) {
-    return function(t2) {
-        return nestedArrayEq(t1, t2);
-    };
-};
-
-exports.clog = function(a) {
-    return function() {
-        console.log("CLOG:", a);
-    };
-};
-
-function nestedArrayEq(t1, t2) {
-  if(Array.isArray(t1)) {
-      if(!(Array.isArray(t2) && (t1.length == t2.length)))
-          return false;
-      for (var i=0; i<t1.length;i++) {
-          if(!nestedArrayEq(t1[i], t2[i]))
-              return false;
-      }
-      return true;
-  }
-  return t1 === t2;
-}
diff --git a/src/Typeable.purs b/src/Typeable.purs
deleted file mode 100644
index 4f93d77..0000000
--- a/src/Typeable.purs
+++ /dev/null
@@ -1,40 +0,0 @@
-module Typeable where
-
-import Data.Either (Either)
-import Data.Unit (Unit)
-import Effect (Effect)
-
--- Indexed TypeReps
-data TypeRep a
-
--- Typeable class
-class Typeable a where
-  typeRep :: TypeRep a
-
--- Implementation detail
--- Tagging types
-data Proxy1 a = Proxy1
-data Proxy2 (t :: Type -> Type) = Proxy2
-data Proxy3 (t :: Type -> Type -> Type) = Proxy3
-class Tag1 a where t1 :: Proxy1 a
-class Tag2 (a :: Type -> Type) where t2 :: Proxy2 a
-class Tag3 (a :: Type -> Type -> Type) where t3 :: Proxy3 a
-
--- Constructors for the opaque data type
-foreign import typerepImpl1 :: forall a. Tag1 a => TypeRep a
-foreign import typerepImpl2 :: forall a b. Tag2 a => Typeable b => TypeRep (a b)
-foreign import typerepImpl3 :: forall a b c. Tag3 a => Typeable b => Typeable c => TypeRep (a b c)
-
--- Type equality
-foreign import eqTypeRep :: forall a b. TypeRep a -> TypeRep b -> Boolean
-
--- Common instances
-instance tag1Int :: Tag1 Int where t1 = Proxy1
-instance typeableInt :: Typeable Int where typeRep = typerepImpl1
-instance tag2Array :: Tag2 Array where t2 = Proxy2
-instance typeableArray :: Typeable a => Typeable (Array a) where typeRep = typerepImpl2
-instance tag3Either :: Tag3 Either where t3 = Proxy3
-instance typeableEither :: (Typeable a, Typeable b) => Typeable (Either a b) where typeRep = typerepImpl3
-
--- DEBUG: Console.log anything
-foreign import clog :: forall a. a -> Effect Unit
diff --git a/test/Main.js b/test/Main.js
new file mode 100644
index 0000000..b46dcf1
--- /dev/null
+++ b/test/Main.js
@@ -0,0 +1,5 @@
+exports.clog = function(x) {
+    return function() {
+        console.log(x);
+    };
+};
diff --git a/test/Main.purs b/test/Main.purs
index deb122f..60cbe26 100644
--- a/test/Main.purs
+++ b/test/Main.purs
@@ -3,39 +3,38 @@ 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 Effect (Effect)
-import Typeable (class Tag1, class Tag2, class Typeable, Proxy1(..), Proxy2(..), TypeRep, clog, eqTypeRep, typeRep, typerepImpl1, typerepImpl2)
+
+foreign import clog :: forall a. a -> Effect Unit
 
 main :: Effect Unit
 main = do
+  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 :: _ (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))
   where
     typeArrPerson :: TypeRep (Array Person)
     typeArrPerson = typeRep
+    typePerson :: TypeRep Person
+    typePerson = typeRep
 
+data Foo a b c = Foo
+instance tag3Foo :: Tag3 Foo where tag3 = proxy3
 
 newtype Person = Person { name :: String, location :: String }
+instance tag0Person :: Tag0 Person where tag0 = proxy0
+
 newtype Person2 = Person2 { name :: String, location :: String }
-
--- Create Typeable instances for Person
-instance tag1Person :: Tag1 Person where t1 = Proxy1
-instance typeablePerson :: Typeable Person where typeRep = typerepImpl1
-
--- Create Typeable instances for Person2
-instance tag1Person2 :: Tag1 Person2 where t1 = Proxy1
-instance typeablePerson2 :: Typeable Person2 where typeRep = typerepImpl1
+instance tag0Person2 :: Tag0 Person2 where tag0 = proxy0
 
 data Optional a = None | Some a
-
--- Create Typeable instances for Person
-instance tag2Optional :: Tag2 Optional where t2 = Proxy2
-instance typeableOptional :: Typeable a => Typeable (Optional a) where
-  typeRep = typerepImpl2
-
-typeRepFromVal :: forall a. Typeable a => a -> TypeRep a
-typeRepFromVal _ = typeRep
+instance tag1Optional :: Tag1 Optional where tag1 = proxy1