diff --git a/Data/OpenWitness.hs b/Data/OpenWitness.hs
--- a/Data/OpenWitness.hs
+++ b/Data/OpenWitness.hs
@@ -1,89 +1,134 @@
+{-# OPTIONS -fno-warn-name-shadowing #-}
 module Data.OpenWitness
 (
-	OpenWitness,
-	RealWorld,IOWitness,newIOWitness,
-	OW,newOpenWitnessOW,runOW,owToIO,
---	unsafeIOWitnessFromInteger,
-	unsafeIOWitnessFromString
+    OpenWitness,
+    RealWorld,IOWitness,newIOWitness,
+    OW,newOpenWitnessOW,runOW,owToIO,
+--    unsafeIOWitnessFromInteger,
+--    unsafeIOWitnessFromString,
+    iowitness
 ) where
 {
-	import Data.Witness;
-	import Unsafe.Coerce;
-	import System.IO.Unsafe (unsafePerformIO);
-	import Control.Concurrent.MVar;
-	import Control.Monad.State;
-	import Data.HashTable;
+    import Prelude;
+    import Data.List;
+    import System.Random;
+    import Language.Haskell.TH;
+    import Unsafe.Coerce;
+    import System.IO.Unsafe (unsafePerformIO);
+    import Control.Concurrent.MVar;
+    import Control.Monad.Fix;
+    import Control.Monad.Trans.State;
+    import Data.Functor.Identity;
+    import Data.Traversable;
+    import Data.Hashable;
+    import Data.Witness;
 
-	unsafeSameType :: EqualType a b;
-	unsafeSameType = unsafeCoerce MkEqualType;
 
-	-- | A witness type that can witness to any type.
-	-- But values cannot be constructed; they can only be generated in 'IO' and certain other monads.
-	;
-	newtype OpenWitness s a = MkOpenWitness Integer deriving Eq;
-	
-	instance SimpleWitness (OpenWitness s) where
-	{
-		matchWitness (MkOpenWitness ua) (MkOpenWitness ub) = 
-			if ua == ub then Just unsafeSameType else Nothing;
-	};
+    unsafeSameType :: a :~: b;
+    unsafeSameType = unsafeCoerce Refl;
 
-	-- | The @s@ type for running 'OW' in 'IO'.
-	;
-	data RealWorld;
+    -- | A witness type that can witness to any type.
+    -- But values cannot be constructed; they can only be generated in 'IO' and certain other monads.
+    ;
+    newtype OpenWitness s (a :: k) = MkOpenWitness Integer deriving Eq;
 
-	-- | An 'OpenWitness' for 'IO'.
-	;
-	type IOWitness = OpenWitness RealWorld;
+    instance TestEquality (OpenWitness s) where
+    {
+        testEquality (MkOpenWitness ua) (MkOpenWitness ub) =
+            if ua == ub then Just unsafeSameType else Nothing;
+    };
 
-	ioWitnessSource :: MVar Integer;
-	{-# NOINLINE ioWitnessSource #-};
-	ioWitnessSource = unsafePerformIO (newMVar 0);
+    -- | The @s@ type for running 'OW' in 'IO'.
+    ;
+    data RealWorld;
 
-	-- | Generate a new 'IOWitness' in 'IO'.
-	;
-	newIOWitness :: forall a. IO (IOWitness a);
-	newIOWitness = do
-	{
-		val <- takeMVar ioWitnessSource;
-		putMVar ioWitnessSource (val + 1);
-		return (MkOpenWitness val);
-	};
-	
-	type OWState = Integer;
-	
-	-- | A runnable monad in which 'OpenWitness' values can be generated.
-	-- The @s@ parameter plays the same role as it does in 'ST', preventing 'OpenWitness' values from one run being used in another.
-	;
-	newtype OW s a = MkOW (State OWState a) deriving (Functor,Monad,MonadFix);
-	
-	-- | Run an 'OW' computation.
-	;
-	runOW :: forall a. (forall s. OW s a) -> a;
-	runOW uw = (\(MkOW st) -> evalState st 0) uw;
-	
-	-- | Generate a new 'OpenWitness' in 'OW'.
-	;
-	newOpenWitnessOW :: forall s a. OW s (OpenWitness s a);
-	newOpenWitnessOW = MkOW (State (\val -> (MkOpenWitness val,val+1)));
-	
-	-- | Run an 'OW' computation in 'IO'.
-	;
-	owToIO :: OW RealWorld a -> IO a;
-	owToIO (MkOW st) = modifyMVar ioWitnessSource (\start -> let
-	{
-		(a,count) = runState st start;
-	} in return (count,a));
-	
-	-- | In the absence of open witness declarations, an unsafe hack to generate 'IOWitness' values.
-	-- This is safe if you use a different integer each time, and if @a@ is a single type.
-	;
-	unsafeIOWitnessFromInteger :: Integer -> IOWitness a;
-	unsafeIOWitnessFromInteger = MkOpenWitness;
-	
-	-- | In the absence of open witness declarations, an unsafe hack to generate 'IOWitness' values.
-	-- This is safe if you use a different string each time (and 'hashString' doesn't collide), and if @a@ is a single type.
-	;
-	unsafeIOWitnessFromString :: String -> IOWitness a;
-	unsafeIOWitnessFromString = unsafeIOWitnessFromInteger . fromIntegral . hashString;
+    -- | An 'OpenWitness' for 'IO'.
+    ;
+    type IOWitness = OpenWitness RealWorld;
+
+    ioWitnessSource :: MVar Integer;
+    {-# NOINLINE ioWitnessSource #-};
+    ioWitnessSource = unsafePerformIO (newMVar 0);
+
+    -- | Generate a new 'IOWitness' in 'IO'.
+    ;
+    newIOWitness :: forall a. IO (IOWitness a);
+    newIOWitness = do
+    {
+        val <- takeMVar ioWitnessSource;
+        putMVar ioWitnessSource (val + 1);
+        return (MkOpenWitness val);
+    };
+
+    type OWState = Integer;
+
+    -- | A runnable monad in which 'OpenWitness' values can be generated.
+    -- The @s@ parameter plays the same role as it does in 'ST', preventing 'OpenWitness' values from one run being used in another.
+    ;
+    newtype OW s a = MkOW (State OWState a) deriving (Functor,Applicative,Monad,MonadFix);
+
+    -- | Run an 'OW' computation.
+    ;
+    runOW :: forall a. (forall s. OW s a) -> a;
+    runOW uw = (\(MkOW st) -> evalState st 0) uw;
+
+    -- | Generate a new 'OpenWitness' in 'OW'.
+    ;
+    newOpenWitnessOW :: forall s a. OW s (OpenWitness s a);
+    newOpenWitnessOW = MkOW (StateT (\val -> Identity (MkOpenWitness val,val+1)));
+
+    -- | Run an 'OW' computation in 'IO'.
+    ;
+    owToIO :: OW RealWorld a -> IO a;
+    owToIO (MkOW st) = modifyMVar ioWitnessSource (\start -> let
+    {
+        (a,count) = runState st start;
+    } in return (count,a));
+
+    -- | An unsafe hack to generate 'IOWitness' values.
+    -- This is safe if you use a different integer each time, and if @a@ is a single type.
+    ;
+    unsafeIOWitnessFromInteger :: Integer -> IOWitness a;
+    unsafeIOWitnessFromInteger = MkOpenWitness;
+
+    -- | An unsafe hack to generate 'IOWitness' values.
+    -- This is safe if you use a different string each time (and 'hashString' doesn't collide), and if @a@ is a single type.
+    ;
+    unsafeIOWitnessFromString :: String -> IOWitness a;
+    unsafeIOWitnessFromString = unsafeIOWitnessFromInteger . fromIntegral . hash;
+
+    -- | Template Haskell function to declare 'IOWitness' values.
+    ;
+    iowitness :: TypeQ -> Q Exp;
+    iowitness qt = do
+    {
+        t <- qt;
+        _ <- forM (freevarsType t) (\v -> reportError ("Type variable "++(show v)++" free in iowitness type"));
+        l <- location;
+        rnd :: Integer <- runIO randomIO;
+        key <- return ((showLoc l) ++ "/" ++ (show rnd));
+        keyExpr <- return (LitE (StringL key));
+        untypedWitExpr <- [| unsafeIOWitnessFromString $(return keyExpr) |];
+        [| $(return untypedWitExpr) :: IOWitness $(return t) |];
+    } where
+    {
+        showLoc :: Loc -> String;
+        showLoc l = (loc_filename l) ++ "=" ++ (loc_package l) ++ ":" ++ (loc_module l) ++ (show (loc_start l)) ++ (show (loc_end l));
+
+        unionList :: (Eq a) => [[a]] -> [a];
+        unionList [] = [];
+        unionList (l:ls) = union l (unionList ls);
+
+        bindingvarTVB :: TyVarBndr -> Name;
+        bindingvarTVB (PlainTV n) = n;
+        bindingvarTVB (KindedTV n _) = n;
+
+        freevarsType :: Language.Haskell.TH.Type -> [Name];
+        freevarsType (ForallT tvbs ps t) =
+         (union (freevarsType t) (unionList (fmap freevarsType ps))) \\ (fmap bindingvarTVB tvbs);
+        freevarsType (VarT name) = [name];
+        freevarsType (AppT t1 t2) = union (freevarsType t1) (freevarsType t2);
+        freevarsType (SigT t _) = freevarsType t;
+        freevarsType _ = [];
+    };
 }
diff --git a/Data/OpenWitness/Dynamic.hs b/Data/OpenWitness/Dynamic.hs
--- a/Data/OpenWitness/Dynamic.hs
+++ b/Data/OpenWitness/Dynamic.hs
@@ -1,53 +1,56 @@
 -- | This is an approximate re-implementation of "Data.Dynamic" using open witnesses.
 module Data.OpenWitness.Dynamic where
 {
-	import Data.Witness;
-	import Data.OpenWitness.Typeable;
+{-
+    import Data.Witness;
+    import Data.OpenWitness.OpenRep;
+    import Data.OpenWitness.Typeable;
 
-	-- * The @Dynamic@ type
-	;
+    -- * The @Dynamic@ type
+    ;
 
-	type Dynamic = Any Rep;
+    type Dynamic = Any OpenRep;
 
-	-- * Converting to and from @Dynamic@
-	;
+    -- * Converting to and from @Dynamic@
+    ;
 
-	toDyn :: Typeable a => a -> Dynamic;
-	toDyn = MkAny rep;
+    toDyn :: Typeable a => a -> Dynamic;
+    toDyn = MkAny rep;
 
-	fromDyn :: Typeable a => Dynamic -> a -> a;
-	fromDyn dyn def = case fromDynamic dyn of
-	{
-		Just a -> a;
-		_ -> def;
-	};
+    fromDyn :: Typeable a => Dynamic -> a -> a;
+    fromDyn dyn def = case fromDynamic dyn of
+    {
+        Just a -> a;
+        _ -> def;
+    };
 
-	fromDynamic :: forall a. Typeable a => Dynamic -> Maybe a;
-	fromDynamic (MkAny uq a) = do
-	{
-		MkEqualType <- matchWitness uq (rep :: Rep a);
-		return a;
-	};
+    fromDynamic :: forall a. Typeable a => Dynamic -> Maybe a;
+    fromDynamic (MkAny uq a) = do
+    {
+        MkEqualType <- testEquality uq (rep :: OpenRep a);
+        return a;
+    };
 
-	-- * Applying functions of dynamic type
-	;
+    -- * Applying functions of dynamic type
+    ;
 
-	dynApply :: Dynamic -> Dynamic -> Maybe Dynamic;
-	dynApply (MkAny (ApplyRep (ApplyRep1 repFn' rx') ry) f) (MkAny rx x) = do
-	{
-		MkEqualType <- matchRep2 repFn' (rep2 :: Rep2 (->));
-		MkEqualType <- matchWitness rx' rx;
-		return (MkAny ry (f x));
-	};
-	dynApply _ _ = Nothing;
+    dynApply :: Dynamic -> Dynamic -> Maybe Dynamic;
+    dynApply (MkAny (ApplyOpenRep (ApplyOpenRep1 repFn' rx') ry) f) (MkAny rx x) = do
+    {
+        MkEqualType <- matchOpenRep2 repFn' (rep2 :: OpenRep2 (->));
+        MkEqualType <- testEquality rx' rx;
+        return (MkAny ry (f x));
+    };
+    dynApply _ _ = Nothing;
 
-	dynApp :: Dynamic -> Dynamic -> Dynamic;
-	dynApp a b = case (dynApply a b) of
-	{
-		Just d -> d;
-		_ -> error "Type error in dynamic application.\nCan't apply function to argument";
-	};
+    dynApp :: Dynamic -> Dynamic -> Dynamic;
+    dynApp a b = case (dynApply a b) of
+    {
+        Just d -> d;
+        _ -> error "Type error in dynamic application.\nCan't apply function to argument";
+    };
 
-	dynTypeRep :: Dynamic -> TypeRep;
-	dynTypeRep (MkAny r _) = MkAnyWitness r;
+    dynTypeRep :: Dynamic -> TypeRep;
+    dynTypeRep (MkAny r _) = MkAnyWitness r;
+-}
 }
diff --git a/Data/OpenWitness/Exception.hs b/Data/OpenWitness/Exception.hs
--- a/Data/OpenWitness/Exception.hs
+++ b/Data/OpenWitness/Exception.hs
@@ -1,39 +1,48 @@
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# OPTIONS -fno-warn-unused-matches #-}
 module Data.OpenWitness.Exception
 (
-	Exn, unsafeExnFromString, throw, catch
+    Exn, declexn, throw, catch
 ) where
 {
-	import Data.OpenWitness;
-	import Data.Witness;
-	import Data.Maybe;
-	import Data.Typeable;
-	import Control.Exception (throwDyn,catchDyn);
-	import Prelude(IO,String);
+    import Data.OpenWitness;
+    import Data.Witness;
+    import Data.Maybe;
+    import Data.Typeable;
+    import Language.Haskell.TH;
+    import qualified Control.Exception as CE (Exception,throw,catch);
+    import Prelude(IO,Show(..));
 
-	-- | A key to match exceptions. The type variable is the data the exception carries.
-	;
-	type Exn = IOWitness;
+    -- | A key to match exceptions. The type variable is the data the exception carries.
+    ;
+    newtype Exn (e :: *) = MkExn (IOWitness e);
 
-	newtype ExnException = MkExnException (Any Exn);
-	
-	-- | In the absence of open witness declarations, an unsafe hack to generate 'Exn' exception keys.
-	-- This is safe if you use a different string each time (and 'hashString' doesn't collide), and if @e@ is a single type.
-	;
-	unsafeExnFromString :: String -> Exn e;
-	unsafeExnFromString = unsafeIOWitnessFromString;
-	
-	instance Typeable ExnException where
-	{
-		typeOf _ = mkTyConApp (mkTyCon "Data.OpenWitness.Exception.ExnException") [];
-	};
-	
-	throw :: Exn e -> e -> a;
-	throw exn e = throwDyn (MkExnException (MkAny exn e));
-	
-	catch :: IO a -> Exn e -> (e -> IO a) -> IO a;
-	catch foo exn catcher = catchDyn foo (\ex@(MkExnException cell) -> case matchAny exn cell of
-	{
-		Just e -> catcher e;
-		_ -> throwDyn ex;
-	});
+    instance TestEquality Exn where
+    {
+        testEquality (MkExn a) (MkExn b) = testEquality a b;
+    };
+
+    newtype ExnException = MkExnException (Any Exn) deriving Typeable;
+
+    -- | Template Haskell function to declare 'Exn' exception keys.
+    ;
+    declexn :: TypeQ -> Q Exp;
+    declexn te = [| MkExn $(iowitness te) |];
+
+    instance Show ExnException where
+    {
+        show _ = "ExnException";
+    };
+
+    instance CE.Exception ExnException;
+
+    throw :: Exn e -> e -> a;
+    throw exn e = CE.throw (MkExnException (MkAny exn e));
+
+    catch :: IO a -> Exn e -> (e -> IO a) -> IO a;
+    catch foo exn catcher = CE.catch foo (\ex@(MkExnException cell) -> case matchAny exn cell of
+    {
+        Just e -> catcher e;
+        _ -> CE.throw ex;
+    });
 }
diff --git a/Data/OpenWitness/OpenRep.hs b/Data/OpenWitness/OpenRep.hs
new file mode 100644
--- /dev/null
+++ b/Data/OpenWitness/OpenRep.hs
@@ -0,0 +1,70 @@
+module Data.OpenWitness.OpenRep where
+{
+--    import Data.Witness;
+--    import Data.OpenWitness;
+--    import Data.Maybe;
+{-
+        data T2 (a :: * -> * -> *);
+
+    data OpenRep2 p where
+    {
+        SimpleOpenRep2 :: IOWitness (T2 p) -> OpenRep2 p;
+--        ApplyOpenRep2 :: OpenRep3 p -> OpenRep a -> OpenRep2 (p a);
+    };
+
+    matchOpenRep2 :: OpenRep2 a -> OpenRep2 b -> Maybe (EqualType (T2 a) (T2 b));
+    matchOpenRep2 (SimpleOpenRep2 wa) (SimpleOpenRep2 wb) = testEquality wa wb;
+{-
+    matchOpenRep2 (ApplyOpenRep1 tfa ta) (ApplyOpenRep1 tfb tb) = do
+    {
+        MkEqualType <- matchOpenRep2 tfa tfb;
+        MkEqualType <- testEquality ta tb;
+        return MkEqualType;
+    };
+    matchOpenRep2 _ _ = Nothing;
+-}
+
+        data T1 (a :: * -> *);
+
+    data OpenRep1 p where
+    {
+        SimpleOpenRep1 :: IOWitness (T1 p) -> OpenRep1 p;
+        ApplyOpenRep1 :: OpenRep2 p -> OpenRep a -> OpenRep1 (p a);
+    };
+
+    matchOpenRep1 :: OpenRep1 a -> OpenRep1 b -> Maybe (EqualType (T1 a) (T1 b));
+    matchOpenRep1 (SimpleOpenRep1 wa) (SimpleOpenRep1 wb) = testEquality wa wb;
+    matchOpenRep1 (ApplyOpenRep1 tfa ta) (ApplyOpenRep1 tfb tb) = do
+    {
+        MkEqualType <- matchOpenRep2 tfa tfb;
+        MkEqualType <- testEquality ta tb;
+        return MkEqualType;
+    };
+    matchOpenRep1 _ _ = Nothing;
+-}
+
+{-
+    data OpenRep :: k -> * where
+    {
+        SimpleOpenRep :: IOWitness a -> OpenRep a;
+        ApplyOpenRep :: OpenRep p -> OpenRep a -> OpenRep (p a);
+    };
+
+    instance TestEquality OpenRep where
+    {
+        testEquality (SimpleOpenRep wa) (SimpleOpenRep wb) = testEquality wa wb;
+        testEquality (ApplyOpenRep tfa ta) (ApplyOpenRep tfb tb) = do
+        {
+            MkEqualType <- testEquality tfa tfb;
+            MkEqualType <- testEquality ta tb;
+            return MkEqualType;
+        };
+        testEquality _ _ = Nothing;
+    };
+
+    instance Eq1 OpenRep where
+    {
+        equals1 r1 r2 = isJust (testEquality r1 r2);
+    };
+-}
+}
diff --git a/Data/OpenWitness/ST.hs b/Data/OpenWitness/ST.hs
--- a/Data/OpenWitness/ST.hs
+++ b/Data/OpenWitness/ST.hs
@@ -1,57 +1,59 @@
 -- | This is an approximate re-implementation of "Control.Monad.ST" and "Data.STRef" using open witnesses.
 module Data.OpenWitness.ST
 (
-	-- * The @ST@ Monad
-	ST,runST,fixST,
-	-- * Converting @ST@ to @OW@ and @IO@
-	stToOW,RealWorld,stToIO,
-	-- * STRefs
-	STRef,newSTRef,readSTRef,writeSTRef,modifySTRef
+    -- * The @ST@ Monad
+    ST,runST,fixST,
+    -- * Converting @ST@ to @OW@ and @IO@
+    stToOW,RealWorld,stToIO,
+    -- * STRefs
+    STRef,newSTRef,readSTRef,writeSTRef,modifySTRef
 ) where
 {
-	import Data.OpenWitness;
-	import Data.Witness.WitnessDict;
-	import Control.Monad.State;
-	
-	type ST s = StateT (WitnessDict (OpenWitness s)) (OW s);
+    import Data.OpenWitness;
+    import Data.Witness.WitnessDict;
+    import Control.Monad.Trans.State;
+    import Control.Monad.Trans.Class;
+    import Control.Monad.Fix;
 
-	stToOW :: ST s a -> OW s a;
-	stToOW st = evalStateT st emptyWitnessDict;
+    type ST s = StateT (WitnessDict (OpenWitness s)) (OW s);
 
-	runST :: (forall s . ST s a) -> a;
-	runST st = runOW (stToOW st);
-	
-	fixST :: (a -> ST s a) -> ST s a;
-	fixST = mfix;
+    stToOW :: ST s a -> OW s a;
+    stToOW st = evalStateT st emptyWitnessDict;
 
-	type STRef = OpenWitness;
-	
-	newSTRef :: a -> ST s (STRef s a);
-	newSTRef a = do
-	{
-		wit <- lift newOpenWitnessOW;
-		dict <- get;
-		put (witnessDictAdd wit a dict);
-		return wit;
-	};
-	
-	readSTRef :: STRef s a -> ST s a;
-	readSTRef key = do
-	{
-		dict <- get;
-		case witnessDictLookup key dict of
-		{
-			Just a -> return a;
-			_ -> fail "ref not found";
-		};
-	};
-	
-	writeSTRef :: forall s a. STRef s a -> a -> ST s ();
-	writeSTRef key newa = modify (witnessDictReplace key newa);
-	
-	modifySTRef :: forall s a. STRef s a -> (a -> a) -> ST s ();
-	modifySTRef key amap = modify (witnessDictModify key amap);
-	
-	stToIO :: ST RealWorld a -> IO a;
-	stToIO = owToIO . stToOW;
+    runST :: (forall s . ST s a) -> a;
+    runST st = runOW (stToOW st);
+
+    fixST :: (a -> ST s a) -> ST s a;
+    fixST = mfix;
+
+    type STRef = OpenWitness;
+
+    newSTRef :: a -> ST s (STRef s a);
+    newSTRef a = do
+    {
+        wit <- lift newOpenWitnessOW;
+        dict <- get;
+        put (witnessDictAdd wit a dict);
+        return wit;
+    };
+
+    readSTRef :: STRef s a -> ST s a;
+    readSTRef key = do
+    {
+        dict <- get;
+        case witnessDictLookup key dict of
+        {
+            Just a -> return a;
+            _ -> fail "ref not found";
+        };
+    };
+
+    writeSTRef :: forall s a. STRef s a -> a -> ST s ();
+    writeSTRef key newa = modify (witnessDictReplace key newa);
+
+    modifySTRef :: forall s a. STRef s a -> (a -> a) -> ST s ();
+    modifySTRef key amap = modify (witnessDictModify key amap);
+
+    stToIO :: ST RealWorld a -> IO a;
+    stToIO = owToIO . stToOW;
 }
diff --git a/Data/OpenWitness/Typeable.hs b/Data/OpenWitness/Typeable.hs
--- a/Data/OpenWitness/Typeable.hs
+++ b/Data/OpenWitness/Typeable.hs
@@ -1,109 +1,102 @@
 -- | This is an approximate re-implementation of "Data.Typeable" using open witnesses.
-module Data.OpenWitness.Typeable
-(
-	module Data.OpenWitness.Typeable.Rep,
-	module Data.OpenWitness.Typeable
-) where
+module Data.OpenWitness.Typeable where
 {
-	import Data.OpenWitness.Typeable.Rep;
-	import Data.OpenWitness;
-	import Data.Witness;
-	import Data.Maybe;
+{-
+    import Data.OpenWitness.OpenRep;
+    import Data.OpenWitness;
+    import Data.Witness;
 
-	-- | types of kind @*@ with a representation
-	;
-	class Typeable a where
-	{
-		rep :: Rep a;
-	};
+    -- | types of kind @*@ with a representation
+    ;
+    class Typeable a where
+    {
+        rep :: OpenRep a;
+    };
 
-	-- | types of kind @* -> *@ with a representation
-	;
-	class Typeable1 t where
-	{
-		rep1 :: Rep1 t;
-	};
+    -- | types of kind @* -> *@ with a representation
+    ;
+    class Typeable1 t where
+    {
+        rep1 :: OpenRep1 t;
+    };
 
-	-- | types of kind @* -> * -> *@ with a representation
-	;
-	class Typeable2 t where
-	{
-		rep2 :: Rep2 t;
-	};
+    -- | types of kind @* -> * -> *@ with a representation
+    ;
+    class Typeable2 t where
+    {
+        rep2 :: OpenRep2 t;
+    };
 
-	instance (Typeable1 f,Typeable a) => Typeable (f a) where
-	{
-		rep = ApplyRep rep1 rep;
-	};
+    instance (Typeable1 f,Typeable a) => Typeable (f a) where
+    {
+        rep = ApplyOpenRep rep1 rep;
+    };
 
-	instance (Typeable2 f,Typeable a) => Typeable1 (f a) where
-	{
-		rep1 = ApplyRep1 rep2 rep;
-	};
+    instance (Typeable2 f,Typeable a) => Typeable1 (f a) where
+    {
+        rep1 = ApplyOpenRep1 rep2 rep;
+    };
 
-	instance Typeable2 (->) where
-	{
-		rep2 = SimpleRep2 witFn where
-		{
-			witFn :: IOWitness (() -> ()); -- <- newIOWitness;
-			witFn = unsafeIOWitnessFromString "Data.OpenWitness.Typeable.witFn";
-		};
-	};
+    instance Typeable2 (->) where
+    {
+        rep2 = SimpleOpenRep2 $(iowitness [t|T2 (->)|]);
+    };
 
-	cast :: forall a b. (Typeable a,Typeable b) => a -> Maybe b;
-	cast a = do
-	{
-		MkEqualType :: EqualType a b <- matchWitness rep rep;
-		return a;
-	};
+    cast :: forall a b. (Typeable a,Typeable b) => a -> Maybe b;
+    cast a = do
+    {
+        MkEqualType :: EqualType a b <- testEquality rep rep;
+        return a;
+    };
 
-	gcast :: forall a b c. (Typeable a,Typeable b) => c a -> Maybe (c b);
-	gcast ca = do
-	{
-		MkEqualType :: EqualType a b <- matchWitness rep rep;
-		return ca;
-	};
+    gcast :: forall a b c. (Typeable a,Typeable b) => c a -> Maybe (c b);
+    gcast ca = do
+    {
+        MkEqualType :: EqualType a b <- testEquality rep rep;
+        return ca;
+    };
 
-	-- | represents a type of kind @*@
-	;
-	type TypeRep = AnyWitness Rep;
+    -- | represents a type of kind @*@
+    ;
+    type TypeRep = AnyWitness OpenRep;
 
-	typeOf :: forall t. (Typeable t) => t -> TypeRep;
-	typeOf _ = MkAnyWitness (rep :: Rep t);
-	
-	-- | represents a type of kind @* -> *@
-	;
-	type TypeRep1 = AnyWitness1 Rep1;
+    typeOf :: forall t. (Typeable t) => t -> TypeRep;
+    typeOf _ = MkAnyWitness (rep :: OpenRep t);
 
-	typeOf1 :: forall t a. (Typeable1 t) => t a -> TypeRep1;
-	typeOf1 _ = MkAnyWitness1 (rep1 :: Rep1 t);
-	
-	-- | represents a type of kind @* -> * -> *@
-	;
-	type TypeRep2 = AnyWitness2 Rep2;
+    -- | represents a type of kind @* -> *@
+    ;
+    type TypeRep1 = AnyWitness1 OpenRep1;
 
-	typeOf2 :: forall t a b. (Typeable2 t) => t a b -> TypeRep2;
-	typeOf2 _ = MkAnyWitness2 (rep2 :: Rep2 t);
-	
-	-- | given representations of @a@ and @b@, make a representation of @a -> b@
-	;
-	mkFunTy :: TypeRep -> TypeRep -> TypeRep;
-	mkFunTy (MkAnyWitness ta) (MkAnyWitness tb) = MkAnyWitness (ApplyRep (ApplyRep1 (rep2 :: Rep2 (->)) ta) tb);
+    typeOf1 :: forall t a. (Typeable1 t) => t a -> TypeRep1;
+    typeOf1 _ = MkAnyWitness1 (rep1 :: OpenRep1 t);
 
-	-- | given representations of @a -> b@ and @a@, make a representation of @b@ (otherwise not)
-	;
-	funResultTy :: TypeRep -> TypeRep -> Maybe TypeRep;
-	funResultTy (MkAnyWitness (ApplyRep (ApplyRep1 repFn' ta') tb')) (MkAnyWitness ta) = do
-	{
-		MkEqualType <- matchRep2 repFn' (rep2 :: Rep2 (->));
-		MkEqualType <- matchWitness ta' ta;
-		return (MkAnyWitness tb');
-	};
-	funResultTy _ _ = Nothing;
-	
-	mkAppTy :: TypeRep1 -> TypeRep -> TypeRep;
-	mkAppTy (MkAnyWitness1 tf) (MkAnyWitness ta) = MkAnyWitness (ApplyRep tf ta);
-	
-	mkAppTy1 :: TypeRep2 -> TypeRep -> TypeRep1;
-	mkAppTy1 (MkAnyWitness2 tf) (MkAnyWitness ta) = MkAnyWitness1 (ApplyRep1 tf ta);
+    -- | represents a type of kind @* -> * -> *@
+    ;
+    type TypeRep2 = AnyWitness2 OpenRep2;
+
+    typeOf2 :: forall t a b. (Typeable2 t) => t a b -> TypeRep2;
+    typeOf2 _ = MkAnyWitness2 (rep2 :: OpenRep2 t);
+
+    -- | given representations of @a@ and @b@, make a representation of @a -> b@
+    ;
+    mkFunTy :: TypeRep -> TypeRep -> TypeRep;
+    mkFunTy (MkAnyWitness ta) (MkAnyWitness tb) = MkAnyWitness (ApplyOpenRep (ApplyOpenRep1 (rep2 :: OpenRep2 (->)) ta) tb);
+
+    -- | given representations of @a -> b@ and @a@, make a representation of @b@ (otherwise not)
+    ;
+    funResultTy :: TypeRep -> TypeRep -> Maybe TypeRep;
+    funResultTy (MkAnyWitness (ApplyOpenRep (ApplyOpenRep1 repFn' ta') tb')) (MkAnyWitness ta) = do
+    {
+        MkEqualType <- matchOpenRep2 repFn' (rep2 :: OpenRep2 (->));
+        MkEqualType <- testEquality ta' ta;
+        return (MkAnyWitness tb');
+    };
+    funResultTy _ _ = Nothing;
+
+    mkAppTy :: TypeRep1 -> TypeRep -> TypeRep;
+    mkAppTy (MkAnyWitness1 tf) (MkAnyWitness ta) = MkAnyWitness (ApplyOpenRep tf ta);
+
+    mkAppTy1 :: TypeRep2 -> TypeRep -> TypeRep1;
+    mkAppTy1 (MkAnyWitness2 tf) (MkAnyWitness ta) = MkAnyWitness1 (ApplyOpenRep1 tf ta);
+-}
 }
diff --git a/Data/OpenWitness/Typeable/Rep.hs b/Data/OpenWitness/Typeable/Rep.hs
deleted file mode 100644
--- a/Data/OpenWitness/Typeable/Rep.hs
+++ /dev/null
@@ -1,62 +0,0 @@
-module Data.OpenWitness.Typeable.Rep where
-{
-	import Data.Witness;
-	import Data.OpenWitness;
-	import Data.Maybe;
-
-	data Rep2 p where
-	{
-		SimpleRep2 :: IOWitness (p () ()) -> Rep2 p;
---		ApplyRep2 :: TypeRep3 p -> Rep a -> Rep2 (p a);
-	};
-
-	matchRep2 :: Rep2 a -> Rep2 b -> Maybe (EqualType (a () ()) (b () ()));
-	matchRep2 (SimpleRep2 wa) (SimpleRep2 wb) = matchWitness wa wb;
-{-
-	matchRep2 (ApplyRep1 tfa ta) (ApplyRep1 tfb tb) = do
-	{
-		MkEqualType <- matchRep2 tfa tfb;
-		MkEqualType <- matchWitness ta tb;
-		return MkEqualType;
-	};
-	matchRep2 _ _ = Nothing;
--}
-	data Rep1 p where
-	{
-		SimpleRep1 :: IOWitness (p ()) -> Rep1 p;
-		ApplyRep1 :: Rep2 p -> Rep a -> Rep1 (p a);
-	};
-
-	matchRep1 :: Rep1 a -> Rep1 b -> Maybe (EqualType (a ()) (b ()));
-	matchRep1 (SimpleRep1 wa) (SimpleRep1 wb) = matchWitness wa wb;
-	matchRep1 (ApplyRep1 tfa ta) (ApplyRep1 tfb tb) = do
-	{
-		MkEqualType <- matchRep2 tfa tfb;
-		MkEqualType <- matchWitness ta tb;
-		return MkEqualType;
-	};
-	matchRep1 _ _ = Nothing;
-
-	data Rep a where
-	{
-		SimpleRep :: IOWitness a -> Rep a;
-		ApplyRep :: Rep1 p -> Rep a -> Rep (p a);
-	};
-
-	instance SimpleWitness Rep where
-	{
-		matchWitness (SimpleRep wa) (SimpleRep wb) = matchWitness wa wb;
-		matchWitness (ApplyRep tfa ta) (ApplyRep tfb tb) = do
-		{
-			MkEqualType <- matchRep1 tfa tfb;
-			MkEqualType <- matchWitness ta tb;
-			return MkEqualType;
-		};
-		matchWitness _ _ = Nothing;
-	};
-
-	instance Eq1 Rep where
-	{
-		equals1 r1 r2 = isJust (matchWitness r1 r2);
-	};
-}
diff --git a/open-witness.cabal b/open-witness.cabal
--- a/open-witness.cabal
+++ b/open-witness.cabal
@@ -1,32 +1,49 @@
-name:			open-witness
-version:		0.1.1
-license:		BSD3
-license-file:	LICENSE
-author:			Ashley Yakeley <ashley@semantic.org>
-maintainer:		Ashley Yakeley <ashley@semantic.org>
-build-depends:	base>=2.0, mtl>=1.1, witness==0.1
-category:		Data
-synopsis:		open witnesses
+cabal-version:  >=1.14
+name:           open-witness
+version:        0.3.1
+x-follows-version-policy:
+license:        BSD3
+license-file:   LICENSE
+copyright:      Ashley Yakeley <ashley@semantic.org>
+author:         Ashley Yakeley <ashley@semantic.org>
+maintainer:     Ashley Yakeley <ashley@semantic.org>
+homepage:       https://github.com/AshleyYakeley/open-witness
+bug-reports:    https://github.com/AshleyYakeley/open-witness/issues
+synopsis:       open witnesses
 description:
-	Open witnesses are witnesses that can witness to any type. However, they cannot be constructed, they can only be generated in the IO monad.
+    Open witnesses are witnesses that can witness to any type. However, they cannot be constructed, they can only be generated in the IO monad.
+    See the paper /Witnesses and Open Witnesses/ (<http://semantic.org/stuff/Open-Witnesses.pdf>).
+category:       Data
+build-type:     Simple
 
-	See the paper /Witnesses and Open Witnesses/ (<http://semantic.org/stuff/Open-Witnesses.pdf>).
-build-type:		Simple
-extensions:
-	RankNTypes
-	EmptyDataDecls
-	GeneralizedNewtypeDeriving
-	ScopedTypeVariables
-	GADTs
-	PatternSignatures
-	FlexibleContexts
-	FlexibleInstances
-	MultiParamTypeClasses
-exposed-modules:
-	Data.OpenWitness
-	Data.OpenWitness.ST
-	Data.OpenWitness.Typeable
-	Data.OpenWitness.Typeable.Rep
-	Data.OpenWitness.Dynamic
-	Data.OpenWitness.Exception
-other-modules:
+library
+    hs-source-dirs: .
+    default-language: Haskell2010
+    default-extensions:
+        MultiParamTypeClasses
+        RankNTypes
+        FlexibleContexts
+        TypeOperators
+        FlexibleInstances
+        EmptyDataDecls
+        KindSignatures
+        TemplateHaskell
+        GeneralizedNewtypeDeriving
+        GADTs
+        PolyKinds
+        ScopedTypeVariables
+    build-depends:
+        base >= 4.8 && < 5,
+        random,
+        template-haskell,
+        transformers,
+        hashable,
+        witness >= 0.3
+    exposed-modules:
+        Data.OpenWitness
+        Data.OpenWitness.Dynamic
+        Data.OpenWitness.Exception
+        Data.OpenWitness.OpenRep
+        Data.OpenWitness.ST
+        Data.OpenWitness.Typeable
+    ghc-options: -Wall