diff --git a/src/TypeUnary/Nat.hs b/src/TypeUnary/Nat.hs
--- a/src/TypeUnary/Nat.hs
+++ b/src/TypeUnary/Nat.hs
@@ -35,6 +35,7 @@
 
 import Control.Applicative ((<$>))
 import Data.Maybe (isJust)
+import Data.Typeable (Typeable)
 
 import Data.Proof.EQ
 
@@ -269,6 +270,7 @@
   (*)    = noIndex "(*)"
   abs    = noIndex "abs"
   signum = noIndex "signum"
+  negate = noIndex "negate"
 
 noIndex :: String -> a
 noIndex meth = error (meth ++ ": no method for Index n. Sorry.")
@@ -281,7 +283,10 @@
 --------------------------------------------------------------------}
 
 -- | Is @n@ a natural number type?
-class IsNat n where nat :: Nat n
+class Typeable n => IsNat n where nat :: Nat n
 
 instance            IsNat Z     where nat = Zero
 instance IsNat n => IsNat (S n) where nat = Succ nat
+
+-- The Typeable superclass enables client code to deduce Typeable from IsNat.
+-- Occasionally useful.
diff --git a/src/TypeUnary/TyNat.hs b/src/TypeUnary/TyNat.hs
--- a/src/TypeUnary/TyNat.hs
+++ b/src/TypeUnary/TyNat.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE TypeFamilies, TypeOperators, EmptyDataDecls #-}
 {-# LANGUAGE UndecidableInstances #-} -- for :*:
+{-# LANGUAGE DeriveDataTypeable #-}
 {-# OPTIONS_GHC -Wall #-}
 ----------------------------------------------------------------------
 -- |
@@ -20,11 +21,12 @@
   , N0,N1,N2,N3,N4,N5,N6,N7,N8,N9,N10,N11,N12,N13,N14,N15,N16
   ) where
 
+import Data.Typeable (Typeable)
 
 -- | Type-level representation of zero
-data Z
+data Z    deriving Typeable
 -- | Type-level representation of successor
-data S n
+data S n  deriving Typeable
 
 -- INSTANCE_TYPEABLE0(Z,zTC ,"Z")
 -- INSTANCE_TYPEABLE1(S,sTC ,"S")
diff --git a/src/TypeUnary/Vec.hs b/src/TypeUnary/Vec.hs
--- a/src/TypeUnary/Vec.hs
+++ b/src/TypeUnary/Vec.hs
@@ -5,6 +5,7 @@
            , ScopedTypeVariables, CPP
            , RankNTypes
            , MultiParamTypeClasses, FunctionalDependencies
+           , DeriveDataTypeable
   #-}
 {-# OPTIONS_GHC -Wall #-}
 
@@ -44,13 +45,11 @@
 
 import Prelude hiding (foldr,sum,and)
 
--- #include "Typeable.h"
-
 import Data.Monoid (Monoid(..))
 import Control.Applicative (Applicative(..),liftA2,(<$>))
 import Data.Foldable (Foldable(..),toList,sum) -- ,and
 import Data.Traversable (Traversable(..))
--- import Data.Typeable
+import Data.Typeable (Typeable)
 
 import Foreign.Storable
 import Foreign.Ptr (Ptr,plusPtr,castPtr)
@@ -70,6 +69,7 @@
 data Vec :: * -> * -> * where
   ZVec :: Vec Z a 
   (:<) :: a -> Vec n a -> Vec (S n) a
+ deriving Typeable
 
 -- | Type-safe un-cons for vectors
 unConsV :: Vec (S n) a -> (a, Vec n a)
@@ -516,6 +516,11 @@
 --     from the context (n ~ S n1)
 
 -}
+
+-- resplit :: (Vec m a, Vec n a) -> (Vec n a, Vec m a)
+-- resplit (u,v) = split (u <+> v)
+-- 
+-- Won't type-check without commutativity of addition. :(
 
 {-
 
diff --git a/type-unary.cabal b/type-unary.cabal
--- a/type-unary.cabal
+++ b/type-unary.cabal
@@ -1,5 +1,5 @@
 Name:                type-unary
-Version:             0.2.8
+Version:             0.2.13
 Cabal-Version:       >= 1.6
 Synopsis:            
   Type-level and typed unary natural numbers, inequality proofs, vectors
@@ -11,7 +11,7 @@
 Author:              Conal Elliott
 Maintainer:          conal@conal.net
 Homepage:            https://github.com/conal/type-unary
-Copyright:           (c) 2009-2012 by Conal Elliott
+Copyright:           (c) 2009-2014 by Conal Elliott
 License:             BSD3
 License-File:        COPYING
 Stability:           provisional
@@ -25,7 +25,7 @@
 Library
   hs-Source-Dirs:      src
   Extensions:
-  Build-Depends:       base >=4 && < 5, ty, vector-space, applicative-numbers
+  Build-Depends:       base >=4 && < 5, ty>=0.1.5, vector-space, applicative-numbers
   Exposed-Modules:     
                        TypeUnary.TyNat
                        TypeUnary.Nat
@@ -33,3 +33,4 @@
                        
   ghc-options:         -Wall
 
+ ghc-prof-options:    -prof -auto-all