diff --git a/Data/Witness.hs b/Data/Witness.hs
deleted file mode 100644
--- a/Data/Witness.hs
+++ /dev/null
@@ -1,33 +0,0 @@
-module Data.Witness
-(
-	module Data.Witness.WitnessDict,
-	module Data.Witness.WitnessFDict,
-	module Data.Witness.Any,
-	module Data.Witness.Representative,
-	module Data.Witness.Type,
-	module Data.Witness.SimpleWitness,
-	module Data.Witness.EqualType,
-	module Data.Witness.Nat,
-	module Data.Witness.List,
-	module Data.Witness
-) where
-{
-	import Data.Witness.List;
-	import Data.Witness.Nat;
-	import Data.Witness.EqualType;
-	import Data.Witness.SimpleWitness;
-	import Data.Witness.Type;
-	import Data.Witness.Representative;
-	import Data.Witness.Any;
-	import Data.Witness.WitnessFDict;
-	import Data.Witness.WitnessDict;
-
-	-- | See whether two represented and witnessed types are the same.
-	;
-	matchIs :: (SimpleWitness w,Is w a,Is w b) => Type (w ()) -> Maybe (EqualType a b);
-	matchIs t = matchWitness (foo t) (foo t) where
-	{
-		foo :: (Is w a) => Type (w ()) -> w a;
-		foo _ = representative;
-	};
-}
diff --git a/Data/Witness/Any.hs b/Data/Witness/Any.hs
deleted file mode 100644
--- a/Data/Witness/Any.hs
+++ /dev/null
@@ -1,56 +0,0 @@
-module Data.Witness.Any where
-{
-	import Data.Witness.SimpleWitness;
-	import Data.Witness.EqualType;
-	import Data.Maybe;
-
-	-- | Any value with a witness to it.
-	;
-	data Any w = forall a. MkAny (w a) a;
-	
-	matchAny :: (SimpleWitness w) => w a -> Any w -> Maybe a;
-	matchAny wit (MkAny cwit ca) = do
-	{
-		MkEqualType <- matchWitness cwit wit;
-		return ca;
-	};
-
-	-- | Any value with a witness to a parameter of its type.
-	;
-	data AnyF w f = forall a. MkAnyF (w a) (f a);
-	
-	matchAnyF :: (SimpleWitness w) => w a -> AnyF w f -> Maybe (f a);
-	matchAnyF wit (MkAnyF cwit cfa) = do
-	{
-		MkEqualType <- matchWitness cwit wit;
-		return cfa;
-	};
-
-	-- | Any value with a witness to a parameter of its type of kind @* -> *@.
-	;
-	data AnyF1 w f = forall (a :: * -> *). MkAnyF1 (w a) (f a);
-
-	-- | Any value with a witness to a parameter of its type of kind @* -> * -> *@.
-	;
-	data AnyF2 w f = forall (a :: * -> * -> *). MkAnyF2 (w a) (f a);
-
-	-- | Any witness.
-	;
-	data AnyWitness w = forall a. MkAnyWitness (w a);
-	
-	matchAnyWitness :: (SimpleWitness w) => w a -> AnyWitness w -> Bool;
-	matchAnyWitness wit (MkAnyWitness cwit) = isJust (matchWitness cwit wit);
-
-	instance (SimpleWitness w) => Eq (AnyWitness w) where
-	{
-		(==) (MkAnyWitness wa) = matchAnyWitness wa;
-	};
-
-	-- | Any witness of a type of kind @* -> *@.
-	;
-	data AnyWitness1 w = forall (a :: * -> *). MkAnyWitness1 (w a);
-
-	-- | Any witness of a type of kind @* -> * -> *@.
-	;
-	data AnyWitness2 w = forall (a :: * -> * -> *). MkAnyWitness2 (w a);
-}
diff --git a/Data/Witness/EqualType.hs b/Data/Witness/EqualType.hs
deleted file mode 100644
--- a/Data/Witness/EqualType.hs
+++ /dev/null
@@ -1,17 +0,0 @@
-module Data.Witness.EqualType where
-{
-	import Control.Category;
-
-	-- | witness that type parameters @a@ and @b@ are the same type
-	;
-	data EqualType a b where
-	{
-		MkEqualType :: EqualType t t;
-	};
-
-	instance Category EqualType where
-	{
-		id = MkEqualType;
-		MkEqualType . MkEqualType = MkEqualType;
-	};
-}
diff --git a/Data/Witness/List.hs b/Data/Witness/List.hs
deleted file mode 100644
--- a/Data/Witness/List.hs
+++ /dev/null
@@ -1,86 +0,0 @@
-module Data.Witness.List where
-{
-	import Data.Witness.Nat;
-	import Data.Witness.Representative;
-	import Data.Witness.SimpleWitness;
-	import Data.Witness.EqualType;
-	import Control.Category;
-	import Prelude hiding (id,(.));
-
-	-- | a witness type for HList-style lists. Here we use @()@ and @(,)@ for @HNil@ and @HCons@. 
-	-- The @w@ parameter is the witness type of the elements.
-	;
-	data ListType w a where
-	{
-		NilListType :: ListType w ();
-		ConsListType :: w a -> ListType w b -> ListType w (a,b);
-	};
-
-	instance Eq1 w => Eq1 (ListType w) where
-	{
-		equals1 NilListType NilListType = True;
-		equals1 (ConsListType pe pl) (ConsListType qe ql) = (equals1 pe qe) && (equals1 pl ql);
-		equals1 _ _ = False;
-	};
-
-	instance Eq1 w => Eq (ListType w a) where
-	{
-		(==) = equals1;
-	};
-
-	instance (Representative w) => Representative (ListType w) where
-	{
-		getRepWitness NilListType = MkRepWitness;
-		getRepWitness (ConsListType w lw) = case (getRepWitness w,getRepWitness lw) of
-		{
-			(MkRepWitness,MkRepWitness) -> MkRepWitness;
-		};
-	};
-
-	instance (Representative w) => Is (ListType w) () where
-	{
-		representative = NilListType;
-	};
-
-	instance (Is w a,Is (ListType w) b) => Is (ListType w) (a,b) where
-	{
-		representative = ConsListType representative representative;
-	};
-
-	instance (SimpleWitness w) => SimpleWitness (ListType w) where
-	{
-		matchWitness NilListType NilListType = Just id;
-		matchWitness (ConsListType wpa wpb) (ConsListType wqa wqb) = do
-		{
-			MkEqualType <- matchWitness wpa wqa;
-			MkEqualType <- matchWitness wpb wqb;
-			return MkEqualType;
-		};
-		matchWitness _ _ = Nothing;
-	};
-
-
-    class HasListElement n list where
-    {
-        type ListElement n list :: *;
-        getListElement :: Nat n -> list -> ListElement n list;
-        putListElement :: Nat n -> ListElement n list -> list -> list;
-    };
-
-    modifyListElement :: (HasListElement n t) => Nat n -> (ListElement n t -> ListElement n t) -> t -> t;
-    modifyListElement n aa t = putListElement n (aa (getListElement n t)) t;
-
-    instance HasListElement Zero (a,r) where
-    {
-        type ListElement Zero (a,r) = a;
-        getListElement _ (a,_) = a;
-        putListElement _ a (_,r) = (a,r);
-    };
-
-    instance (HasListElement n r) => HasListElement (Succ n) (a,r) where
-    {
-        type ListElement (Succ n) (a,r) = ListElement n r;
-        getListElement (SuccNat n) (_,r) = getListElement n r;
-        putListElement (SuccNat n) a (f,r) = (f,putListElement n a r);
-    };
-}
diff --git a/Data/Witness/Nat.hs b/Data/Witness/Nat.hs
deleted file mode 100644
--- a/Data/Witness/Nat.hs
+++ /dev/null
@@ -1,53 +0,0 @@
-module Data.Witness.Nat where
-{
-	import Data.Witness.Representative;
-	import Data.Witness.SimpleWitness;
-	import Data.Witness.EqualType;
-	import Data.Maybe;
-	import Prelude hiding (id,(.));
-
-    data Zero;
-    
-    data Succ n;
-    
-    data Nat t where
-    {
-        ZeroNat :: Nat Zero;
-        SuccNat :: Nat t -> Nat (Succ t);
-    };
-
-    instance SimpleWitness Nat where
-    {
-        matchWitness ZeroNat ZeroNat = return MkEqualType;
-        matchWitness (SuccNat a) (SuccNat b) = do
-        {
-            MkEqualType <- matchWitness a b;
-            return MkEqualType;
-        };
-        matchWitness _ _ = Nothing;
-    };
-
-    instance Eq1 Nat where
-    {
-        equals1 a b = isJust (matchWitness a b);
-    };
-
-    instance Representative Nat where
-    {
-        getRepWitness ZeroNat = MkRepWitness;
-        getRepWitness (SuccNat n) = case getRepWitness n of
-        {
-            MkRepWitness -> MkRepWitness;
-        };
-    };
-
-    instance Is Nat Zero where
-    {
-        representative = ZeroNat;
-    };
-
-    instance (Is Nat n) => Is Nat (Succ n) where
-    {
-        representative = SuccNat representative;
-    };
-}
diff --git a/Data/Witness/Representative.hs b/Data/Witness/Representative.hs
deleted file mode 100644
--- a/Data/Witness/Representative.hs
+++ /dev/null
@@ -1,72 +0,0 @@
-module Data.Witness.Representative where
-{
-	import Data.Witness.Any;
-	import Data.Witness.SimpleWitness;
-
-	class Eq1 p where
-	{
-		equals1 :: forall a. p a -> p a -> Bool;
-	};
-
-	data RepWitness rep a where
-	{
-		MkRepWitness :: (Is rep a) => RepWitness rep a;
-	};
-
-	isWitnessRepresentative :: RepWitness rep a -> rep a;
-	isWitnessRepresentative MkRepWitness = representative;
-
-	instance (SimpleWitness w) => SimpleWitness (RepWitness w) where
-	{
-		matchWitness wa wb = matchWitness (isWitnessRepresentative wa) (isWitnessRepresentative wb);
-	};
-
-	class Eq1 rep => Representative rep where
-	{
-		-- | Every value is an instance of 'Is'.
-		;
-		getRepWitness :: rep a -> RepWitness rep a;
-	};
-
-	withRepresentative :: forall rep r. (Representative rep) => (forall a. (Is rep a) => rep a -> r) -> (forall b. rep b -> r);
-	withRepresentative foo rep = case getRepWitness rep of
-	{
-		MkRepWitness -> foo rep;
-	};
-
-	-- | If two representatives have the same type, then they have the same value.
-	;
-	class Representative rep => Is rep a where
-	{
-		-- | The representative value for type @a@.
-		;
-		representative :: rep a;
-	};
-
-	getRepresentative :: (Is rep a) => a -> rep a;
-	getRepresentative _ = representative;
-
-	rerepresentative :: (Is rep a) => p a -> rep a;
-	rerepresentative _ = representative;
-
-	mkAny :: (Is rep a) => a -> Any rep;
-	mkAny a = MkAny representative a;
-
-	mkAnyF :: (Is rep a) => f a -> AnyF rep f;
-	mkAnyF fa = MkAnyF representative fa;
-
-	instance Eq1 (RepWitness rep) where
-	{
-		equals1 MkRepWitness MkRepWitness = True;
-	};
-
-	instance Representative (RepWitness rep) where
-	{
-		getRepWitness MkRepWitness = MkRepWitness;
-	};
-
-	instance (Is rep a) => Is (RepWitness rep) a where
-	{
-		representative = MkRepWitness;
-	};
-}
diff --git a/Data/Witness/SimpleWitness.hs b/Data/Witness/SimpleWitness.hs
deleted file mode 100644
--- a/Data/Witness/SimpleWitness.hs
+++ /dev/null
@@ -1,15 +0,0 @@
-module Data.Witness.SimpleWitness where
-{
-	import Data.Witness.EqualType;
-
-	-- | @w@ is a simple witness type if each value witnesses to a single type. Thus if two values are the same, then they have the same type.
-	;
-	class SimpleWitness w where
-	{
-		-- | If the two values are the same, then @a@ and @b@ are the same type.
-		--
-		-- As an equivalence relation, 'matchWitness' must be reflexive, commutative, and transitive.
-		;
-		matchWitness :: w a -> w b -> Maybe (EqualType a b);
-	};
-}
diff --git a/Data/Witness/Type.hs b/Data/Witness/Type.hs
deleted file mode 100644
--- a/Data/Witness/Type.hs
+++ /dev/null
@@ -1,28 +0,0 @@
-module Data.Witness.Type where
-{
-	import Data.Witness.Representative;
-
-	-- | The simplest 'Representative', with one value that represents all types.
-	;
-	data Type a = Type;
-
-	instance Eq1 Type where
-	{
-		equals1 Type Type = True;
-	};
-
-	instance Eq (Type a) where
-	{
-		(==) = equals1;
-	};
-
-	instance Representative Type where
-	{
-		getRepWitness Type = MkRepWitness;
-	};
-
-	instance Is Type a where
-	{
-		representative = Type;
-	};
-}
diff --git a/Data/Witness/WitnessDict.hs b/Data/Witness/WitnessDict.hs
deleted file mode 100644
--- a/Data/Witness/WitnessDict.hs
+++ /dev/null
@@ -1,63 +0,0 @@
-module Data.Witness.WitnessDict where
-{
-	import Data.Witness.Any;
-	import Data.Witness.SimpleWitness;
-	import Data.Maybe;
-	
-	-- | A dictionary that is heterogenous up to its simple witness type @w@. 
-	-- Witnesses are the keys of the dictionary, and the values they witness are the values of the dictionary.
-	;
-	newtype WitnessDict w = MkWitnessDict [Any w];
-	
-	-- | An empty dictionary.
-	;
-	emptyWitnessDict :: WitnessDict w;
-	emptyWitnessDict = MkWitnessDict[];
-	
-	-- | Look up the first value in the dictionary that matches the given witness.
-	;
-	witnessDictLookup :: (SimpleWitness w) => w a -> WitnessDict w -> Maybe a;
-	witnessDictLookup wit (MkWitnessDict cells) = listToMaybe (mapMaybe (matchAny wit) cells);
-	
-	-- | Modify the first value in the dictionary that matches a particular witness.
-	;
-	witnessDictModify :: (SimpleWitness w) => w a -> (a -> a) -> WitnessDict w -> WitnessDict w;
-	witnessDictModify wit amap (MkWitnessDict cells) = MkWitnessDict 
-		(replaceFirst ((fmap ((MkAny wit) . amap)) . (matchAny wit)) cells) where
-	{
-		replaceFirst :: (a -> Maybe a) -> [a] -> [a];
-		replaceFirst ama (a:aa) = case ama a of
-		{
-			Just newa -> (newa:aa);
-			_ -> a : (replaceFirst ama aa);
-		};
-		replaceFirst _ _ = [];
-	};
-
-	-- | Replace the first value in the dictionary that matches the witness
-	;
-	witnessDictReplace :: (SimpleWitness w) => w a -> a -> WitnessDict w -> WitnessDict w;
-	witnessDictReplace wit newa = witnessDictModify wit (const newa);
-	
-	-- | Add a witness and value as the first entry in the dictionary.
-	;
-	witnessDictAdd :: w a -> a -> WitnessDict w -> WitnessDict w;
-	witnessDictAdd wit a (MkWitnessDict cells) = MkWitnessDict ((MkAny wit a):cells);
-	
-	-- | Remove the first entry in the dictionary that matches the given witness.
-	;
-	witnessDictRemove :: (SimpleWitness w) => w a -> WitnessDict w -> WitnessDict w;
-	witnessDictRemove wit (MkWitnessDict cells) = MkWitnessDict 
-		(removeFirst (\(MkAny cwit _) -> isJust (matchWitness wit cwit)) cells) where
-	{
-		removeFirst :: (a -> Bool) -> [a] -> [a];
-		removeFirst p (a:as) | p a = as;
-		removeFirst p (a:as) = a : (removeFirst p as);
-		removeFirst _ _ = [];
-	};
-	
-	-- | Create a dictionary from a list of witness\/value pairs
-	;
-	witnessDictFromList :: (SimpleWitness w) => [Any w] -> WitnessDict w;
-	witnessDictFromList = MkWitnessDict;
-}
diff --git a/Data/Witness/WitnessFDict.hs b/Data/Witness/WitnessFDict.hs
deleted file mode 100644
--- a/Data/Witness/WitnessFDict.hs
+++ /dev/null
@@ -1,63 +0,0 @@
-module Data.Witness.WitnessFDict where
-{
-	import Data.Witness.Any;
-	import Data.Witness.SimpleWitness;
-	import Data.Maybe;
-	
-	-- | A dictionary that is heterogenous up to its simple witness type @w@. 
-	-- Witnesses are the keys of the dictionary, and the values they witness are the values of the dictionary.
-	;
-	newtype WitnessFDict w f = MkWitnessFDict [AnyF w f];
-	
-	-- | An empty dictionary.
-	;
-	emptyWitnessFDict :: WitnessFDict w f;
-	emptyWitnessFDict = MkWitnessFDict [];
-	
-	-- | Look up the first value in the dictionary that matches the given witness.
-	;
-	witnessFDictLookup :: (SimpleWitness w) => w a -> WitnessFDict w f -> Maybe (f a);
-	witnessFDictLookup wit (MkWitnessFDict cells) = listToMaybe (mapMaybe (matchAnyF wit) cells);
-	
-	-- | Modify the first value in the dictionary that matches a particular witness.
-	;
-	witnessFDictModify :: (SimpleWitness w) => w a -> (f a -> f a) -> WitnessFDict w f -> WitnessFDict w f;
-	witnessFDictModify wit amap (MkWitnessFDict cells) = MkWitnessFDict 
-		(replaceFirst ((fmap ((MkAnyF wit) . amap)) . (matchAnyF wit)) cells) where
-	{
-		replaceFirst :: (a -> Maybe a) -> [a] -> [a];
-		replaceFirst ama (a:aa) = case ama a of
-		{
-			Just newa -> (newa:aa);
-			_ -> a : (replaceFirst ama aa);
-		};
-		replaceFirst _ _ = [];
-	};
-
-	-- | Replace the first value in the dictionary that matches the witness
-	;
-	witnessFDictReplace :: (SimpleWitness w) => w a -> f a -> WitnessFDict w f -> WitnessFDict w f;
-	witnessFDictReplace wit newfa = witnessFDictModify wit (const newfa);
-	
-	-- | Add a witness and value as the first entry in the dictionary.
-	;
-	witnessFDictAdd :: w a -> f a -> WitnessFDict w f -> WitnessFDict w f;
-	witnessFDictAdd wit fa (MkWitnessFDict cells) = MkWitnessFDict ((MkAnyF wit fa):cells);
-	
-	-- | Remove the first entry in the dictionary that matches the given witness.
-	;
-	witnessFDictRemove :: (SimpleWitness w) => w a -> WitnessFDict w f -> WitnessFDict w f;
-	witnessFDictRemove wit (MkWitnessFDict cells) = MkWitnessFDict 
-		(removeFirst (\(MkAnyF cwit _) -> isJust (matchWitness wit cwit)) cells) where
-	{
-		removeFirst :: (a -> Bool) -> [a] -> [a];
-		removeFirst p (a:as) | p a = as;
-		removeFirst p (a:as) = a : (removeFirst p as);
-		removeFirst _ _ = [];
-	};
-	
-	-- | Create a dictionary from a list of witness\/value pairs
-	;
-	witnessFDictFromList :: (SimpleWitness w) => [AnyF w f] -> WitnessFDict w f;
-	witnessFDictFromList = MkWitnessFDict;
-}
diff --git a/src/Data/Witness.hs b/src/Data/Witness.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Witness.hs
@@ -0,0 +1,33 @@
+module Data.Witness
+(
+    module Data.Proxy,
+    module Data.Type.Equality,
+    module Data.Witness.Any,
+    module Data.Witness.WitnessDict,
+    module Data.Witness.WitnessFDict,
+    module Data.Witness.Nat,
+    module Data.Witness.ListElement,
+    module Data.Witness.List,
+    module Data.Witness.Representative,
+    module Data.Witness
+) where
+{
+    import Data.Proxy;
+    import Data.Type.Equality;
+    import Data.Witness.Any;
+    import Data.Witness.WitnessDict;
+    import Data.Witness.WitnessFDict;
+    import Data.Witness.Nat;
+    import Data.Witness.ListElement;
+    import Data.Witness.List;
+    import Data.Witness.Representative;
+
+    -- | See whether two represented and witnessed types are the same.
+    ;
+    matchIs :: forall w a b. (TestEquality w,Is w a,Is w b) => Proxy w -> Maybe (a :~: b);
+    matchIs _ = testEquality r r where
+    {
+        r :: forall t. (Is w t) => w t;
+        r = representative;
+    };
+}
diff --git a/src/Data/Witness/Any.hs b/src/Data/Witness/Any.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Witness/Any.hs
@@ -0,0 +1,39 @@
+module Data.Witness.Any where
+{
+    import Data.Maybe;
+    import Data.Type.Equality;
+
+    -- | Any value with a witness to it.
+    ;
+    data Any (w :: * -> *) = forall (a :: *). MkAny (w a) a;
+
+    matchAny :: (TestEquality w) => w a -> Any w -> Maybe a;
+    matchAny wit (MkAny cwit ca) = do
+    {
+        Refl <- testEquality cwit wit;
+        return ca;
+    };
+
+    -- | Any value with a witness to a parameter of its type.
+    ;
+    data AnyF (w :: k -> *) (f :: k -> *) = forall (a :: k). MkAnyF (w a) (f a);
+
+    matchAnyF :: (TestEquality w) => w a -> AnyF w f -> Maybe (f a);
+    matchAnyF wit (MkAnyF cwit cfa) = do
+    {
+        Refl <- testEquality cwit wit;
+        return cfa;
+    };
+
+    -- | Any witness.
+    ;
+    data AnyWitness (w :: k -> *) = forall (a :: k). MkAnyWitness (w a);
+
+    matchAnyWitness :: (TestEquality w) => w a -> AnyWitness w -> Bool;
+    matchAnyWitness wit (MkAnyWitness cwit) = isJust (testEquality cwit wit);
+
+    instance (TestEquality w) => Eq (AnyWitness w) where
+    {
+        (==) (MkAnyWitness wa) = matchAnyWitness wa;
+    };
+}
diff --git a/src/Data/Witness/List.hs b/src/Data/Witness/List.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Witness/List.hs
@@ -0,0 +1,358 @@
+module Data.Witness.List where
+{
+    import Prelude hiding (id,(.));
+    import Data.Witness.Representative;
+    import Data.Type.Equality;
+    import Control.Category.Dual;
+    import Data.Constraint(Dict(..));
+    import Control.Applicative;
+    import Control.Category;
+    import Data.Functor.Identity as Import;
+
+    -- | a witness type for HList-style lists.
+    -- The @w@ parameter is the witness type of the elements.
+    ;
+    data ListType (w :: * -> *) (lt :: *) where
+    {
+        NilListType :: ListType w ();
+        ConsListType :: w a -> ListType w lt -> ListType w (a,lt);
+    };
+
+    instance Eq1 w => Eq1 (ListType w) where
+    {
+        equals1 NilListType NilListType = True;
+        equals1 (ConsListType pe pl) (ConsListType qe ql) = (equals1 pe qe) && (equals1 pl ql);
+        equals1 _ _ = False;
+    };
+
+    instance Eq1 w => Eq (ListType w a) where
+    {
+        (==) = equals1;
+    };
+
+    instance (Representative w) => Representative (ListType w) where
+    {
+        getRepWitness NilListType = Dict;
+        getRepWitness (ConsListType w lw) = case (getRepWitness w,getRepWitness lw) of
+        {
+            (Dict,Dict) -> Dict;
+        };
+    };
+
+    instance (Representative w) => Is (ListType w) () where
+    {
+        representative = NilListType;
+    };
+
+    instance (Is w a,Is (ListType w) lt) => Is (ListType w) (a,lt) where
+    {
+        representative = ConsListType representative representative;
+    };
+
+    instance (TestEquality w) => TestEquality (ListType w) where
+    {
+        testEquality NilListType NilListType = Just Refl;
+        testEquality (ConsListType wpa wpb) (ConsListType wqa wqb) = do
+        {
+            Refl <- testEquality wpa wqa;
+            Refl <- testEquality wpb wqb;
+            return Refl;
+        };
+        testEquality _ _ = Nothing;
+    };
+
+    listFill :: ListType w t -> (forall a. w a -> a) -> t;
+    listFill NilListType _f = ();
+    listFill (ConsListType wa wr) f = (f wa,listFill wr f);
+
+    listMap :: ListType w t -> (forall a. w a -> a -> a) -> t -> t;
+    listMap NilListType _f () = ();
+    listMap (ConsListType wa wr) f (a,rest) = (f wa a,listMap wr f rest);
+
+    listLift2 :: ListType w t -> (forall a. w a -> a -> a -> a) -> t -> t -> t;
+    listLift2 NilListType _f () () = ();
+    listLift2 (ConsListType wa wr) f (a,resta) (b,restb) = (f wa a b,listLift2 wr f resta restb);
+
+    listTypeToList :: (forall a. w a -> r) -> ListType w t -> [r];
+    listTypeToList _wr NilListType = [];
+    listTypeToList wr (ConsListType wa rest) = (wr wa):(listTypeToList wr rest);
+
+    listTypeMap :: (forall a. w1 a -> w2 a) -> ListType w1 t -> ListType w2 t;
+    listTypeMap _ww NilListType = NilListType;
+    listTypeMap ww (ConsListType wa rest) = ConsListType (ww wa) (listTypeMap ww rest);
+
+    listIdentity :: ListType Identity lt -> lt;
+    listIdentity NilListType = ();
+    listIdentity (ConsListType (Identity a) rest) = (a,listIdentity rest);
+
+    listSequence ::  (Applicative f) => ListType f lt -> f lt;
+    listSequence NilListType = pure ();
+    listSequence (ConsListType fa rest) = liftA2 (,) fa (listSequence rest);
+
+    data AppendList w la lb = forall lr. MkAppendList
+    {
+        listAppendWitness :: ListType w lr,
+        listAppend :: la -> lb -> lr,
+        listSplit :: lr -> (la,lb)
+    };
+
+    appendList :: ListType w la -> ListType w lb -> AppendList w la lb;
+    appendList NilListType wlb = MkAppendList
+    {
+        listAppendWitness = wlb,
+        listAppend = \() lb -> lb,
+        listSplit = \lb -> ((),lb)
+    };
+    appendList (ConsListType wa wla) wlb = case appendList wla wlb of
+    {
+        MkAppendList wit join split -> MkAppendList
+        {
+            listAppendWitness = ConsListType wa wit,
+            listAppend = \(a,la) lb -> (a,join la lb),
+            listSplit = \(a,lab) -> case split lab of
+            {
+                (la,lb) -> ((a,la),lb);
+            }
+        };
+    };
+
+    data AddItemList w a l = forall lr. MkAddItemList
+    {
+        listAddItemWitness :: ListType w lr,
+        listAddItem :: a -> l -> lr,
+        listSplitItem :: lr -> (a,l)
+    };
+
+    addListItem :: w a -> ListType w l -> AddItemList w a l;
+    addListItem wa wl = MkAddItemList
+    {
+        listAddItemWitness = ConsListType wa wl,
+        listAddItem = (,),
+        listSplitItem = id
+    };
+
+    data MergeItemList w a l = forall lr. MkMergeItemList
+    {
+        listMergeItemWitness :: ListType w lr,
+        listMergeItem :: (Maybe a -> a) -> l -> lr,
+        listUnmergeItem :: lr -> (a,l)
+    };
+
+    mergeListItem :: (TestEquality w) => ListType w l -> w a -> MergeItemList w a l;
+    mergeListItem NilListType wa = MkMergeItemList
+    {
+        listMergeItemWitness = ConsListType wa NilListType,
+        listMergeItem = \maa () -> (maa Nothing,()),
+        listUnmergeItem = id
+    };
+    mergeListItem wl@(ConsListType wa' _) wa | Just Refl <- testEquality wa wa' = MkMergeItemList
+    {
+        listMergeItemWitness = wl,
+        listMergeItem = \maa (a,l) -> (maa (Just a),l),
+        listUnmergeItem = \(a,l) -> (a,(a,l))
+    };
+    mergeListItem (ConsListType wa' wl) wa = case mergeListItem wl wa of
+    {
+        MkMergeItemList wit merge unmerge -> MkMergeItemList
+        {
+            listMergeItemWitness = ConsListType wa' wit,
+            listMergeItem = \maa (a',l) -> (a',merge maa l),
+            listUnmergeItem = \(a',l') -> case unmerge l' of
+            {
+                (a,l) -> (a,(a',l));
+            }
+        };
+    };
+
+    data MergeList w la lb = forall lr. MkMergeList
+    {
+        listMergeWitness :: ListType w lr,
+        listMerge :: (forall t. w t -> t -> t -> t) -> la -> lb -> lr,
+        listUnmerge :: lr -> (la,lb)
+    };
+
+    mergeList :: (TestEquality w) => ListType w la -> ListType w lb -> MergeList w la lb;
+    mergeList wla NilListType = MkMergeList
+    {
+        listMergeWitness = wla,
+        listMerge = \_ la () -> la,
+        listUnmerge = \la -> (la,())
+    };
+    mergeList wla (ConsListType wb wlb) = case mergeListItem wla wb of
+    {
+        MkMergeItemList wla' mergeItem unmergeItem -> case mergeList wla' wlb of
+        {
+            MkMergeList wlr merge unmerge -> MkMergeList
+            {
+                listMergeWitness = wlr,
+                listMerge = \f la (b,lb) -> merge f (mergeItem (\mb' -> case mb' of
+                {
+                    Just b' -> f wb b' b;
+                    Nothing -> b;
+                }) la) lb,
+                listUnmerge = \lr -> case unmerge lr of
+                {
+                    (la',lb) -> case unmergeItem la' of
+                    {
+                        (b,la) -> (la,(b,lb));
+                    };
+                }
+            };
+        };
+    };
+
+    -- could use data-lens:Control.Category.Product(Tensor)
+    class Tensor cc where
+    {
+        tensorUnit :: cc () ();
+        tensorPair :: cc a1 b1 -> cc a2 b2 -> cc (a1,a2) (b1,b2);
+    };
+
+    instance Tensor (->) where
+    {
+        tensorUnit = id;
+        tensorPair ab1 ab2 (a1,a2) = (ab1 a1,ab2 a2);
+    };
+
+    instance (Tensor cc) => Tensor (Dual cc) where
+    {
+        tensorUnit = Dual tensorUnit;
+        tensorPair (Dual ab1) (Dual ab2) = Dual (tensorPair ab1 ab2);
+    };
+
+    type MapWitness cc w1 w2 = forall r v1. w1 v1 -> (forall v2. w2 v2 -> (cc v1 v2) -> r) -> r;
+
+    sameMapWitness :: (forall v. w v -> cc v v) -> MapWitness cc w w;
+    sameMapWitness wc w wcr = wcr w (wc w);
+
+    data MapList cc w2 l = forall lr. MkMapList
+    {
+        listMapWitness :: ListType w2 lr,
+        listMapW :: cc l lr
+    };
+
+    mapList :: (Tensor cc) => MapWitness cc w1 w2 -> ListType w1 l -> MapList cc w2 l;
+    mapList _ NilListType = MkMapList
+    {
+        listMapWitness = NilListType,
+        listMapW = tensorUnit
+    };
+    mapList mapwit (ConsListType w rest) = case mapList mapwit rest of
+    {
+        MkMapList wit listMapW' -> mapwit w (\w' vmap -> MkMapList
+        {
+            listMapWitness = ConsListType w' wit,
+            listMapW = tensorPair vmap listMapW'
+        });
+    };
+
+    data RemoveFromList w a l = forall lr. MkRemoveFromList
+    {
+        listRemoveWitness :: ListType w lr,
+        listInsert :: a -> lr -> l,
+        listRemove :: l -> lr
+    };
+
+    removeAllMatching :: (TestEquality w) => w a -> ListType w l -> RemoveFromList w a l;
+    removeAllMatching _ NilListType = MkRemoveFromList
+    {
+        listRemoveWitness = NilListType,
+        listInsert = \_ -> id,
+        listRemove = id
+    };
+    removeAllMatching wa (ConsListType wb rest) = case removeAllMatching wa rest of
+    {
+        MkRemoveFromList wit ins rm -> case testEquality wa wb of
+        {
+            Just Refl -> MkRemoveFromList
+            {
+                listRemoveWitness = wit,
+                listInsert = \a l2 -> (a,ins a l2),
+                listRemove = \(_,l1) -> rm l1
+            };
+            Nothing -> MkRemoveFromList
+            {
+                listRemoveWitness = ConsListType wb wit,
+                listInsert = \a (b,l2) -> (b,ins a l2),
+                listRemove = \(b,l1) -> (b,rm l1)
+            };
+        };
+    };
+
+    data RemoveManyFromList wit lx l = forall lr. MkRemoveManyFromList
+    {
+        listRemoveManyWitness :: ListType wit lr,
+        listInsertMany :: lx -> lr -> l,
+        listRemoveMany :: l -> lr
+    };
+
+    removeAllMatchingMany :: (TestEquality wit) => ListType wit lx -> ListType wit l -> RemoveManyFromList wit lx l;
+    removeAllMatchingMany NilListType wl = MkRemoveManyFromList
+    {
+        listRemoveManyWitness = wl,
+        listInsertMany = \_ lr -> lr,
+        listRemoveMany = \l -> l
+    };
+    removeAllMatchingMany (ConsListType wa wlx) wl = case removeAllMatching wa wl of
+    {
+        MkRemoveFromList wl' ins rm -> case removeAllMatchingMany wlx wl' of
+        {
+            MkRemoveManyFromList wl'' insM remM -> MkRemoveManyFromList
+            {
+                listRemoveManyWitness = wl'',
+                listInsertMany = \(a,lx) lr -> ins a (insM lx lr),
+                listRemoveMany = remM . rm
+            };
+        };
+    };
+
+    newtype EitherWitness (w1 :: k -> *) (w2 :: k -> *) (a :: k) = MkEitherWitness (Either (w1 a) (w2 a));
+
+    instance (TestEquality w1,TestEquality w2) => TestEquality (EitherWitness w1 w2) where
+    {
+        testEquality (MkEitherWitness (Left wa)) (MkEitherWitness (Left wb)) = testEquality wa wb;
+        testEquality (MkEitherWitness (Right wa)) (MkEitherWitness (Right wb)) = testEquality wa wb;
+        testEquality _ _ = Nothing;
+    };
+
+    data PartitionList wit1 wit2 l = forall l1 l2. MkPartitionList
+    {
+        listPartitionWitness1 :: ListType wit1 l1,
+        listPartitionWitness2 :: ListType wit2 l2,
+        listFromPartition :: l1 -> l2 -> l,
+        listToPartition1 :: l -> l1,
+        listToPartition2 :: l -> l2
+    };
+
+    partitionList :: ListType (EitherWitness w1 w2) l -> PartitionList w1 w2 l;
+    partitionList NilListType = MkPartitionList
+    {
+        listPartitionWitness1 = NilListType,
+        listPartitionWitness2 = NilListType,
+        listFromPartition = \() () -> (),
+        listToPartition1 = \() -> (),
+        listToPartition2 = \() -> ()
+    };
+    partitionList (ConsListType (MkEitherWitness (Left w1a)) rest) = case partitionList rest of
+    {
+        MkPartitionList pw1 pw2 fp tp1 tp2 -> MkPartitionList
+        {
+            listPartitionWitness1 = ConsListType w1a pw1,
+            listPartitionWitness2 = pw2,
+            listFromPartition = \(a,l1) l2 -> (a,fp l1 l2),
+            listToPartition1 = \(a,l) -> (a,tp1 l),
+            listToPartition2 = \(_,l) -> tp2 l
+        };
+    };
+    partitionList (ConsListType (MkEitherWitness (Right w2a)) rest) = case partitionList rest of
+    {
+        MkPartitionList pw1 pw2 fp tp1 tp2 -> MkPartitionList
+        {
+            listPartitionWitness1 = pw1,
+            listPartitionWitness2 = ConsListType w2a pw2,
+            listFromPartition = \l1 (a,l2) -> (a,fp l1 l2),
+            listToPartition1 = \(_,l) -> tp1 l,
+            listToPartition2 = \(a,l) -> (a,tp2 l)
+        };
+    };
+}
diff --git a/src/Data/Witness/ListElement.hs b/src/Data/Witness/ListElement.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Witness/ListElement.hs
@@ -0,0 +1,28 @@
+module Data.Witness.ListElement where
+{
+    import Data.Witness.Nat;
+
+    class HasListElement (n :: NatKind) (list :: *) where
+    {
+        type ListElement n list :: *;
+        getListElement :: Nat n -> list -> ListElement n list;
+        putListElement :: Nat n -> ListElement n list -> list -> list;
+    };
+
+    modifyListElement :: (HasListElement n t) => Nat n -> (ListElement n t -> ListElement n t) -> t -> t;
+    modifyListElement n aa t = putListElement n (aa (getListElement n t)) t;
+
+    instance HasListElement Zero (a,r) where
+    {
+        type ListElement Zero (a,r) = a;
+        getListElement _ (a,_) = a;
+        putListElement _ a (_,r) = (a,r);
+    };
+
+    instance (HasListElement n r) => HasListElement (Succ n) (a,r) where
+    {
+        type ListElement (Succ n) (a,r) = ListElement n r;
+        getListElement (SuccNat n) (_,r) = getListElement n r;
+        putListElement (SuccNat n) a (f,r) = (f,putListElement n a r);
+    };
+}
diff --git a/src/Data/Witness/Nat.hs b/src/Data/Witness/Nat.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Witness/Nat.hs
@@ -0,0 +1,51 @@
+module Data.Witness.Nat where
+{
+    import Prelude hiding (id,(.));
+    import Data.Maybe;
+    import Data.Type.Equality;
+    import Data.Constraint(Dict(..));
+    import Data.Witness.Representative;
+
+    data NatKind = Zero | Succ NatKind;
+
+    data Nat (t :: NatKind) where
+    {
+        ZeroNat :: Nat Zero;
+        SuccNat :: Nat t -> Nat (Succ t);
+    };
+
+    instance TestEquality Nat where
+    {
+        testEquality ZeroNat ZeroNat = return Refl;
+        testEquality (SuccNat a) (SuccNat b) = do
+        {
+            Refl <- testEquality a b;
+            return Refl;
+        };
+        testEquality _ _ = Nothing;
+    };
+
+    instance Eq1 Nat where
+    {
+        equals1 a b = isJust (testEquality a b);
+    };
+
+    instance Representative Nat where
+    {
+        getRepWitness ZeroNat = Dict;
+        getRepWitness (SuccNat n) = case getRepWitness n of
+        {
+            Dict -> Dict;
+        };
+    };
+
+    instance Is Nat Zero where
+    {
+        representative = ZeroNat;
+    };
+
+    instance (Is Nat n) => Is Nat (Succ n) where
+    {
+        representative = SuccNat representative;
+    };
+}
diff --git a/src/Data/Witness/Representative.hs b/src/Data/Witness/Representative.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Witness/Representative.hs
@@ -0,0 +1,64 @@
+module Data.Witness.Representative where
+{
+    import Data.Witness.Any;
+    import Data.Constraint;
+    import Data.Proxy;
+
+    class Eq1 (p :: k -> *) where
+    {
+        equals1 :: forall a. p a -> p a -> Bool;
+    };
+
+    instance Eq1 Proxy where
+    {
+        equals1 Proxy Proxy = True;
+    };
+
+    isWitnessRepresentative :: Dict (Is rep a) -> rep a;
+    isWitnessRepresentative Dict = representative;
+
+    class Eq1 rep => Representative (rep :: k -> *) where
+    {
+        -- | Every value is an instance of 'Is'.
+        ;
+        getRepWitness :: forall (a :: k). rep a -> Dict (Is rep a);
+    };
+
+    instance Representative Proxy where
+    {
+        getRepWitness Proxy = Dict;
+    };
+
+    withRepresentative :: forall (rep :: k -> *) r. (Representative rep) =>
+      (forall (a :: k). (Is rep a) => rep a -> r) -> (forall (b :: k). rep b -> r);
+    withRepresentative foo rep = case getRepWitness rep of
+    {
+        Dict -> foo rep;
+    };
+
+    -- | If two representatives have the same type, then they have the same value.
+    ;
+    class Representative rep => Is (rep :: k -> *) (a :: k) where
+    {
+        -- | The representative value for type @a@.
+        ;
+        representative :: rep a;
+    };
+
+    instance Is Proxy a where
+    {
+        representative = Proxy;
+    };
+
+    getRepresentative :: (Is rep a) => a -> rep a;
+    getRepresentative _ = representative;
+
+    rerepresentative :: (Is rep a) => p a -> rep a;
+    rerepresentative _ = representative;
+
+    mkAny :: (Is rep a) => a -> Any rep;
+    mkAny a = MkAny representative a;
+
+    mkAnyF :: (Is rep a) => f a -> AnyF rep f;
+    mkAnyF fa = MkAnyF representative fa;
+}
diff --git a/src/Data/Witness/WitnessDict.hs b/src/Data/Witness/WitnessDict.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Witness/WitnessDict.hs
@@ -0,0 +1,63 @@
+module Data.Witness.WitnessDict where
+{
+    import Data.Maybe;
+    import Data.Type.Equality;
+    import Data.Witness.Any;
+
+    -- | A dictionary that is heterogenous up to its simple witness type @w@.
+    -- Witnesses are the keys of the dictionary, and the values they witness are the values of the dictionary.
+    ;
+    newtype WitnessDict (w :: * -> *) = MkWitnessDict [Any w];
+
+    -- | An empty dictionary.
+    ;
+    emptyWitnessDict :: WitnessDict w;
+    emptyWitnessDict = MkWitnessDict[];
+
+    -- | Look up the first value in the dictionary that matches the given witness.
+    ;
+    witnessDictLookup :: (TestEquality w) => w a -> WitnessDict w -> Maybe a;
+    witnessDictLookup wit (MkWitnessDict cells) = listToMaybe (mapMaybe (matchAny wit) cells);
+
+    -- | Modify the first value in the dictionary that matches a particular witness.
+    ;
+    witnessDictModify :: (TestEquality w) => w a -> (a -> a) -> WitnessDict w -> WitnessDict w;
+    witnessDictModify wit amap (MkWitnessDict cells) = MkWitnessDict
+        (replaceFirst ((fmap ((MkAny wit) . amap)) . (matchAny wit)) cells) where
+    {
+        replaceFirst :: (a -> Maybe a) -> [a] -> [a];
+        replaceFirst ama (a:aa) = case ama a of
+        {
+            Just newa -> (newa:aa);
+            _ -> a : (replaceFirst ama aa);
+        };
+        replaceFirst _ _ = [];
+    };
+
+    -- | Replace the first value in the dictionary that matches the witness
+    ;
+    witnessDictReplace :: (TestEquality w) => w a -> a -> WitnessDict w -> WitnessDict w;
+    witnessDictReplace wit newa = witnessDictModify wit (const newa);
+
+    -- | Add a witness and value as the first entry in the dictionary.
+    ;
+    witnessDictAdd :: w a -> a -> WitnessDict w -> WitnessDict w;
+    witnessDictAdd wit a (MkWitnessDict cells) = MkWitnessDict ((MkAny wit a):cells);
+
+    -- | Remove the first entry in the dictionary that matches the given witness.
+    ;
+    witnessDictRemove :: (TestEquality w) => w a -> WitnessDict w -> WitnessDict w;
+    witnessDictRemove wit (MkWitnessDict cells) = MkWitnessDict
+        (removeFirst (\(MkAny cwit _) -> isJust (testEquality wit cwit)) cells) where
+    {
+        removeFirst :: (a -> Bool) -> [a] -> [a];
+        removeFirst p (a:as) | p a = as;
+        removeFirst p (a:as) = a : (removeFirst p as);
+        removeFirst _ _ = [];
+    };
+
+    -- | Create a dictionary from a list of witness\/value pairs
+    ;
+    witnessDictFromList :: (TestEquality w) => [Any w] -> WitnessDict w;
+    witnessDictFromList = MkWitnessDict;
+}
diff --git a/src/Data/Witness/WitnessFDict.hs b/src/Data/Witness/WitnessFDict.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Witness/WitnessFDict.hs
@@ -0,0 +1,63 @@
+module Data.Witness.WitnessFDict where
+{
+    import Data.Maybe;
+    import Data.Type.Equality;
+    import Data.Witness.Any;
+
+    -- | A dictionary that is heterogenous up to its simple witness type @w@.
+    -- Witnesses are the keys of the dictionary, and the values they witness are the values of the dictionary.
+    ;
+    newtype WitnessFDict (w :: k -> *) (f :: k -> *) = MkWitnessFDict [AnyF w f];
+
+    -- | An empty dictionary.
+    ;
+    emptyWitnessFDict :: WitnessFDict w f;
+    emptyWitnessFDict = MkWitnessFDict [];
+
+    -- | Look up the first value in the dictionary that matches the given witness.
+    ;
+    witnessFDictLookup :: (TestEquality w) => w a -> WitnessFDict w f -> Maybe (f a);
+    witnessFDictLookup wit (MkWitnessFDict cells) = listToMaybe (mapMaybe (matchAnyF wit) cells);
+
+    -- | Modify the first value in the dictionary that matches a particular witness.
+    ;
+    witnessFDictModify :: (TestEquality w) => w a -> (f a -> f a) -> WitnessFDict w f -> WitnessFDict w f;
+    witnessFDictModify wit amap (MkWitnessFDict cells) = MkWitnessFDict
+        (replaceFirst ((fmap ((MkAnyF wit) . amap)) . (matchAnyF wit)) cells) where
+    {
+        replaceFirst :: (a -> Maybe a) -> [a] -> [a];
+        replaceFirst ama (a:aa) = case ama a of
+        {
+            Just newa -> (newa:aa);
+            _ -> a : (replaceFirst ama aa);
+        };
+        replaceFirst _ _ = [];
+    };
+
+    -- | Replace the first value in the dictionary that matches the witness
+    ;
+    witnessFDictReplace :: (TestEquality w) => w a -> f a -> WitnessFDict w f -> WitnessFDict w f;
+    witnessFDictReplace wit newfa = witnessFDictModify wit (const newfa);
+
+    -- | Add a witness and value as the first entry in the dictionary.
+    ;
+    witnessFDictAdd :: w a -> f a -> WitnessFDict w f -> WitnessFDict w f;
+    witnessFDictAdd wit fa (MkWitnessFDict cells) = MkWitnessFDict ((MkAnyF wit fa):cells);
+
+    -- | Remove the first entry in the dictionary that matches the given witness.
+    ;
+    witnessFDictRemove :: (TestEquality w) => w a -> WitnessFDict w f -> WitnessFDict w f;
+    witnessFDictRemove wit (MkWitnessFDict cells) = MkWitnessFDict
+        (removeFirst (\(MkAnyF cwit _) -> isJust (testEquality wit cwit)) cells) where
+    {
+        removeFirst :: (a -> Bool) -> [a] -> [a];
+        removeFirst p (a:as) | p a = as;
+        removeFirst p (a:as) = a : (removeFirst p as);
+        removeFirst _ _ = [];
+    };
+
+    -- | Create a dictionary from a list of witness\/value pairs
+    ;
+    witnessFDictFromList :: (TestEquality w) => [AnyF w f] -> WitnessFDict w f;
+    witnessFDictFromList = MkWitnessFDict;
+}
diff --git a/witness.cabal b/witness.cabal
--- a/witness.cabal
+++ b/witness.cabal
@@ -1,53 +1,52 @@
-cabal-version: >= 1.6
+cabal-version:  >=1.14
+name:           witness
+version:        0.3
+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/witness
+bug-reports:    https://github.com/AshleyYakeley/witness/issues
+synopsis:       values that witness types
+description:
+    A witness is a value that /witnesses/ some sort of constraint on some list of type variables.
+    This library provides support for simple witnesses, that constrain a type variable to a single type, and equality witnesses, that constrain two type variables to be the same type.
+    It also provides classes for representatives, which are values that represent types.
+    See the paper /Witnesses and Open Witnesses/ (<http://semantic.org/stuff/Open-Witnesses.pdf>).
+category:       Data
+build-type:     Simple
 
-name: witness
-version: 0.2
-build-type: Simple
-license: BSD3
-license-file: LICENSE
-copyright:
-maintainer: Ashley Yakeley <ashley@semantic.org>
-build-depends: base == 4.*, mtl >=1.1
-stability:
-homepage:
-package-url:
-bug-reports:
-synopsis: values that witness types
-description: A witness is a value that /witnesses/ some sort of constraint on some list of type variables.
-             This library provides support for simple witnesses, that constrain a type variable to a single type, and equality witnesses, that constrain two type variables to be the same type. It also provides classes for representatives, which are values that represent types.
-             See the paper /Witnesses and Open Witnesses/ (<http://semantic.org/stuff/Open-Witnesses.pdf>).
-category: Data
-author: Ashley Yakeley <ashley@semantic.org>
-tested-with:
-data-files:
-data-dir: ""
-extra-source-files:
-extra-tmp-files:
-exposed-modules: Data.Witness Data.Witness.SimpleWitness
-                 Data.Witness.Type Data.Witness.List Data.Witness.WitnessDict
-                 Data.Witness.WitnessFDict Data.Witness.Any Data.Witness.Nat
-                 Data.Witness.Representative Data.Witness.EqualType
-exposed: True
-buildable: True
-build-tools:
-cpp-options:
-cc-options:
-ld-options:
-pkgconfig-depends:
-frameworks:
-c-sources:
-extensions: MultiParamTypeClasses RankNTypes FlexibleContexts
-            FlexibleInstances EmptyDataDecls KindSignatures TypeFamilies GADTs
-extra-libraries:
-extra-lib-dirs:
-includes:
-install-includes:
-include-dirs:
-hs-source-dirs: .
-other-modules:
-ghc-prof-options:
-ghc-shared-options:
-ghc-options: -Wall
-hugs-options:
-nhc98-options:
-jhc-options:
+library
+    hs-source-dirs: src
+    default-language: Haskell98
+    default-extensions:
+        MultiParamTypeClasses
+        RankNTypes
+        FlexibleContexts
+        TypeOperators
+        FlexibleInstances
+        EmptyDataDecls
+        KindSignatures
+        TypeFamilies
+        GADTs
+        PolyKinds
+        DataKinds
+        ScopedTypeVariables
+        PatternGuards
+    build-depends:
+        base == 4.*,
+        transformers >=0.3,
+        categories == 1.0.*,
+        constraints >= 0.3
+    exposed-modules:
+        Data.Witness.Any
+        Data.Witness.WitnessDict
+        Data.Witness.WitnessFDict
+        Data.Witness.Nat
+        Data.Witness.ListElement
+        Data.Witness.List
+        Data.Witness.Representative
+        Data.Witness
+    ghc-options: -Wall