diff --git a/Data/OpenWitness.hs b/Data/OpenWitness.hs
deleted file mode 100644
--- a/Data/OpenWitness.hs
+++ /dev/null
@@ -1,134 +0,0 @@
-{-# OPTIONS -fno-warn-name-shadowing #-}
-module Data.OpenWitness
-(
-    OpenWitness,
-    RealWorld,IOWitness,newIOWitness,
-    OW,newOpenWitnessOW,runOW,owToIO,
---    unsafeIOWitnessFromInteger,
---    unsafeIOWitnessFromString,
-    iowitness
-) where
-{
-    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 :: a :~: b;
-    unsafeSameType = unsafeCoerce Refl;
-
-    -- | 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;
-
-    instance TestEquality (OpenWitness s) where
-    {
-        testEquality (MkOpenWitness ua) (MkOpenWitness ub) =
-            if ua == ub then Just unsafeSameType else Nothing;
-    };
-
-    -- | The @s@ type for running 'OW' in 'IO'.
-    ;
-    data RealWorld;
-
-    -- | 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
deleted file mode 100644
--- a/Data/OpenWitness/Dynamic.hs
+++ /dev/null
@@ -1,56 +0,0 @@
--- | This is an approximate re-implementation of "Data.Dynamic" using open witnesses.
-module Data.OpenWitness.Dynamic where
-{
-{-
-    import Data.Witness;
-    import Data.OpenWitness.OpenRep;
-    import Data.OpenWitness.Typeable;
-
-    -- * The @Dynamic@ type
-    ;
-
-    type Dynamic = Any OpenRep;
-
-    -- * Converting to and from @Dynamic@
-    ;
-
-    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;
-    };
-
-    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
-    ;
-
-    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";
-    };
-
-    dynTypeRep :: Dynamic -> TypeRep;
-    dynTypeRep (MkAny r _) = MkAnyWitness r;
--}
-}
diff --git a/Data/OpenWitness/Exception.hs b/Data/OpenWitness/Exception.hs
deleted file mode 100644
--- a/Data/OpenWitness/Exception.hs
+++ /dev/null
@@ -1,48 +0,0 @@
-{-# LANGUAGE DeriveDataTypeable #-}
-{-# OPTIONS -fno-warn-unused-matches #-}
-module Data.OpenWitness.Exception
-(
-    Exn, declexn, throw, catch
-) where
-{
-    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.
-    ;
-    newtype Exn (e :: *) = MkExn (IOWitness e);
-
-    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
deleted file mode 100644
--- a/Data/OpenWitness/OpenRep.hs
+++ /dev/null
@@ -1,70 +0,0 @@
-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
deleted file mode 100644
--- a/Data/OpenWitness/ST.hs
+++ /dev/null
@@ -1,59 +0,0 @@
--- | 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
-) where
-{
-    import Data.OpenWitness;
-    import Data.Witness.WitnessDict;
-    import Control.Monad.Trans.State;
-    import Control.Monad.Trans.Class;
-    import Control.Monad.Fix;
-
-    type ST s = StateT (WitnessDict (OpenWitness s)) (OW s);
-
-    stToOW :: ST s a -> OW s a;
-    stToOW st = evalStateT st emptyWitnessDict;
-
-    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
deleted file mode 100644
--- a/Data/OpenWitness/Typeable.hs
+++ /dev/null
@@ -1,102 +0,0 @@
--- | This is an approximate re-implementation of "Data.Typeable" using open witnesses.
-module Data.OpenWitness.Typeable where
-{
-{-
-    import Data.OpenWitness.OpenRep;
-    import Data.OpenWitness;
-    import Data.Witness;
-
-    -- | types of kind @*@ with a representation
-    ;
-    class Typeable a where
-    {
-        rep :: OpenRep a;
-    };
-
-    -- | types of kind @* -> *@ with a representation
-    ;
-    class Typeable1 t where
-    {
-        rep1 :: OpenRep1 t;
-    };
-
-    -- | types of kind @* -> * -> *@ with a representation
-    ;
-    class Typeable2 t where
-    {
-        rep2 :: OpenRep2 t;
-    };
-
-    instance (Typeable1 f,Typeable a) => Typeable (f a) where
-    {
-        rep = ApplyOpenRep rep1 rep;
-    };
-
-    instance (Typeable2 f,Typeable a) => Typeable1 (f a) where
-    {
-        rep1 = ApplyOpenRep1 rep2 rep;
-    };
-
-    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 <- 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 <- testEquality rep rep;
-        return ca;
-    };
-
-    -- | represents a type of kind @*@
-    ;
-    type TypeRep = AnyWitness OpenRep;
-
-    typeOf :: forall t. (Typeable t) => t -> TypeRep;
-    typeOf _ = MkAnyWitness (rep :: OpenRep t);
-
-    -- | represents a type of kind @* -> *@
-    ;
-    type TypeRep1 = AnyWitness1 OpenRep1;
-
-    typeOf1 :: forall t a. (Typeable1 t) => t a -> TypeRep1;
-    typeOf1 _ = MkAnyWitness1 (rep1 :: OpenRep1 t);
-
-    -- | 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/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-open-witness is Copyright (c) Ashley Yakeley, 2007-2008.
+open-witness is Copyright (c) Ashley Yakeley, 2007-2017.
 All rights reserved.
 
 Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
diff --git a/open-witness.cabal b/open-witness.cabal
--- a/open-witness.cabal
+++ b/open-witness.cabal
@@ -1,6 +1,6 @@
 cabal-version:  >=1.14
 name:           open-witness
-version:        0.3.1
+version:        0.4
 x-follows-version-policy:
 license:        BSD3
 license-file:   LICENSE
@@ -17,7 +17,7 @@
 build-type:     Simple
 
 library
-    hs-source-dirs: .
+    hs-source-dirs: src
     default-language: Haskell2010
     default-extensions:
         MultiParamTypeClasses
@@ -30,20 +30,49 @@
         TemplateHaskell
         GeneralizedNewtypeDeriving
         GADTs
-        PolyKinds
         ScopedTypeVariables
+        TypeInType
+        ConstraintKinds
+        UndecidableInstances
     build-depends:
-        base >= 4.8 && < 5,
+        base >= 4.9.1 && < 5,
         random,
         template-haskell,
         transformers,
         hashable,
-        witness >= 0.3
+        constraints,
+        witness == 0.4
     exposed-modules:
+        Data.Type.Heterogeneous
         Data.OpenWitness
+        Data.OpenWitness.TypeRep
+        Data.OpenWitness.Typeable
         Data.OpenWitness.Dynamic
         Data.OpenWitness.Exception
-        Data.OpenWitness.OpenRep
         Data.OpenWitness.ST
-        Data.OpenWitness.Typeable
+        Data.OpenWitness.Instance
     ghc-options: -Wall
+
+test-suite tests
+    type: exitcode-stdio-1.0
+    hs-source-dirs: test
+    default-language: Haskell2010
+    default-extensions:
+        RankNTypes
+        EmptyDataDecls
+        GeneralizedNewtypeDeriving
+        ScopedTypeVariables
+        GADTs
+        FlexibleContexts
+        MultiParamTypeClasses
+        TemplateHaskell
+    build-depends:
+        base,
+        mtl,
+        witness,
+        open-witness,
+        tasty,
+        tasty-hunit
+    main-is: Main.hs
+    other-modules:
+        Object
diff --git a/src/Data/OpenWitness.hs b/src/Data/OpenWitness.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/OpenWitness.hs
@@ -0,0 +1,144 @@
+{-# OPTIONS -fno-warn-name-shadowing #-}
+module Data.OpenWitness
+(
+    OpenWitness,
+    RealWorld,IOWitness,newIOWitness,
+    OW,newOpenWitnessOW,runOW,owToIO,
+--    unsafeIOWitnessFromInteger,
+--    unsafeIOWitnessFromString,
+    iowitness
+) where
+{
+    import Prelude;
+    import Data.Kind;
+    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;
+    import Data.Type.Heterogeneous;
+
+
+    unsafeSameType :: HetEq a b;
+    unsafeSameType = unsafeCoerce ReflH;
+
+    -- | 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 :: * -> forall (k :: *). k -> * where
+    {
+        MkOpenWitness :: Integer -> OpenWitness s a;
+    } deriving Eq;
+
+    instance TestHetEquality (OpenWitness s) where
+    {
+        testHetEquality (MkOpenWitness ua) (MkOpenWitness ub) =
+            if ua == ub then Just unsafeSameType else Nothing;
+    };
+
+    instance TestEquality (OpenWitness s) where
+    {
+        testEquality wa wb = fmap homoHetEq $ testHetEquality wa wb;
+    };
+
+    -- | The @s@ type for running 'OW' in 'IO'.
+    ;
+    data RealWorld;
+
+    -- | 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/src/Data/OpenWitness/Dynamic.hs b/src/Data/OpenWitness/Dynamic.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/OpenWitness/Dynamic.hs
@@ -0,0 +1,56 @@
+-- | This is an approximate re-implementation of "Data.Dynamic" using open witnesses.
+module Data.OpenWitness.Dynamic where
+{
+    import Data.Kind;
+    import Data.Witness;
+    import Data.Type.Heterogeneous;
+    import Data.OpenWitness.TypeRep;
+    import Data.OpenWitness.Typeable;
+
+    -- * The @Dynamic@ type
+    ;
+
+    type Dynamic = Any TypeRep;
+
+    -- * Converting to and from @Dynamic@
+    ;
+
+    toDyn :: forall (a :: *). Typeable a => a -> Dynamic;
+    toDyn = MkAny typeRep;
+
+    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
+    {
+        Refl <- testEquality uq (typeRep :: TypeRep a);
+        return a;
+    };
+
+    -- * Applying functions of dynamic type
+    ;
+
+    dynApply :: Dynamic -> Dynamic -> Maybe Dynamic;
+    dynApply (MkAny (ApplyTypeRep (ApplyTypeRep repFn' rx') ry) f) (MkAny rx x) = do
+    {
+        ReflH <- testHetEquality repFn' (typeRep :: TypeRep (->));
+        ReflH <- testHetEquality 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";
+    };
+
+    dynTypeRep :: Dynamic -> AnyWitness (TypeRep :: * -> *);
+    dynTypeRep (MkAny r _) = MkAnyWitness r;
+}
diff --git a/src/Data/OpenWitness/Exception.hs b/src/Data/OpenWitness/Exception.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/OpenWitness/Exception.hs
@@ -0,0 +1,49 @@
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# OPTIONS -fno-warn-unused-matches #-}
+module Data.OpenWitness.Exception
+(
+    Exn, declexn, throw, catch
+) where
+{
+    import Data.Kind;
+    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.
+    ;
+    newtype Exn (e :: *) = MkExn (IOWitness e);
+
+    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/src/Data/OpenWitness/Instance.hs b/src/Data/OpenWitness/Instance.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/OpenWitness/Instance.hs
@@ -0,0 +1,17 @@
+module Data.OpenWitness.Instance where
+{
+    import Data.Kind;
+    import Data.Constraint;
+    import Data.Type.Heterogeneous;
+    import Data.OpenWitness.TypeRep;
+
+    data Instance = forall (t :: Constraint). t => MkInstance (TypeRep t);
+
+    findInstance :: [Instance] -> TypeRep t -> Maybe (Dict t);
+    findInstance [] _ = Nothing;
+    findInstance (MkInstance ti:ii) t = case testHetEquality ti t of
+    {
+        Just ReflH -> Just Dict;
+        Nothing -> findInstance ii t;
+    };
+}
diff --git a/src/Data/OpenWitness/ST.hs b/src/Data/OpenWitness/ST.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/OpenWitness/ST.hs
@@ -0,0 +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
+) where
+{
+    import Data.OpenWitness;
+    import Data.Witness.WitnessDict;
+    import Control.Monad.Trans.State;
+    import Control.Monad.Trans.Class;
+    import Control.Monad.Fix;
+
+    type ST s = StateT (WitnessDict (OpenWitness s)) (OW s);
+
+    stToOW :: ST s a -> OW s a;
+    stToOW st = evalStateT st emptyWitnessDict;
+
+    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/src/Data/OpenWitness/TypeRep.hs b/src/Data/OpenWitness/TypeRep.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/OpenWitness/TypeRep.hs
@@ -0,0 +1,36 @@
+module Data.OpenWitness.TypeRep where
+{
+    import Data.Kind;
+    import Data.Maybe;
+    import Data.Witness;
+    import Data.OpenWitness;
+    import Data.Type.Heterogeneous;
+
+    data TypeRep :: forall (k :: *). k -> * where
+    {
+        SimpleTypeRep :: forall (k :: *) (a :: k). IOWitness a -> TypeRep a;
+        ApplyTypeRep :: forall (k1 :: *) (k2 :: *) (p :: k1 -> k2) (a :: k1). TypeRep p -> TypeRep a -> TypeRep (p a);
+    };
+
+    instance TestHetEquality TypeRep where
+    {
+        testHetEquality (SimpleTypeRep wa) (SimpleTypeRep wb) = testHetEquality wa wb;
+        testHetEquality (ApplyTypeRep tfa ta) (ApplyTypeRep tfb tb) = do
+        {
+            ReflH <- testHetEquality tfa tfb;
+            ReflH <- testHetEquality ta tb;
+            return ReflH;
+        };
+        testHetEquality _ _ = Nothing;
+    };
+
+    instance TestEquality TypeRep where
+    {
+        testEquality wa wb = fmap homoHetEq $ testHetEquality wa wb;
+    };
+
+    instance Eq1 TypeRep where
+    {
+        equals1 r1 r2 = isJust (testHetEquality r1 r2);
+    };
+}
diff --git a/src/Data/OpenWitness/Typeable.hs b/src/Data/OpenWitness/Typeable.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/OpenWitness/Typeable.hs
@@ -0,0 +1,120 @@
+-- | This is an approximate re-implementation of "Data.Typeable" using open witnesses.
+module Data.OpenWitness.Typeable where
+{
+    import Data.Kind;
+    import Data.OpenWitness.TypeRep;
+    import Data.OpenWitness;
+    import Data.Witness;
+
+    -- | types of kind @*@ with a representation
+    ;
+    class Typeable (a :: k) where
+    {
+        typeRep :: TypeRep a;
+    };
+
+    instance (Typeable (f :: k1 -> k2),Typeable (a :: k1)) => Typeable (f a) where
+    {
+        typeRep = ApplyTypeRep typeRep typeRep;
+    };
+
+    instance Typeable Type where
+    {
+        typeRep = SimpleTypeRep $(iowitness [t|Type|]);
+    };
+
+    type Fun = (->);
+
+    instance Typeable (->) where
+    {
+        typeRep = SimpleTypeRep $(iowitness [t|Fun|]);
+    };
+
+    instance Typeable Constraint where
+    {
+        typeRep = SimpleTypeRep $(iowitness [t|Constraint|]);
+    };
+
+    instance Typeable TypeRep where
+    {
+        typeRep = SimpleTypeRep $(iowitness [t|TypeRep|]);
+    };
+
+    instance Typeable Typeable where
+    {
+        typeRep = SimpleTypeRep $(iowitness [t|Typeable|]);
+    };
+
+    instance Typeable () where
+    {
+        typeRep = SimpleTypeRep $(iowitness [t|()|]);
+    };
+
+    instance Typeable (,) where
+    {
+        typeRep = SimpleTypeRep $(iowitness [t|(,)|]);
+    };
+
+    instance Typeable Either where
+    {
+        typeRep = SimpleTypeRep $(iowitness [t|Either|]);
+    };
+
+    instance Typeable Maybe where
+    {
+        typeRep = SimpleTypeRep $(iowitness [t|Maybe|]);
+    };
+
+    instance Typeable [] where
+    {
+        typeRep = SimpleTypeRep $(iowitness [t|[]|]);
+    };
+
+    instance Typeable Bool where
+    {
+        typeRep = SimpleTypeRep $(iowitness [t|Bool|]);
+    };
+
+    instance Typeable Char where
+    {
+        typeRep = SimpleTypeRep $(iowitness [t|Char|]);
+    };
+
+    instance Typeable Int where
+    {
+        typeRep = SimpleTypeRep $(iowitness [t|Int|]);
+    };
+
+    cast :: forall (a :: *) (b :: *). (Typeable a,Typeable b) => a -> Maybe b;
+    cast a = do
+    {
+        Refl :: a :~: b <- testEquality typeRep typeRep;
+        return a;
+    };
+
+    gcast :: forall (k :: *) (a :: k) (b :: k) (c :: k -> *). (Typeable a,Typeable b) => c a -> Maybe (c b);
+    gcast ca = do
+    {
+        Refl :: a :~: b <- testEquality typeRep typeRep;
+        return ca;
+    };
+
+    -- | given representations of @a@ and @b@, make a representation of @a -> b@
+    ;
+    mkFunTy :: TypeRep a -> TypeRep b -> TypeRep (a -> b);
+    mkFunTy ta tb = ApplyTypeRep (ApplyTypeRep (typeRep :: TypeRep (->)) ta) tb;
+
+    -- | given representations of @a -> b@ and @a@, make a representation of @b@ (otherwise not)
+    ;
+    funResultTy :: TypeRep (a -> b) -> TypeRep a -> Maybe (TypeRep b);
+    funResultTy (ApplyTypeRep (ApplyTypeRep repFn' ta') tb') ta = do
+    {
+        Refl <- testEquality repFn' (typeRep :: TypeRep (->));
+        Refl <- testEquality ta' ta;
+        return tb';
+    };
+    funResultTy _ _ = Nothing;
+
+    mkAppTy :: forall (k1 :: *) (k2 :: *) (f :: k1 -> k2) (a :: k1). TypeRep f -> TypeRep a -> TypeRep (f a);
+    mkAppTy = ApplyTypeRep;
+}
diff --git a/src/Data/Type/Heterogeneous.hs b/src/Data/Type/Heterogeneous.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Heterogeneous.hs
@@ -0,0 +1,20 @@
+module Data.Type.Heterogeneous where
+{
+    import Data.Kind;
+    import Data.Type.Equality;
+
+    data HetEq (a :: ka) (b :: kb) where
+    {
+        ReflH :: forall (k :: *) (t :: k). HetEq t t;
+    };
+
+    -- | somewhat awkwardly named
+    ;
+    homoHetEq :: forall (k :: *) (a :: k) (b :: k). HetEq a b -> a :~: b;
+    homoHetEq ReflH = Refl;
+
+    class TestHetEquality (w :: forall k. k -> *) where
+    {
+        testHetEquality :: forall (ka :: *) (a :: ka) (kb :: *) (b :: kb). w a -> w b -> Maybe (HetEq a b);
+    };
+}
diff --git a/test/Main.hs b/test/Main.hs
new file mode 100644
--- /dev/null
+++ b/test/Main.hs
@@ -0,0 +1,63 @@
+{-# LANGUAGE TemplateHaskell #-}
+module Main where
+{
+    import Data.OpenWitness.ST;
+    import Data.OpenWitness.Exception;
+    import Prelude;
+    import Test.Tasty;
+    import Test.Tasty.HUnit;
+
+    stuff :: ST s [Int];
+    stuff = do
+    {
+        ra <- newSTRef 3;
+        a1 <- readSTRef ra;
+        rb <- newSTRef 4;
+        b1 <- readSTRef rb;
+        writeSTRef ra 5;
+        a2 <- readSTRef ra;
+        writeSTRef rb 7;
+        b2 <- readSTRef rb;
+        return [a1,b1,a2,b2];
+    };
+
+    testST :: TestTree;
+    testST = testCase "ST" $ assertEqual "vals" [3,4,5,7] $ runST stuff;
+
+    intExn :: Exn Int;
+    intExn = $(declexn [t|Int|]);
+    stringExn :: Exn String;
+    stringExn = $(declexn [t|String|]);
+
+    data Caught = NotCaught | IntCaught Int | StringCaught String deriving (Eq,Show);
+
+    getCaught :: IO a -> IO Caught;
+    getCaught f = ((do
+    {
+        _ <- f;
+        return NotCaught;
+    }
+    `catch` intExn) (\x -> return (IntCaught x))
+    `catch` stringExn) (\x -> return (StringCaught x));
+
+    testCaught :: String -> Caught -> IO a -> TestTree;
+    testCaught name expected f = testCase name $ do
+    {
+        result <- getCaught f;
+        assertEqual "caught" expected result;
+    };
+
+    tests :: TestTree;
+    tests = testGroup "test"
+    [
+        testST,
+        testCaught "return" NotCaught $ return "hello",
+        testCaught "throw intExn 3" (IntCaught 3) $ throw intExn 3,
+        testCaught "throw stringExn text" (StringCaught "text") $ throw stringExn "text",
+        testCaught "throw intExn 67" (IntCaught 67) $ throw intExn 67,
+        testCaught "throw stringExn str" (StringCaught "str") $ throw stringExn "str"
+    ];
+
+    main :: IO ();
+    main = defaultMain tests;
+}
diff --git a/test/Object.hs b/test/Object.hs
new file mode 100644
--- /dev/null
+++ b/test/Object.hs
@@ -0,0 +1,24 @@
+module Object where
+{
+	import Data.Witness;
+	import Data.OpenWitness;
+
+	data Object s = forall a. MkObject (OpenWitness s a) a;
+
+	matchObject :: OpenWitness s b -> Object s -> Maybe b;
+	matchObject uqb (MkObject uqa a) = do
+	{
+		MkEqualType <- testEquality uqa uqb;
+		return a;
+	};
+
+	makeConversions :: OpenWitness s b -> (b -> Object s,Object s -> Maybe b);
+	makeConversions wit = (MkObject wit,matchObject wit);
+
+	getConversions :: OW s (b -> Object s,Object s -> Maybe b);
+	getConversions = do
+	{
+		wit <- newOpenWitnessOW;
+		return (makeConversions wit);
+	};
+}