diff --git a/changelog b/changelog
--- a/changelog
+++ b/changelog
@@ -1,3 +1,6 @@
+structural-induction 0.2.0.1 (released 2015-06-10)
+	* Add missing test suite files to extra-source-files.
+
 structural-induction 0.2 (released 2015-04-10)
 	* Support GHC 7.10
 
diff --git a/structural-induction.cabal b/structural-induction.cabal
--- a/structural-induction.cabal
+++ b/structural-induction.cabal
@@ -1,6 +1,6 @@
 name:               structural-induction
 category:           Theorem Provers, Logic
-version:            0.2
+version:            0.2.0.1
 license:            LGPL-3
 license-file:       LICENSE
 author:             Dan Rosén
@@ -12,20 +12,14 @@
 tested-with:        GHC == 7.4.2, GHC == 7.6.3, GHC == 7.8.3, GHC == 7.10.1
 synopsis:           Instantiate structural induction schemas for algebraic data types
 description:        See documentation for Induction.Structural
-extra-source-files: changelog
+extra-source-files: changelog test/Env.hs test/EnvTypes.hs test/Walk.hs test/Util.hs test/Trace.hs test/Nat.hs
 
 source-repository head
   type: git
   location: git://github.com/danr/structural-induction.git
 
-flag Werror
-  default: False
-  manual: True
-
 library
   ghc-options:    -Wall -fno-warn-unused-imports
-  if flag(Werror)
-    ghc-options: -Werror
 
   exposed-modules:
     Induction.Structural,
@@ -50,8 +44,6 @@
   main-is:        Main.hs
   hs-source-dirs: test
   ghc-options:    -Wall -fno-warn-unused-imports
-  if flag(Werror)
-    ghc-options: -Werror
 
   build-depends:
     structural-induction,
diff --git a/test/Env.hs b/test/Env.hs
new file mode 100644
--- /dev/null
+++ b/test/Env.hs
@@ -0,0 +1,129 @@
+{-# LANGUAGE GADTs, ConstraintKinds, ExplicitForAll, PatternGuards #-}
+module Env where
+
+import Test.QuickCheck
+import Control.Applicative
+
+import Induction.Structural
+
+import EnvTypes
+import Nat
+import Util
+
+type Oblig = Obligation Con' String Ty'
+type Tm    = Term Con' String
+type P     = Predicate Con' String
+type Hyp   = Hypothesis Con' String Ty'
+
+-- | A small test environment. No exponentials for now.
+testEnv :: Repr a -> Maybe [(Con a,[Arg Ty'])]
+testEnv t = case t of
+    Unit      -> Just [(TT,[])]
+    Nat       -> Just [(Zero,[])
+                      ,(Succ,[Rec (Si Nat)])
+                      ]
+    PInt      -> Just [(Pos,[NonRec (Si Nat)])
+                      ,(Neg,[NonRec (Si Nat)])
+                      ]
+    Bool      -> Just [(Tru,[]),(Fls,[])]
+    List a    -> Just [(Nil a,[])
+                      ,(Cons,[NonRec (Si a),Rec (Si (List a))])
+                      ]
+    Maybe a   -> Just [(Ntng a,[])
+                      ,(Jst,[NonRec (Si a)])
+                      ]
+    TupTy a b -> Just [(Tup,[NonRec (Si a),NonRec (Si b)])]
+    TyVar     -> Nothing
+
+-- | Forgetting some type info
+testEnv' :: TyEnv Con' Ty'
+testEnv' (Si t) = case testEnv t of
+    Just ksargs -> Just (map (uncurry forget) ksargs)
+    Nothing -> Nothing
+  where
+    forget :: forall a . EqShow a => Con a -> [Arg Ty'] -> (Con',[Arg Ty'])
+    forget k args = (Si k, args)
+
+-- | Generates a random value of some type
+arbFromType :: Repr a -> Gen a
+arbFromType t = case t of
+    Unit   -> arbitrary
+    Nat    -> arbitrary
+    PInt   -> arbitrary
+    Bool   -> arbitrary
+    List a -> halfSize $ \ s -> frequency
+        [ (1, return [])
+        , (s, (:) <$> arbFromType a <*> arbFromType (List a))
+        ]
+    Maybe a -> sized $ \ s -> frequency
+        [ (1, return Nothing)
+        , (s, Just <$> arbFromType a)
+        ]
+    TupTy a b -> (,) <$> arbFromType a <*> arbFromType b
+    TyVar -> arbitrary
+
+-- | Forget type information
+arbFromType' :: Sigma Repr -> Gen (Exists Repr)
+arbFromType' (Si r) = Val r <$> arbFromType r
+
+startFromTypes :: [Ty'] -> Gen [Repr']
+startFromTypes = mapM arbFromType'
+
+-- Cannot make this well typed in a nice way
+mkCon :: Con' -> [Repr'] -> Repr'
+mkCon (Si c) as = case c of
+    TT     -> case as of { []                -> Val Unit ()            ; _ -> ill_typed }
+    Zero   -> case as of { []                -> Val Nat Z              ; _ -> ill_typed }
+    Succ   -> case as of { [Val Nat n]       -> Val Nat (S n)          ; _ -> ill_typed }
+    Pos    -> case as of { [Val Nat n]       -> Val PInt (P n)         ; _ -> ill_typed }
+    Neg    -> case as of { [Val Nat n]       -> Val PInt (N n)         ; _ -> ill_typed }
+    Fls    -> case as of { []                -> Val Bool False         ; _ -> ill_typed }
+    Tru    -> case as of { []                -> Val Bool True          ; _ -> ill_typed }
+    Ntng a -> case as of { []                -> Val (Maybe a) Nothing  ; _ -> ill_typed }
+    Jst    -> case as of { [Val a x]         -> Val (Maybe a) (Just x) ; _ -> ill_typed }
+    Tup    -> case as of { [Val a x,Val b y] -> Val (TupTy a b) (x,y)  ; _ -> ill_typed }
+    Nil a  -> case as of { []                -> Val (List a) []        ; _ -> ill_typed }
+    Cons   -> case as of
+        [Val a x,Val (List b) xs] -> case a ==? b of
+            Just Refl -> Val (List a) (x:xs)
+            Nothing   -> error $ "mkCon: " ++ show as ++ " is heterogenous!"
+        _ -> ill_typed
+  where
+    ill_typed :: a
+    ill_typed = error $ "mkCon: illtyped: " ++ show (Si c) ++ " on " ++ show as
+
+type VarMap = [(String,Repr')]
+
+-- | Tries to match a representation to a term, returning bound variables
+match :: Repr' -> Tm -> Maybe VarMap
+match v tm0 = case tm0 of
+    Var s -> Just [(s,v)]
+    Con (Si c) tms -> case (v,c,tms) of
+        (Val Unit ()            , TT     , [])   -> ok
+        (Val Nat Z              , Zero   , [])   -> ok
+        (Val Nat (S x)          , Succ   , [tm]) -> match (Val Nat x) tm
+        (Val PInt (P x)         , Pos    , [tm]) -> match (Val Nat x) tm
+        (Val PInt (N x)         , Neg    , [tm]) -> match (Val Nat x) tm
+        (Val Bool True          , Tru    , [])   -> ok
+        (Val Bool False         , Fls    , [])   -> ok
+        (Val (Maybe a) Nothing  , Ntng b , []) | Just Refl <- a ==? b -> ok
+        (Val (Maybe a) (Just x) , Jst    , [tm]) -> match (Val a x) tm
+        (Val (List a) []        , Nil b  , []) | Just Refl <- a ==? b -> ok
+        (Val (List a) (x:xs)    , Cons   , [t1,t2]) ->
+            match (Val a x) t1 `comb` match (Val (List a) xs) t2
+        (Val (TupTy a b) (x,y)  , Tup    , [t1,t2]) ->
+            match (Val a x) t1 `comb` match (Val b y) t2
+        _ -> Nothing
+    Fun{} -> error "match: No support for exponentials!"
+  where
+    ok = Just []
+    comb r s = (++) <$> r <*> s
+
+-- | Show induction schema
+showOblig :: [Oblig] -> String
+showOblig = unlines . map ((++ ".") . render . linObligation style)
+
+-- | The style for printing
+style :: Style Con' String Ty'
+style = Style (text . show) text (text . show)
+
diff --git a/test/EnvTypes.hs b/test/EnvTypes.hs
new file mode 100644
--- /dev/null
+++ b/test/EnvTypes.hs
@@ -0,0 +1,164 @@
+{-# LANGUAGE GADTs, KindSignatures, DeriveDataTypeable,
+        FlexibleInstances, ConstraintKinds,
+        PatternGuards, TemplateHaskell #-}
+module EnvTypes where
+
+import Nat
+
+import Data.Function (on)
+import Data.Typeable (Typeable)
+
+import Test.QuickCheck
+import Test.Feat
+
+type EqShow a = (Eq a,Show a,Arbitrary a)
+
+data Sigma :: (* -> *) -> * where
+    Si :: EqShow a => r a -> Sigma r
+
+data Exists :: (* -> *) -> * where
+    Val :: EqShow a => r a -> a -> Exists r
+
+type Repr' = Exists Repr
+
+type Ty' = Sigma Repr
+
+
+-- Representations of our types.
+-- Putting Eq and Show here simplifies those instances for Repr a bit
+data Repr a where
+    Unit  :: Repr ()
+    Nat   :: Repr Nat
+    PInt  :: Repr PInt
+    Bool  :: Repr Bool
+    List  :: EqShow a => Repr a -> Repr [a]
+    Maybe :: EqShow a => Repr a -> Repr (Maybe a)
+    TupTy :: (EqShow a,EqShow b) => Repr a -> Repr b -> Repr (a,b)
+    TyVar :: Repr Int
+    -- ^ Should this contain more information?
+  deriving Typeable
+
+-- The more number of units, the more boring this type is to test
+data URepr
+    = UUnit () () ()
+    | UNat
+    | UPInt
+    | UBool () ()
+    | UList URepr
+    | UMaybe URepr ()
+    | UTupTy URepr URepr ()
+    | UTyVar () () ()
+  deriving Typeable
+
+deriveEnumerable ''URepr
+
+toTy :: URepr -> Ty'
+toTy u = case u of
+    UUnit{}      -> Si Unit
+    UNat         -> Si Nat
+    UPInt        -> Si PInt
+    UBool{}      -> Si Bool
+    UList a      | Si a' <- toTy a -> Si (List a')
+    UMaybe a _   | Si a' <- toTy a -> Si (Maybe a')
+    UTupTy a b _ | Si a' <- toTy a
+                 , Si b' <- toTy b -> Si (TupTy a' b')
+    UTyVar{}     -> Si TyVar
+
+enumTy' :: Enumerate Ty'
+enumTy' = fmap toTy enumerate
+
+{-# ANN enumTy's "HLint: ignore Use camelCase" #-}
+enumTy's :: Enumerate [Ty']
+enumTy's = fmap (map toTy) enumerate
+
+showRepr :: Repr a -> String
+showRepr r = case r of
+    Unit      -> "Unit"
+    Nat       -> "Nat"
+    PInt      -> "PInt"
+    Bool      -> "Bool"
+    List a    -> "List " ++ showRepr a
+    Maybe a   -> "Maybe " ++ showRepr a
+    TupTy a b -> "TupTy " ++ showRepr a ++ " " ++ showRepr b
+    TyVar     -> "TyVar"
+
+showRepr' :: Repr' -> String
+showRepr' (Val r x) = "Val " ++ showRepr r ++ " " ++ show x
+
+instance Show Ty' where
+    show (Si r) = case r of
+        Unit      -> "()"
+        Nat       -> "Nat"
+        PInt      -> "Int"
+        Bool      -> "Bool"
+        List a    -> "[" ++ show (Si a) ++ "]"
+        Maybe a   -> "Maybe " ++ show (Si a)
+        TupTy a b -> "(" ++ show (Si a) ++ "," ++ show (Si b) ++ ")"
+        TyVar     -> "a"
+
+type Con' = Sigma Con
+
+data Con a where
+    TT   :: Con ()
+    Zero :: Con Nat
+    Succ :: Con Nat
+    Pos  :: Con PInt
+    Neg  :: Con PInt
+    Tru  :: Con Bool
+    Fls  :: Con Bool
+    Nil  :: EqShow a => Repr a -> Con [a]
+    Cons :: Con [a]
+    Jst  :: Con (Maybe a)
+    Ntng :: EqShow a => Repr a -> Con (Maybe a)
+    Tup  :: Con (a,b)
+
+infoCon' :: Con' -> (Int,String)
+infoCon' c = case c of
+    Si TT     -> (0,"()")
+    Si Zero   -> (1,"Zero")
+    Si Succ   -> (2,"Succ")
+    Si Nil{}  -> (3,"Nil")
+    Si Cons   -> (4,"Cons")
+    Si Pos    -> (5,"Pos")
+    Si Neg    -> (6,"Neg")
+    Si Jst    -> (7,"Just")
+    Si Ntng{} -> (8,"Nothing")
+    Si Tru    -> (9,"True")
+    Si Fls    -> (10,"False")
+    Si Tup    -> (11,"Tup")
+
+instance Eq Con' where
+    (==) = (==) `on` (fst . infoCon')
+
+instance Ord Con' where
+    compare = compare `on` (fst . infoCon')
+
+instance Show Con' where
+    show = snd . infoCon'
+
+instance Show (Exists a) where
+    show (Val _ x) = show x
+
+shrinkRepr' :: Repr' -> [Repr']
+shrinkRepr' (Val r x) = map (Val r) (shrink x)
+
+data Equal :: * -> * -> * where
+    Refl :: Equal a a
+
+(==?) :: Repr a -> Repr b -> Maybe (Equal a b)
+Unit      ==? Unit  = Just Refl
+Nat       ==? Nat   = Just Refl
+PInt      ==? PInt  = Just Refl
+Bool      ==? Bool  = Just Refl
+TyVar     ==? TyVar = Just Refl
+Maybe a   ==? Maybe b   | Just Refl <- a ==? b = Just Refl
+List a    ==? List b    | Just Refl <- a ==? b = Just Refl
+TupTy a u ==? TupTy b v | Just Refl <- a ==? b
+                        , Just Refl <- u ==? v = Just Refl
+_         ==? _     = Nothing
+
+instance Eq (Exists Repr) where
+    Val s u == Val t v = case s ==? t of
+        Just Refl -> u == v
+        Nothing   -> False
+
diff --git a/test/Nat.hs b/test/Nat.hs
new file mode 100644
--- /dev/null
+++ b/test/Nat.hs
@@ -0,0 +1,45 @@
+{-# OPTIONS_GHC -fno-warn-missing-methods #-}
+{-# LANGUAGE ViewPatterns #-}
+module Nat where
+
+import Test.QuickCheck
+
+-- A classic!
+data Nat = Z | S Nat deriving (Show,Eq)
+
+instance Arbitrary Nat where
+    arbitrary = sized $ \ s -> do
+        x <- choose (0,round (sqrt (toEnum s) :: Double))
+        return (nats !! x)
+
+    shrink (S n) = n : shrink n
+    shrink Z     = []
+
+nats :: [Nat]
+nats = iterate S Z
+
+-- warning: partial instance
+instance Num Nat where
+    fromInteger n = nats !! fromEnum n
+
+-- Another classic!
+data PInt = P Nat | N Nat
+  deriving (Show,Eq)
+
+p :: PInt -> Nat
+p (P n) = n
+p (N n) = n
+
+instance Arbitrary PInt where
+    arbitrary = do
+        (b,x) <- arbitrary
+        return $ if b then P x else N x
+
+    shrink (p -> n ) = map P (shrink n) ++ map N (shrink n)
+
+-- warning: partial instance
+instance Num PInt where
+    fromInteger x
+        | x < 0     = N (fromInteger (negate (x + 1)))
+        | otherwise = P (fromInteger x)
+
diff --git a/test/Trace.hs b/test/Trace.hs
new file mode 100644
--- /dev/null
+++ b/test/Trace.hs
@@ -0,0 +1,26 @@
+module Trace where
+
+import Data.List (find)
+import Control.Monad (mplus,msum)
+
+data Trace a = Fork a [Trace a]
+
+instance Show a => Show (Trace a) where
+    show = unlines . go
+      where
+        go (Fork x ts) = show x:bars (map go ts)
+
+        bar :: [String] -> [String]
+        bar [] = []
+        bar (s:xs) = ("┣┉" ++ s):map ("┃ " ++) xs
+
+        bars :: [[String]] -> [String]
+        bars [] = []
+        bars [s:xs] = ("┗┉" ++ s):map ("  " ++) xs
+        bars (x:xs) = bar x ++ bars xs
+
+loop :: Eq a => Trace a -> Maybe a
+loop = go []
+  where
+    go vis (Fork x ts) = find (x ==) vis `mplus` msum (map (go (x:vis)) ts)
+
diff --git a/test/Util.hs b/test/Util.hs
new file mode 100644
--- /dev/null
+++ b/test/Util.hs
@@ -0,0 +1,15 @@
+module Util where
+
+import Test.QuickCheck
+
+halfSize :: (Int -> Gen a) -> Gen a
+halfSize m = sized $ \s -> resize (s `div` 2) (m s)
+
+divSize :: Int -> (Int -> Gen a) -> Gen a
+divSize d m = sized $ \s -> resize (s `div` d) (m s)
+
+coordss :: Int -> Int -> [[Int]]
+coordss n _ | n < 0 = [[]]
+coordss 0 d = [replicate d 0]
+coordss n d = concat [ map (++ replicate t n) (coordss (n-1) (d-t)) | t <- [0..d] ]
+
diff --git a/test/Walk.hs b/test/Walk.hs
new file mode 100644
--- /dev/null
+++ b/test/Walk.hs
@@ -0,0 +1,62 @@
+{-# LANGUAGE GADTs, RankNTypes, TypeOperators, FlexibleInstances #-}
+module Walk where
+
+import Test.QuickCheck
+import Data.List
+import Control.Monad
+import Control.Applicative
+
+import Induction.Structural
+
+import Trace
+import EnvTypes
+import Env
+import Util
+
+construct :: VarMap -> Hyp -> Gen [Repr']
+construct vm (hyps,tms) = mapM (construct1 hyps vm) tms
+
+construct1 :: [(String,Ty')] -> VarMap -> Tm -> Gen Repr'
+construct1 hyps vm tm = case tm of
+    Var s -> case lookup s vm of
+        Just u  -> return u
+        Nothing -> case lookup s hyps of
+            Just t  -> arbFromType' t
+            -- ^ if this is missing, generate a new one with arbitrary!!
+            Nothing -> error $ show s ++ " missing!" ++ show vm ++ "," ++ show hyps
+    Con s tms ->  mkCon s <$> mapM (construct1 hyps vm) tms
+    Fun{} -> error "exponentials not supported"
+
+-- | We can only pick 1-2 hyps, otherwise we get crazy exponential behaviour
+pickHyps :: [a] -> Gen [a]
+pickHyps [] = return []
+pickHyps hs = do
+    let n = length hs - 1
+    i <- choose (0,n)
+    i' <- choose (0,n)
+    two <- arbitrary
+    return $ if two && i /= i' then [hs !! i,hs !! i'] else [hs !! i]
+
+-- TODO: Can this be reorganized so we get an efficient unrolling?
+makeTracer :: [Repr'] -> [Oblig] -> Gen (Trace [Repr'])
+makeTracer args parts = go parts
+  where
+    go p = case p of
+        Obligation _ hyps conc:is
+            | length args == length conc -> case zipWithM match args conc of
+                Nothing -> go is
+                Just vms -> halfSize $ \ _ -> do
+                    -- Throw away some hypotheses
+                    hyps' <- pickHyps hyps
+                    argss' <- mapM (construct (concat vms)) hyps'
+                    forks <- mapM (`makeTracer` parts) argss'
+                    return (Fork args forks)
+            | otherwise -> mk_error $ "Unequal lengths (conc=" ++
+                intercalate "," (map (render . linTerm style) conc) ++ ")"
+        _ -> mk_error "No case"
+      where
+        mk_error msg = error $
+            "makeTracer " ++ show args ++ " : " ++ msg ++ "!" ++
+            "\nDetails: args = (" ++ intercalate " , " (map showRepr' args) ++ ")" ++
+            "\nCheck Env.match and EnvTypes.==?, or case is missing from schema:" ++
+            "\n" ++ showOblig parts