diff --git a/constrained-generators.cabal b/constrained-generators.cabal
index b23fc0d..0998370 100644
--- a/constrained-generators.cabal
+++ b/constrained-generators.cabal
@@ -15,6 +15,11 @@ source-repository head
   type: git
   location: https://github.com/input-output-hk/constrained-generators
 
+flag devel
+  description:       Enable development mode
+  default:           False
+  manual:            True
+
 library
   exposed-modules:
     Constrained.API
@@ -46,6 +51,23 @@ library
     Constrained.TypeErrors
 
   hs-source-dirs: src
+
+  if flag(devel)
+    exposed-modules:
+      Constrained.Examples
+      Constrained.Examples.Basic
+      Constrained.Examples.BinTree
+      Constrained.Examples.CheatSheet
+      Constrained.Examples.Either
+      Constrained.Examples.Fold
+      Constrained.Examples.List
+      Constrained.Examples.ManualExamples
+      Constrained.Examples.Map
+      Constrained.Examples.Set
+      Constrained.Examples.Tree
+
+    hs-source-dirs: examples
+
   default-language: Haskell2010
   ghc-options:
     -Wall
diff --git a/examples/Constrained/Examples/Basic.hs b/examples/Constrained/Examples/Basic.hs
index f9ce5db..5ca680a 100644
--- a/examples/Constrained/Examples/Basic.hs
+++ b/examples/Constrained/Examples/Basic.hs
@@ -319,3 +319,27 @@ wtfSpec = constrained' $ \ [var| options |] [var| mpair |] ->
         , assert $ unit ==. lit ()
         ]
     )
+
+manyInconsistent :: Specification (Int, Int, Int, Int, Int, Int)
+manyInconsistent = constrained' $ \ [var| a |] b c d e [var| f |] ->
+  [ assert $ a <. 10
+  , assert $ b >. a
+  , assert $ c >. b
+  , assert $ d >. c
+  , assert $ e >. d
+  , f `dependsOn` e
+  , assert $ f >. 10
+  , assert $ f <. a
+  ]
+
+manyInconsistentTrans :: Specification (Int, Int, Int, Int, Int, Int)
+manyInconsistentTrans = constrained' $ \ [var| a |] [var| b |] c d e [var| f |] ->
+  [ assert $ a <. 10
+  , assert $ b <. a
+  , assert $ c >. b
+  , assert $ d >. c
+  , assert $ e >. d
+  , f `dependsOn` e
+  , assert $ f >. 10
+  , assert $ f <. b
+  ]
diff --git a/examples/Constrained/Examples/Map.hs b/examples/Constrained/Examples/Map.hs
index 07ea177..2d71019 100644
--- a/examples/Constrained/Examples/Map.hs
+++ b/examples/Constrained/Examples/Map.hs
@@ -125,3 +125,16 @@ mapSetSmall = constrained $ \x ->
 mapIsJust :: Specification (Int, Int)
 mapIsJust = constrained' $ \ [var| x |] [var| y |] ->
   just_ x ==. lookup_ y (lit $ Map.fromList [(z, z) | z <- [100 .. 102]])
+
+eitherKeys :: Specification ([Int], [Int], Map (Either Int Int) Int)
+eitherKeys = constrained' $ \ [var| as |] [var| bs |] [var| m |] ->
+  [
+    forAll' m $ \ [var| k |] _v ->
+      [ caseOn k
+          (branch $ \ a -> a `elem_` as)
+          (branch $ \ b -> b `elem_` bs)
+      , reify as (map Left) $ \ ls ->
+        reify bs (map Right) $ \ rs ->
+          k `elem_` ls ++. rs
+      ]
+  ]
diff --git a/src/Constrained/AbstractSyntax.hs b/src/Constrained/AbstractSyntax.hs
index efc33c9..4efe15c 100644
--- a/src/Constrained/AbstractSyntax.hs
+++ b/src/Constrained/AbstractSyntax.hs
@@ -134,6 +134,7 @@ fastInequality _ _ = True
 class Syntax (t :: [Type] -> Type -> Type) where
   isInfix :: t dom rng -> Bool
   isInfix _ = False
+
   prettySymbol ::
     forall deps dom rng ann.
     t dom rng ->
@@ -305,10 +306,9 @@ instance Pretty (PredD deps) where
         sep
           [ "memberPred"
           , pretty term
-          , "(" <> viaShow (length vs) <> " items)"
-          , brackets (fillSep (punctuate "," (map viaShow (NE.toList vs))))
+          , prettyShowList (NE.toList vs)
           ]
-    ElemPred False term vs -> align $ sep ["notMemberPred", pretty term, fillSep (punctuate "," (map viaShow (NE.toList vs)))]
+    ElemPred False term vs -> align $ sep ["notMemberPred", pretty term, prettyShowList (NE.toList vs)]
     Exists _ (x :-> p) -> align $ sep ["exists" <+> viaShow x <+> "in", pretty p]
     Let t (x :-> p) -> align $ sep ["let" <+> viaShow x <+> "=" /> pretty t <+> "in", pretty p]
     And ps -> braces $ vsep' $ map pretty ps
@@ -377,7 +377,7 @@ instance (Show a, Typeable a, Show (TypeSpecD deps a)) => Pretty (WithPrec (Spec
     ExplainSpec es z -> "ExplainSpec" <+> viaShow es <+> "$" /> pretty z
     ErrorSpec es -> "ErrorSpec" /> vsep' (map fromString (NE.toList es))
     TrueSpec -> fromString $ "TrueSpec @(" ++ showType @a ++ ")"
-    MemberSpec xs -> "MemberSpec" <+> short (NE.toList xs)
+    MemberSpec xs -> "MemberSpec" <+> prettyShowList (NE.toList xs)
     SuspendedSpec x p -> parensIf (d > 10) $ "constrained $ \\" <+> viaShow x <+> "->" /> pretty p
     -- TODO: require pretty for `TypeSpec` to make this much nicer
     TypeSpecD ts cant ->
@@ -385,7 +385,7 @@ instance (Show a, Typeable a, Show (TypeSpecD deps a)) => Pretty (WithPrec (Spec
         "TypeSpec"
           /> vsep
             [ fromString (showsPrec 11 ts "")
-            , viaShow cant
+            , prettyShowList cant
             ]
 
 instance (Show a, Typeable a, Show (TypeSpecD deps a)) => Pretty (SpecificationD deps a) where
diff --git a/src/Constrained/Base.hs b/src/Constrained/Base.hs
index e63724c..876a268 100644
--- a/src/Constrained/Base.hs
+++ b/src/Constrained/Base.hs
@@ -99,7 +99,6 @@ import Constrained.FunctionSymbol
 import Constrained.GenT
 import Constrained.Generic
 import Constrained.List hiding (toList)
-import Constrained.PrettyUtils
 import Constrained.TypeErrors
 import Control.Monad.Writer (
   Writer,
@@ -671,8 +670,6 @@ instance Show (BaseW d r) where
   show FromGenericW = "fromSimpleRep"
 
 instance Syntax BaseW where
-  prettySymbol ToGenericW (x :> Nil) p = Just $ "to" <+> pretty (WithPrec p x)
-  prettySymbol FromGenericW (x :> Nil) p = Just $ "from" <+> pretty (WithPrec p x)
 
 instance Semantics BaseW where
   semantics FromGenericW = fromSimpleRep
diff --git a/src/Constrained/Env.hs b/src/Constrained/Env.hs
index 0e9beaa..06bbba3 100644
--- a/src/Constrained/Env.hs
+++ b/src/Constrained/Env.hs
@@ -1,4 +1,6 @@
 {-# LANGUAGE DerivingVia #-}
+{-# LANGUAGE ImpredicativeTypes #-}
+{-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE ImportQualifiedPost #-}
@@ -13,6 +15,7 @@ module Constrained.Env (
   lookup,
   find,
   remove,
+  filterKeys,
 ) where
 
 import Constrained.Core
@@ -34,7 +37,7 @@ data EnvValue where
 deriving instance Show EnvValue
 
 data EnvKey where
-  EnvKey :: !(Var a) -> EnvKey
+  EnvKey :: Typeable a => !(Var a) -> EnvKey
 
 instance Eq EnvKey where
   EnvKey v == EnvKey v' = nameOf v == nameOf v'
@@ -50,7 +53,7 @@ extend :: (Typeable a, Show a) => Var a -> a -> Env -> Env
 extend v a (Env m) = Env $ Map.insert (EnvKey v) (EnvValue a) m
 
 -- | Remove a variable from an environment if it exists
-remove :: Var a -> Env -> Env
+remove :: Typeable a => Var a -> Env -> Env
 remove v (Env m) = Env $ Map.delete (EnvKey v) m
 
 -- | Create a singleton environment
@@ -70,13 +73,18 @@ find env var = do
     Just a -> pure a
     Nothing -> genError ("Couldn't find " ++ show var ++ " in " ++ show env)
 
+-- | Filter the keys in an env, useful for removing irrelevant variables in
+-- error messages
+filterKeys :: Env -> (forall a. Typeable a => Var a -> Bool) -> Env
+filterKeys (Env m) f = Env $ Map.filterWithKey (\ (EnvKey k) _ -> f k) m
+
 instance Pretty EnvValue where
-  pretty (EnvValue x) = pretty $ take 80 (show x)
+  pretty (EnvValue x) = viaShow x
 
 instance Pretty EnvKey where
   pretty (EnvKey x) = viaShow x
 
 instance Pretty Env where
-  pretty (Env m) = vsep ("Env" : (map f (Map.toList m)))
+  pretty (Env m) = vsep (map f (Map.toList m))
     where
       f (k, v) = hsep [pretty k, "->", pretty v]
diff --git a/src/Constrained/Generation.hs b/src/Constrained/Generation.hs
index 61e7307..3f4c6db 100644
--- a/src/Constrained/Generation.hs
+++ b/src/Constrained/Generation.hs
@@ -27,7 +27,7 @@ module Constrained.Generation (
   shrinkWithSpec,
   simplifySpec,
 
-  -- ** Debuggin
+  -- ** Debugging
   printPlan,
   debugSpec,
   prettyPlan,
@@ -121,7 +121,7 @@ genFromSpecT (simplifySpec -> spec) = case spec of
           [ "genFromSpecT on (TypeSpec tspec cant) at type " ++ showType @a
           , "tspec = "
           , show s
-          , "cant = " ++ show (short cant)
+          , "cant = " ++ show cant
           , "with mode " ++ show mode
           ]
       )
@@ -194,11 +194,15 @@ prettyPlan (simplifySpec -> spec)
 
 -- ---------------------- Building a plan -----------------------------------
 
-substStage :: Env -> SolverStage -> SolverStage
-substStage env (SolverStage y ps spec) = normalizeSolverStage $ SolverStage y (substPred env <$> ps) spec
+substStage :: HasSpec a => Set Name -> Var a -> a -> SolverStage -> SolverStage
+substStage rel' x val (SolverStage y ps spec relevant) =
+  normalizeSolverStage $ SolverStage y (substPred env <$> ps) spec relevant'
+  where env = Env.singleton x val
+        relevant' | Name x `appearsIn` ps = rel' <> relevant
+                  | otherwise = relevant
 
 normalizeSolverStage :: SolverStage -> SolverStage
-normalizeSolverStage (SolverStage x ps spec) = SolverStage x ps'' (spec <> spec')
+normalizeSolverStage (SolverStage x ps spec relevant) = SolverStage x ps'' (spec <> spec') relevant
   where
     (ps', ps'') = partition ((1 ==) . Set.size . freeVarSet) ps
     spec' = fromGESpec $ computeSpec x (And ps')
@@ -228,7 +232,7 @@ prepareLinearization p = do
           ]
       )
       $ linearize preds graph
-  pure $ backPropagation $ SolverPlan plan graph
+  pure $ backPropagation mempty $ SolverPlan plan
 
 -- | Flatten nested `Let`, `Exists`, and `And` in a `Pred fn`. `Let` and
 -- `Exists` bound variables become free in the result.
@@ -300,7 +304,7 @@ linearize preds graph = do
               ]
     go (n@(Name x) : ns) ps = do
       let (nps, ops) = partition (isLastVariable n . fst) ps
-      (normalizeSolverStage (SolverStage x (map snd nps) mempty) :) <$> go ns ops
+      (normalizeSolverStage (SolverStage x (map snd nps) mempty mempty):) <$> go ns ops
 
     isLastVariable n set = n `Set.member` set && solvableFrom n (Set.delete n set) graph
 
@@ -823,98 +827,75 @@ totalWeight = fmap getSum . foldMapList (fmap Semigroup.Sum . weight)
 
 -- | Does nothing if the variable is not in the plan already.
 mergeSolverStage :: SolverStage -> [SolverStage] -> [SolverStage]
-mergeSolverStage (SolverStage x ps spec) plan =
+mergeSolverStage (SolverStage x ps spec relevant) plan =
   [ case eqVar x y of
       Just Refl ->
-        SolverStage
-          y
-          (ps ++ ps')
-          ( addToErrorSpec
-              ( NE.fromList
-                  ( [ "Solving var " ++ show x ++ " fails."
-                    , "Merging the Specs"
-                    , "   1. " ++ show spec
-                    , "   2. " ++ show spec'
-                    ]
-                  )
-              )
-              (spec <> spec')
-          )
+        normalizeSolverStage $ SolverStage
+            y
+            (ps ++ ps')
+            ( addToErrorSpec
+                ( NE.fromList
+                    ( [ "Solving var " ++ show x ++ " fails."
+                      , "Merging the Specs"
+                      , "   1. " ++ show spec
+                      , "   2. " ++ show spec'
+                      ]
+                    )
+                )
+                (spec <> spec')
+            )
+            (relevant <> relevant')
       Nothing -> stage
-  | stage@(SolverStage y ps' spec') <- plan
+  | stage@(SolverStage y ps' spec' relevant') <- plan
   ]
 
 isEmptyPlan :: SolverPlan -> Bool
-isEmptyPlan (SolverPlan plan _) = null plan
-
-stepPlan :: MonadGenError m => Env -> SolverPlan -> GenT m (Env, SolverPlan)
-stepPlan env plan@(SolverPlan [] _) = pure (env, plan)
-stepPlan env (SolverPlan (SolverStage (x :: Var a) ps spec : pl) gr) = do
-  (spec', specs) <- runGE
-    $ explain
-      ( show
-          ( "Computing specs for variable "
-              <> pretty x
-                /> vsep' (map pretty ps)
-          )
-      )
-    $ do
-      ispecs <- mapM (computeSpec x) ps
-      pure $ (fold ispecs, ispecs)
-  val <-
-    genFromSpecT
-      ( addToErrorSpec
-          ( NE.fromList
-              ( ( "\nStepPlan for variable: "
-                    ++ show x
-                    ++ "::"
-                    ++ showType @a
-                    ++ " fails to produce Specification, probably overconstrained."
-                    ++ "PS = "
-                    ++ unlines (map show ps)
-                )
-                  : ("Original spec " ++ show spec)
-                  : "Predicates"
-                  : zipWith
-                    (\pred specx -> "  pred " ++ show pred ++ " -> " ++ show specx)
-                    ps
-                    specs
-              )
-          )
-          (spec <> spec')
-      )
-  let env1 = Env.extend x val env
-  pure (env1, backPropagation $ SolverPlan (substStage env1 <$> pl) (deleteNode (Name x) gr))
+isEmptyPlan (SolverPlan plan) = null plan
+
+stepPlan :: MonadGenError m => SolverPlan -> Env -> SolverPlan -> GenT m (Env, SolverPlan)
+stepPlan _ env plan@(SolverPlan []) = pure (env, plan)
+stepPlan (SolverPlan origStages) env (SolverPlan (stage@(SolverStage (x :: Var a) ps spec relevant) : pl)) = do
+  let errorMessage = "Failed to step the plan" />
+                        vsep [ "Relevant parts of the original plan:" //> pretty narrowedOrigPlan
+                             , "Already generated variables:" //> pretty narrowedEnv
+                             , "Current stage:" //> pretty stage
+                             ]
+      relevant' = Set.insert (Name x) relevant
+      narrowedOrigPlan = SolverPlan $ [ st | st@(SolverStage v _ _ _) <- origStages, Name v `Set.member` relevant' ]
+      narrowedEnv = Env.filterKeys env (\v -> nameOf v `Set.member` (Set.map (\ (Name n) -> nameOf n) relevant'))
+  explain (show errorMessage) $ do
+    when (isErrorLike spec) $
+      genError "The specification in the current stage is unsatisfiable, giving up."
+    when (not $ null ps) $
+      fatalError "Something went wrong and not all predicates have been discharged. Report this as a bug in Constrained.Generation"
+    val <- genFromSpecT spec
+    let env1 = Env.extend x val env
+    pure (env1, backPropagation relevant' $ SolverPlan (substStage relevant' x val <$> pl) )
 
 -- | Generate a satisfying `Env` for a `p : Pred fn`. The `Env` contains values for
 -- all the free variables in `flattenPred p`.
 genFromPreds :: forall m. MonadGenError m => Env -> Pred -> GenT m Env
 -- TODO: remove this once optimisePred does a proper fixpoint computation
-genFromPreds env0 (optimisePred . optimisePred -> preds) =
-  {- explain1 (show $ "genFromPreds fails\nPreds are:" /> pretty preds) -} do
+genFromPreds env0 (optimisePred . optimisePred -> preds) = do
     -- NOTE: this is just lazy enough that the work of flattening,
     -- computing dependencies, and linearizing is memoized in
     -- properties that use `genFromPreds`.
-    plan <- runGE $ prepareLinearization preds
-    go env0 plan
+    origPlan <- runGE $ prepareLinearization preds
+    let go :: Env -> SolverPlan -> GenT m Env
+        go env plan | isEmptyPlan plan = pure env
+        go env plan = do
+          (env', plan') <- stepPlan origPlan env plan
+          go env' plan'
+    go env0 origPlan
   where
-    go :: Env -> SolverPlan -> GenT m Env
-    go env plan | isEmptyPlan plan = pure env
-    go env plan = do
-      (mess :: String) <- (unlines . map NE.head) <$> getMessages
-      (env', plan') <-
-        explain (show (fromString (mess ++ "Stepping the plan:") /> vsep [pretty plan, pretty env])) $
-          stepPlan env plan
-      go env' plan'
 
 -- | Push as much information we can backwards through the plan.
-backPropagation :: SolverPlan -> SolverPlan
--- backPropagation (SolverPlan _plan _graph) =
-backPropagation (SolverPlan initplan graph) = SolverPlan (go [] (reverse initplan)) graph
+backPropagation :: Set Name -> SolverPlan -> SolverPlan
+backPropagation relevant (SolverPlan initplan) = SolverPlan (go [] (reverse initplan))
   where
     go :: [SolverStage] -> [SolverStage] -> [SolverStage]
     go acc [] = acc
-    go acc (s@(SolverStage (x :: Var a) ps spec) : plan) = go (s : acc) plan'
+    go acc (s@(SolverStage (x :: Var a) ps spec _) : plan) = go (s : acc) plan'
       where
         newStages = concatMap (newStage spec) ps
         plan' = foldr mergeSolverStage plan newStages
@@ -928,12 +909,14 @@ backPropagation (SolverPlan initplan graph) = SolverPlan (go [] (reverse initpla
         termVarEqCases :: HasSpec b => Specification a -> Var b -> Term b -> [SolverStage]
         termVarEqCases (MemberSpec vs) x' t
           | Set.singleton (Name x) == freeVarSet t =
-              [SolverStage x' [] $ MemberSpec (NE.nub (fmap (\v -> errorGE $ runTerm (Env.singleton x v) t) vs))]
+              [SolverStage x' [] (MemberSpec (NE.nub (fmap (\v -> errorGE $ runTerm (Env.singleton x v) t) vs)))
+               (Set.insert (Name x') relevant)]
         termVarEqCases specx x' t
           | Just Refl <- eqVar x x'
           , [Name y] <- Set.toList $ freeVarSet t
           , Result ctx <- toCtx y t =
-              [SolverStage y [] (propagateSpec specx ctx)]
+              [SolverStage y [] (propagateSpec specx ctx)
+               (Set.insert (Name x') relevant)]
         termVarEqCases _ _ _ = []
 
 -- | Function symbols for `(==.)`
@@ -1027,10 +1010,11 @@ pinnedBy _ _ = Nothing
 --      assert $ just_ x ==. lookup_ y (lit $ Map.fromList [(z, z) | z <- [100 .. 102]])
 
 -- Without this code the example wouldn't work because `y` is completely unconstrained during
--- generation. With this code we essentially rewrite occurences of `just_ A == B` to
--- `[cJust A == B, case B of Nothing -> False; Just _ -> True]` to add extra information
+-- generation. With this code we _essentially_ rewrite occurences of `just_ A == B` to
+-- `[just_ A == B, case B of Nothing -> False; Just _ -> True]` to add extra information
 -- about the variables in `B`. Consequently, `y` in the example above is
--- constrained to `MemberSpec [100 .. 102]` in the plan.
+-- constrained to `MemberSpec [100 .. 102]` in the plan. This is implemented using the `saturate`
+-- function in the logic type class - in the example above for `==`.
 saturatePred :: Pred -> [Pred]
 saturatePred p =
   -- [p]
@@ -1309,6 +1293,7 @@ data SolverStage where
     { stageVar :: Var a
     , stagePreds :: [Pred]
     , stageSpec :: Specification a
+    , relevantVariables :: Set Name
     } ->
     SolverStage
 
@@ -1323,20 +1308,14 @@ instance Pretty SolverStage where
           ( [pretty stageSpec | not $ isTrueSpec stageSpec]
               ++ ["---" | not $ null stagePreds, not $ isTrueSpec stageSpec]
               ++ map pretty stagePreds
+              ++ ["_" | null stagePreds && isTrueSpec stageSpec]
           )
 
-data SolverPlan = SolverPlan
-  { solverPlan :: [SolverStage]
-  , solverDependencies :: Graph Name
-  }
+newtype SolverPlan = SolverPlan { solverPlan :: [SolverStage] }
 
 instance Pretty SolverPlan where
   pretty SolverPlan {..} =
-    "\nSolverPlan"
-      /> vsep'
-        [ -- "\nDependencies:" /> pretty solverDependencies, -- Might be usefull someday
-          "\nLinearization:" /> prettyLinear solverPlan
-        ]
+    "SolverPlan" /> prettyLinear solverPlan
 
 isTrueSpec :: Specification a -> Bool
 isTrueSpec TrueSpec = True
diff --git a/src/Constrained/PrettyUtils.hs b/src/Constrained/PrettyUtils.hs
index e8598b5..29771b3 100644
--- a/src/Constrained/PrettyUtils.hs
+++ b/src/Constrained/PrettyUtils.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ImportQualifiedPost #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE GADTs #-}
@@ -15,19 +16,23 @@ module Constrained.PrettyUtils (
   parensIf,
   prettyPrec,
 
-  -- * Lists
+  -- * Lists and sets
   ppList,
   ppListC,
+  prettyShowSet,
+  prettyShowList,
 
   -- * General helpers
   prettyType,
   vsep',
   (/>),
+  (//>),
   showType,
-  short,
 ) where
 
 import Constrained.List
+import Data.Set (Set)
+import Data.Set qualified as Set
 import Data.String (fromString)
 import Data.Typeable
 import Prettyprinter
@@ -58,6 +63,12 @@ ppListC ::
 ppListC _ Nil = []
 ppListC pp (a :> as) = pp a : ppListC @c pp as
 
+prettyShowSet :: Show a => Set a -> Doc ann
+prettyShowSet xs = fillSep $ "{" : punctuate "," (map viaShow (Set.toList xs)) ++ ["}"]
+
+prettyShowList :: Show a => [a] -> Doc ann
+prettyShowList xs = fillSep $ "[" : punctuate "," (map viaShow xs) ++ ["]"]
+
 -- | Pretty-print a type
 prettyType :: forall t x. Typeable t => Doc x
 prettyType = fromString $ show (typeRep (Proxy @t))
@@ -73,26 +84,13 @@ h /> cont = hang 2 $ sep [h, align cont]
 
 infixl 5 />
 
+-- | Lay the header (first argument) out above the body
+-- and and indent the body by 2
+(//>) :: Doc ann -> Doc ann -> Doc ann
+h //> cont = hang 2 $ vsep [h, align cont]
+
+infixl 5 //>
+
 -- | Show a `Typeable` thing's type
 showType :: forall t. Typeable t => String
 showType = show (typeRep (Proxy @t))
-
--- | Set to True if you need to see everything while debugging
-verboseShort :: Bool
-verboseShort = True
-
--- | Pretty-print a short list in full and truncate longer lists
-short :: forall a x. (Show a, Typeable a) => [a] -> Doc x
-short [] = "[]"
-short [x] =
-  let raw = show x
-      refined = if length raw <= 20 || verboseShort then raw else take 20 raw ++ " ... "
-   in "[" <+> fromString refined <+> "]"
-short xs =
-  if verboseShort
-    then fromString $ unlines (map show xs)
-    else
-      let raw = show xs
-       in if length raw <= 50
-            then fromString raw
-            else "([" <+> viaShow (length xs) <+> "elements ...] @" <> prettyType @a <> ")"
diff --git a/src/Constrained/Spec/List.hs b/src/Constrained/Spec/List.hs
index 4025391..381a24f 100644
--- a/src/Constrained/Spec/List.hs
+++ b/src/Constrained/Spec/List.hs
@@ -358,8 +358,8 @@ instance Semantics ListW where
   semantics AppendW = (++)
 
 instance Syntax ListW where
-  prettySymbol AppendW (Lit n :> y :> Nil) p = Just $ parensIf (p > 10) $ "append_" <+> short n <+> prettyPrec 10 y
-  prettySymbol AppendW (y :> Lit n :> Nil) p = Just $ parensIf (p > 10) $ "append_" <+> prettyPrec 10 y <+> short n
+  prettySymbol AppendW (Lit n :> y :> Nil) p = Just $ parensIf (p > 10) $ "append_" <+> prettyShowList n <+> prettyPrec 10 y
+  prettySymbol AppendW (y :> Lit n :> Nil) p = Just $ parensIf (p > 10) $ "append_" <+> prettyPrec 10 y <+> prettyShowList n
   prettySymbol _ _ _ = Nothing
 
 instance Show (ListW d r) where
diff --git a/src/Constrained/Spec/Set.hs b/src/Constrained/Spec/Set.hs
index 336a606..c81e0b5 100644
--- a/src/Constrained/Spec/Set.hs
+++ b/src/Constrained/Spec/Set.hs
@@ -87,7 +87,7 @@ prettySetSpec :: HasSpec a => SetSpec a -> Doc ann
 prettySetSpec (SetSpec must elemS size) =
   parens
     ( "SetSpec"
-        /> sep ["must=" <> short (Set.toList must), "elem=" <> pretty elemS, "size=" <> pretty size]
+        /> sep ["must=" <> viaShow (Set.toList must), "elem=" <> pretty elemS, "size=" <> pretty size]
     )
 
 instance HasSpec a => Show (SetSpec a) where
@@ -163,7 +163,7 @@ instance (Ord a, HasSpec a) => HasSpec (Set a) where
       ( NE.fromList
           [ "Choose size = " ++ show chosenSize
           , "szSpec' = " ++ show szSpec'
-          , "Picking items not in must = " ++ show (short (Set.toList must))
+          , "Picking items not in must = " ++ show (Set.toList must)
           , "that also meet the element test: "
           , "  " ++ show elemS
           ]
@@ -251,13 +251,13 @@ instance Semantics SetW where
   semantics = setSem
 
 instance Syntax SetW where
-  prettySymbol SubsetW (Lit n :> y :> Nil) p = Just $ parensIf (p > 10) $ "subset_" <+> short (Set.toList n) <+> prettyPrec 10 y
-  prettySymbol SubsetW (y :> Lit n :> Nil) p = Just $ parensIf (p > 10) $ "subset_" <+> prettyPrec 10 y <+> short (Set.toList n)
-  prettySymbol DisjointW (Lit n :> y :> Nil) p = Just $ parensIf (p > 10) $ "disjoint_" <+> short (Set.toList n) <+> prettyPrec 10 y
-  prettySymbol DisjointW (y :> Lit n :> Nil) p = Just $ parensIf (p > 10) $ "disjoint_" <+> prettyPrec 10 y <+> short (Set.toList n)
-  prettySymbol UnionW (Lit n :> y :> Nil) p = Just $ parensIf (p > 10) $ "union_" <+> short (Set.toList n) <+> prettyPrec 10 y
-  prettySymbol UnionW (y :> Lit n :> Nil) p = Just $ parensIf (p > 10) $ "union_" <+> prettyPrec 10 y <+> short (Set.toList n)
-  prettySymbol MemberW (y :> Lit n :> Nil) p = Just $ parensIf (p > 10) $ "member_" <+> prettyPrec 10 y <+> short (Set.toList n)
+  prettySymbol SubsetW (Lit n :> y :> Nil) p = Just $ parensIf (p > 10) $ "subset_" <+> prettyShowSet n <+> prettyPrec 10 y
+  prettySymbol SubsetW (y :> Lit n :> Nil) p = Just $ parensIf (p > 10) $ "subset_" <+> prettyPrec 10 y <+> prettyShowSet n
+  prettySymbol DisjointW (Lit n :> y :> Nil) p = Just $ parensIf (p > 10) $ "disjoint_" <+> prettyShowSet n <+> prettyPrec 10 y
+  prettySymbol DisjointW (y :> Lit n :> Nil) p = Just $ parensIf (p > 10) $ "disjoint_" <+> prettyPrec 10 y <+> prettyShowSet n
+  prettySymbol UnionW (Lit n :> y :> Nil) p = Just $ parensIf (p > 10) $ "union_" <+> prettyShowSet n <+> prettyPrec 10 y
+  prettySymbol UnionW (y :> Lit n :> Nil) p = Just $ parensIf (p > 10) $ "union_" <+> prettyPrec 10 y <+> prettyShowSet n
+  prettySymbol MemberW (y :> Lit n :> Nil) p = Just $ parensIf (p > 10) $ "member_" <+> prettyPrec 10 y <+> prettyShowSet n
   prettySymbol _ _ _ = Nothing
 
 instance (Ord a, HasSpec a, HasSpec (Set a)) => Semigroup (Term (Set a)) where
diff --git a/test/Constrained/Tests.hs b/test/Constrained/Tests.hs
index b0d7bbf..976bfc0 100644
--- a/test/Constrained/Tests.hs
+++ b/test/Constrained/Tests.hs
@@ -85,6 +85,7 @@ tests nightly =
     testSpec "mapElemKeySpec" mapElemKeySpec
     -- TODO: double shrinking
     testSpecNoShrink "mapIsJust" mapIsJust
+    testSpecNoShrink "eitherKeys" eitherKeys
     testSpecNoShrink "intSpec" intSpec
     testSpecNoShrink "mapPairSpec" mapPairSpec
     testSpecNoShrink "mapEmptyDomainSpec" mapEmptyDomainSpec
@@ -235,6 +236,8 @@ negativeTests =
     testSpecFail "overconstrainedPrefixes" overconstrainedPrefixes
     testSpecFail "overconstrainedSuffixes" overconstrainedSuffixes
     testSpecFail "appendForAllBad" appendForAllBad
+    testSpecFail "manyInconsistent" manyInconsistent
+    testSpecFail "manyInconsistentTrans" manyInconsistentTrans
 
 testSpecFail :: HasSpec a => String -> Specification a -> Spec
 testSpecFail s spec =