diff --git a/libs/base/Data/SnocList.idr b/libs/base/Data/SnocList.idr
index 73a35350a..68964dc06 100644
--- a/libs/base/Data/SnocList.idr
+++ b/libs/base/Data/SnocList.idr
@@ -156,6 +156,31 @@ findIndex p (xs :< x) = if p x
   then Just FZ
   else FS <$> findIndex p xs
 
+---------------------------
+-- Zippable --
+---------------------------
+
+public export
+Zippable SnocList where
+  zipWith _ [<] _ = [<]
+  zipWith _ _ [<] = [<]
+  zipWith f (xs :< x) (ys :< y) = zipWith f xs ys :< f x y
+
+  zipWith3 _ [<] _ _ = [<]
+  zipWith3 _ _ [<] _ = [<]
+  zipWith3 _ _ _ [<] = [<]
+  zipWith3 f (xs :< x) (ys :< y) (zs :< z) = zipWith3 f xs ys zs :< f x y z
+
+  unzipWith f [<] = ([<], [<])
+  unzipWith f (xs :< x) = let (bs, cs) = unzipWith f xs
+                              (b, c) = f x
+                          in (bs :< b, cs :< c)
+
+  unzipWith3 f [<] = ([<], [<], [<])
+  unzipWith3 f (xs :< x) = let (bs, cs, ds) = unzipWith3 f xs
+                               (b, c, d) = f x
+                           in  (bs :< b, cs :< c, ds :< d)
+
 ------------------
 --- Properties ---
 ------------------
diff --git a/libs/base/Deriving/Common.idr b/libs/base/Deriving/Common.idr
index 90c49dc7c..c002b6283 100644
--- a/libs/base/Deriving/Common.idr
+++ b/libs/base/Deriving/Common.idr
@@ -1,5 +1,6 @@
 module Deriving.Common
 
+import Data.SnocList
 import Language.Reflection
 
 %default total
@@ -64,7 +65,7 @@ isType : Elaboration m => TTImp -> m IsType
 isType = go Z [] where
 
   go : Nat -> List (Argument Name, Nat) -> TTImp -> m IsType
-  go idx acc (IVar _ n) = MkIsType n acc <$> isTypeCon n
+  go idx acc (IVar _ n) = MkIsType n (map (map (minus idx . S)) acc) <$> isTypeCon n
   go idx acc (IApp _ t (IVar _ nm)) = case nm of
     -- Unqualified: that's a local variable
     UN (Basic _) => go (S idx) ((Arg emptyFC nm, idx) :: acc) t
@@ -86,8 +87,7 @@ isType = go Z [] where
 public export
 record ConstructorView where
   constructor MkConstructorView
-  params      : List Name
-  functorPara : Name
+  params      : SnocList (Name, Nat)
   conArgTypes : List (Count, Argument TTImp)
 
 export
@@ -98,13 +98,13 @@ constructorView (IPi fc rig pinfo x a b) = do
   let True = rig /= M1
     | False => constructorView b -- this better be another boring argument...
   { conArgTypes $= ((rig, arg) ::) } <$> constructorView b
-constructorView (IApp _ f (IVar _ a)) = do
+constructorView f = do
   MkAppView _ ts _ <- appView f
-  let ps = flip mapMaybe ts $ \ t => the (Maybe Name) $ case t of
-             Arg _ (IVar _ nm) => Just nm
+  let range = [<] <>< [0..minus (length ts) 1]
+  let ps = flip mapMaybe (zip ts range) $ \ t => the (Maybe (Name, Nat)) $ case t of
+             (Arg _ (IVar _ nm), n) => Just (nm, n)
              _ => Nothing
-  pure (MkConstructorView (ps <>> []) a [])
-constructorView _ = Nothing
+  pure (MkConstructorView ps [])
 
 ------------------------------------------------------------------------------
 -- Satisfying an interface
@@ -131,6 +131,32 @@ withParams fc params nms t = go nms where
     $ addConstraint (params pos) nm
     $ go nms
 
+||| Type of proofs that something has a given type
+export
+data HasType : (nm : Name) -> (ty : TTImp) -> Type where
+  TrustMeHT : HasType nm ty
+
+export
+hasType : Elaboration m => (nm : Name) ->
+          m (Maybe (ty : TTImp ** HasType nm ty))
+hasType nm = catch $ do
+  [(_, ty)] <- getType nm
+    | _ => fail "Ambiguous name"
+  pure (ty ** TrustMeHT)
+
+||| Type of proofs that a type is inhabited
+export
+data IsProvable : (ty : TTImp) -> Type where
+  TrustMeIP : IsProvable ty
+
+export
+isProvable : Elaboration m => (ty : TTImp) ->
+             m (Maybe (IsProvable ty))
+isProvable ty = catch $ do
+  ty <- check {expected = Type} ty
+  ignore $ check {expected = ty} `(%search)
+  pure TrustMeIP
+
 ||| Type of proofs that a type satisfies a constraint.
 ||| Internally it's vacuous. We don't export the constructor so
 ||| that users cannot manufacture buggy proofs.
@@ -196,14 +222,3 @@ freshName ns a = assert_total $ go (basicNames ns) Nothing where
   go ns mi =
     let nm = a ++ maybe "" show mi in
     ifThenElse (nm `elem` ns) (go ns (Just $ maybe 0 S mi)) nm
-
-------------------------------------------------------------------------------
--- TODO: move to Data.List?
-
-export
-elemPos : Eq a => a -> List a -> Maybe Nat
-elemPos x = go 0 where
-
-  go : Nat -> List a -> Maybe Nat
-  go idx [] = Nothing
-  go idx (y :: ys) = idx <$ guard (x == y) <|> go (S idx) ys
diff --git a/libs/base/Deriving/Foldable.idr b/libs/base/Deriving/Foldable.idr
index 0c9d81109..7b200e06f 100644
--- a/libs/base/Deriving/Foldable.idr
+++ b/libs/base/Deriving/Foldable.idr
@@ -143,7 +143,7 @@ parameters
   {auto error : MonadError Error m}
   {auto cs : MonadState Parameters m}
   (t : Name)
-  (ps : List Name)
+  (ps : List (Name, Nat))
   (x : Name)
 
   ||| When analysing the type of a constructor for the type family t,
@@ -161,7 +161,7 @@ parameters
   fromTypeView (Left prf) = prf
   fromTypeView (Right fo) = FIFree fo
 
-  ||| Hoping to observe that ty is functorial
+  ||| Hoping to observe that ty is foldable
   export
   typeView : (ty : TTImp) -> m (TypeView ty)
 
@@ -187,7 +187,7 @@ parameters
           Yes Refl => pure $ Left (FIRec prf sp)
           No diff => case !(hasImplementation Foldable f) of
             Just prf => pure (Left (FIFold isFO prf sp))
-            Nothing => case hd `elemPos` ps of
+            Nothing => case lookup hd ps of
               Just n => do
                 -- record that the nth parameter should be functorial
                 ns <- gets asFoldables
@@ -220,7 +220,7 @@ parameters
           Nothing => do
             let Just (MkAppView (_, hd) ts prf) = appView f
                | _ => throwError (NotAnApplication f)
-            case hd `elemPos` ps of
+            case lookup hd ps of
               Just n => do
                 -- record that the nth parameter should be bifoldable
                 ns <- gets asBifoldables
@@ -335,8 +335,9 @@ namespace Foldable
     (ns, cls) <- runStateT {m = m} initParameters $ for cs $ \ (cName, ty) =>
       withError (WhenCheckingConstructor cName) $ do
         -- Grab the types of the constructor's explicit arguments
-        let Just (MkConstructorView paras para args) = constructorView ty
+        let Just (MkConstructorView (paraz :< (para, _)) args) = constructorView ty
               | _ => throwError ConfusingReturnType
+        let paras = paraz <>> []
         logMsg "derive.foldable.clauses" 10 $
           "\{showPrefix True (dropNS cName)} (\{joinBy ", " (map (showPrec Dollar . mapTTImp cleanup . unArg . snd) args)})"
         let vars = map (map (IVar fc . un . ("x" ++) . show . (`minus` 1)))
diff --git a/libs/base/Deriving/Functor.idr b/libs/base/Deriving/Functor.idr
index dbb308f43..30cddf02a 100644
--- a/libs/base/Deriving/Functor.idr
+++ b/libs/base/Deriving/Functor.idr
@@ -132,7 +132,7 @@ parameters
   {auto error : MonadError Error m}
   {auto cs : MonadState Parameters m}
   (t : Name)
-  (ps : List Name)
+  (ps : List (Name, Nat))
   (x : Name)
 
   ||| When analysing the type of a constructor for the type family t,
@@ -178,7 +178,7 @@ parameters
             Negative => throwError (NegativeOccurrence t (IApp fc f arg))
           No diff => case !(hasImplementation Functor f) of
             Just prf => pure (Left (FIFun isFO prf sp))
-            Nothing => case hd `elemPos` ps of
+            Nothing => case lookup hd ps of
               Just n => do
                 -- record that the nth parameter should be functorial
                 ns <- gets asFunctors
@@ -222,7 +222,7 @@ parameters
           Nothing => do
             let Just (MkAppView (_, hd) ts prf) = appView f
                | _ => throwError (NotAnApplication f)
-            case hd `elemPos` ps of
+            case lookup hd ps of
               Just n => do
                 -- record that the nth parameter should be bifunctorial
                 ns <- gets asBifunctors
@@ -345,8 +345,9 @@ namespace Functor
     (ns, cls) <- runStateT {m = m} initParameters $ for cs $ \ (cName, ty) =>
       withError (WhenCheckingConstructor cName) $ do
         -- Grab the types of the constructor's explicit arguments
-        let Just (MkConstructorView paras para args) = constructorView ty
+        let Just (MkConstructorView (paraz :< (para, _)) args) = constructorView ty
               | _ => throwError ConfusingReturnType
+        let paras = paraz <>> []
         logMsg "derive.functor.clauses" 10 $
           "\{showPrefix True (dropNS cName)} (\{joinBy ", " (map (showPrec Dollar . mapTTImp cleanup . unArg . snd) args)})"
         let vars = map (map (IVar fc . un . ("x" ++) . show . (`minus` 1)))
@@ -376,6 +377,11 @@ namespace Functor
     let b = un $ freshName paramNames "b"
     let va = IVar fc a
     let vb = IVar fc b
+    logMsg "derive.functor.parameters" 20 $ unlines
+      [ "Functors: \{show ns.asFunctors}"
+      , "Bifunctors: \{show ns.asBifunctors}"
+      , "Parameters: \{show (map (mapFst unArg) params)}"
+      ]
     let ty = MkTy fc fc mapName $ withParams fc (paramConstraints ns) params
            $ IPi fc M0 ImplicitArg (Just a) (IType fc)
            $ IPi fc M0 ImplicitArg (Just b) (IType fc)
diff --git a/libs/base/Deriving/Show.idr b/libs/base/Deriving/Show.idr
new file mode 100644
index 000000000..847165843
--- /dev/null
+++ b/libs/base/Deriving/Show.idr
@@ -0,0 +1,293 @@
+||| Deriving show instances using reflection
+||| You can for instance define:
+||| ```
+||| data Tree a = Leaf a | Node (Tree a) (Tree a)
+||| treeShow : Show a => Show (Tree a)
+||| treeShow = %runElab derive
+||| ```
+
+module Deriving.Show
+
+import public Control.Monad.Either
+import public Control.Monad.State
+import public Data.Maybe
+import public Decidable.Equality
+import public Language.Reflection
+
+import public Deriving.Common
+
+%language ElabReflection
+%default total
+
+public export
+fromShowPrec :
+  (Prec -> ty -> String) ->
+  Show ty
+fromShowPrec sp = MkShow (sp Open) sp
+
+------------------------------------------------------------------------------
+-- Errors
+
+||| Possible errors for the functor-deriving machinery.
+public export
+data Error : Type where
+  NotAShowable : Name -> Error
+  UnsupportedType : TTImp -> Error
+  NotAFiniteStructure : Error
+  NotAnUnconstrainedValue : Count -> Error
+  InvalidGoal : Error
+  ConfusingReturnType : Error
+  -- Contextual information
+  WhenCheckingConstructor : Name -> Error -> Error
+  WhenCheckingArg : TTImp -> Error -> Error
+
+export
+Show Error where
+  show = joinBy "\n" . go [<] where
+
+    go : SnocList String -> Error -> List String
+    go acc (NotAShowable nm) = acc <>> ["Couldn't find a `Show' instance for the type \{show nm}"]
+    go acc (UnsupportedType s) = acc <>> ["Unsupported type \{show s}"]
+    go acc NotAFiniteStructure = acc <>> ["Cannot show an infinite structure"]
+    go acc (NotAnUnconstrainedValue rig) = acc <>> ["Cannot show a \{enunciate rig} value"]
+    go acc InvalidGoal = acc <>> ["Expected a goal of the form `Show t`"]
+    go acc ConfusingReturnType = acc <>> ["Confusing telescope"]
+    go acc (WhenCheckingConstructor nm err) = go (acc :< "When checking constructor \{show nm}") err
+    go acc (WhenCheckingArg s err) = go (acc :< "When checking argument of type \{show s}") err
+
+record Parameters where
+  constructor MkParameters
+  asShowables : List Nat
+
+initParameters : Parameters
+initParameters = MkParameters []
+
+paramConstraints : Parameters -> Nat -> Maybe TTImp
+paramConstraints params pos
+    = IVar emptyFC `{Prelude.Show.Show} <$ guard (pos `elem` params.asShowables)
+
+------------------------------------------------------------------------------
+-- Core machinery: being showable
+
+ShowN : TTImp -> Name -> TTImp
+ShowN ty nm = go (IVar emptyFC nm) ty Z where
+
+  go : TTImp -> TTImp -> Nat -> TTImp
+  go acc (IPi _ _ pinfo mn (IType _) ty) n
+    = let var = MN "__param" (cast n) in
+      IPi emptyFC M0 ImplicitArg (Just var) (Implicit emptyFC False)
+    $ IPi emptyFC MW AutoImplicit Nothing (IApp emptyFC `(Show) (IVar emptyFC var))
+    $ go (TTImp.apply acc (toList (fromPiInfo emptyFC pinfo mn (IVar emptyFC var)))) ty (S n)
+  go acc (IPi _ _ pinfo mn _ ty) n
+    = let var = MN "__param" (cast n) in
+      IPi emptyFC M0 ImplicitArg (Just var) (Implicit emptyFC False)
+    $ go (TTImp.apply acc (toList (fromPiInfo emptyFC pinfo mn (IVar emptyFC var)))) ty (S n)
+  go acc _ _ = IApp emptyFC `(Show) acc
+
+||| IsShowable is parametrised by
+||| @ t  the name of the data type whose constructors are being analysed
+||| @ ty the type being analysed
+||| The inductive type delivers a proof that ty can be shown,
+||| assuming that t also is showable.
+public export
+data IsShowable : (t : Name) -> (ty : TTImp) -> Type
+data IsShowableArgs : (t : Name) -> (tconty : TTImp) -> (ty : List (Argument TTImp)) -> Type
+
+data IsShowable : (t : Name) -> (ty : TTImp) -> Type where
+  ||| The subterm is delayed (Lazy only, we can't traverse infinite structures)
+  ISDelayed : IsShowable t ty -> IsShowable t (IDelayed fc LLazy ty)
+  ||| There is a recursive subtree of type (t a1 ... an)
+  ISRec : (0 _ : IsAppView (_, t) _ ty) -> IsShowable t ty
+  ||| There are nested subtrees somewhere inside a 3rd party type constructor
+  ||| which satisfies the Show interface
+  ISShowN : (0 _ : IsAppView (_, tcon) args ty) ->
+            HasType tcon tconty ->
+            IsProvable (ShowN tconty tcon) ->
+            IsShowableArgs t tconty (args <>> []) -> IsShowable t ty
+  ||| Or we could be referring to one of the parameters
+  ISParam : IsShowable t ty
+  ||| A primitive type is trivially Showable
+  ISPrim : (ty : PrimType) -> IsShowable t (IPrimVal fc (PrT ty))
+
+data IsShowableArgs : (t : Name) -> (tconty : TTImp) -> (ty : List (Argument TTImp)) -> Type where
+  Done : IsShowableArgs t tconty []
+  Step :  IsShowable t (unArg arg) -> IsShowableArgs t ty args ->
+         IsShowableArgs t (IPi fc1 r ExplicitArg mn (IType fc2) ty) (arg :: args)
+  Drop : (forall fc. Not (dom === IType fc)) -> IsShowableArgs t ty args ->
+         IsShowableArgs t (IPi fc1 r ExplicitArg mn dom ty) (arg :: args)
+  Skip : Not (pinfo === ExplicitArg) -> IsShowableArgs t ty args ->
+         IsShowableArgs t (IPi fc1 r pinfo mn dom ty) args -- TODO: constrain more?
+
+parameters (fc : FC) (mutualWith : List Name)
+
+  isRecs : IsShowableArgs t ty ts -> Bool
+  isRec : IsShowable t ts -> Bool
+
+  isRecs Done = False
+  isRecs (Step x xs) = isRec x || isRecs xs
+  isRecs (Drop f xs) = isRecs xs
+  isRecs (Skip f xs) = isRecs xs
+
+  isRec (ISDelayed x) = isRec x
+  isRec (ISRec _) = True
+  isRec (ISShowN _ _ _ xs) = isRecs xs
+  isRec ISParam = False
+  isRec (ISPrim _) = False
+
+  showPrecFun : {ty : _} -> IsShowable t ty -> TTImp -> TTImp
+  showPrecFun (ISDelayed p) t = showPrecFun p (IForce (getFC t) t)
+  showPrecFun (ISRec _) t = IApp emptyFC `(assert_total) (IApp emptyFC `(showArg) t)
+  showPrecFun {ty} (ISShowN _ _ _ as) t
+    = let isMutual = fromMaybe False (appView ty >>= \ v => pure (snd v.head `elem` mutualWith)) in
+      ifThenElse (isMutual || isRecs as) (IApp emptyFC `(assert_total)) id
+    $ IApp emptyFC `(showArg) t
+  showPrecFun ISParam t = IApp emptyFC  `(showArg) t
+  showPrecFun (ISPrim pty) t = IApp emptyFC  `(showArg) t
+
+parameters
+  {0 m : Type -> Type}
+  {auto elab : Elaboration m}
+  {auto error : MonadError Error m}
+  {auto cs : MonadState Parameters m}
+  (t : Name)
+  (ps : List (Name, Nat))
+
+  ||| Hoping to observe that ty can be shown
+  export
+  typeView : (ty : TTImp) -> m (IsShowable t ty)
+  typeViews : (tconty : TTImp) -> (tys : List (Argument TTImp)) ->
+              m (IsShowableArgs t tconty tys)
+
+  typeView (IDelayed _ lz ty) = case lz of
+    LLazy => ISDelayed <$> typeView ty
+    _ => throwError NotAFiniteStructure
+  typeView (IPrimVal _ (PrT ty)) = pure (ISPrim ty)
+  typeView ty = do
+    let Just (MkAppView (_, hd) ts prf) = appView ty
+      | _ => throwError (UnsupportedType ty)
+    let No _ = decEq hd t
+      | Yes Refl => pure (ISRec prf)
+    Just (hdty ** hT) <- hasType hd
+      | _ => case lookup hd ps <* guard (null ts) of
+               Just n => do
+                 -- record that the nth parameter should be showable
+                 ns <- gets asShowables
+                 let ns = ifThenElse (n `elem` ns) ns (n :: ns)
+                 modify { asShowables := ns }
+                 -- and happily succeed
+                 logMsg "derive.show.assumption" 10 $
+                   "I am assuming that the parameter \{show hd} can be shown"
+                 pure ISParam
+               _ => throwError (UnsupportedType ty)
+    Just iP <- isProvable (ShowN hdty hd)
+      | _ => throwError (NotAShowable hd)
+    ISShowN prf hT iP <$> typeViews hdty (ts <>> [])
+
+  typeViews _ [] = pure Done
+  typeViews (IPi _ _ ExplicitArg _ (IType fc) ty) (t :: ts)
+    = Step <$> assert_total (typeView (unArg t)) <*> typeViews ty ts
+  typeViews (IPi _ _ ExplicitArg _ dom ty) (t :: ts)
+    = Drop (\ x => believe_me x) <$> typeViews ty ts
+  typeViews (IPi _ _ _ _ _ ty) ts
+    = Skip (\ x => believe_me x) <$> typeViews ty ts
+  typeViews ty ts = throwError (UnsupportedType ty)
+
+namespace Show
+
+  derive' : (Elaboration m, MonadError Error m) =>
+            {default Private vis : Visibility} ->
+            {default Total treq : TotalReq} ->
+            {default [] mutualWith : List Name} ->
+            m (Show f)
+  derive' = do
+
+    -- expand the mutualwith names to have the internal, fully qualified, names
+    mutualWith <- map concat $ for mutualWith $ \ nm => do
+                    ntys <- getType nm
+                    pure (fst <$> ntys)
+
+    -- The goal should have the shape (Show t)
+    Just (IApp _ (IVar _ showable) t) <- goal
+      | _ => throwError InvalidGoal
+    when (`{Prelude.Show.Show} /= showable) $
+      logMsg "derive.show" 1 "Expected to derive Show but got \{show showable}"
+
+    -- t should be a type constructor
+    logMsg "derive.show" 1 "Deriving Show for \{showPrec App $ mapTTImp cleanup t}"
+    MkIsType f params cs <- isType t
+    logMsg "derive.show.constructors" 1 $
+      joinBy "\n" $ "" :: map (\ (n, ty) => "  \{showPrefix True $ dropNS n} : \{show $ mapTTImp cleanup ty}") cs
+
+    -- Generate a clause for each data constructor
+    let fc = emptyFC
+    let un = UN . Basic
+    let showName = un ("showPrec" ++ show (dropNS f))
+    let precName = un "d"
+    let prec = IVar fc precName
+    (ns, cls) <- runStateT {m = m} initParameters $ for cs $ \ (cName, ty) =>
+      withError (WhenCheckingConstructor cName) $ do
+        -- Grab the types of the constructor's explicit arguments
+        let Just (MkConstructorView paraz args) = constructorView ty
+              | _ => throwError ConfusingReturnType
+        logMsg "derive.show.clauses" 10 $
+          "\{showPrefix True (dropNS cName)} (\{joinBy ", " (map (showPrec Dollar . mapTTImp cleanup . unArg . snd) args)})"
+        -- Only keep the visible arguments
+        let args = mapMaybe (bitraverse pure (map snd . isExplicit)) args
+        -- Special case for constructors with no argument
+        let (_ :: _) = args
+          | [] => pure $ PatClause fc
+                    (apply fc (IVar fc showName) [ prec, IVar fc cName])
+                    (IPrimVal fc (Str (showPrefix True (dropNS cName))))
+
+        let vars = zipWith (const . IVar fc . un . ("x" ++) . show . (`minus` 1)) [1..length args] args
+        recs <- for (zip vars args) $ \ (v, (rig, ty)) => do
+
+                  let MW = rig
+                    | _ => throwError (NotAnUnconstrainedValue rig)
+
+                  res <- withError (WhenCheckingArg (mapTTImp cleanup ty)) $ do
+                           typeView f (paraz <>> []) ty
+                  pure $ Just (showPrecFun fc mutualWith res v)
+
+        let args = catMaybes recs
+        let asList = foldr (\ a, as => apply fc (IVar fc `{Prelude.(::)}) [a,as]) `(Prelude.Nil)
+        pure $ PatClause fc
+          (apply fc (IVar fc showName) [ prec, apply fc (IVar fc cName) vars])
+          (apply fc (IVar fc (un "showCon"))
+            [ prec
+            , IPrimVal fc (Str (showPrefix True (dropNS cName)))
+            , case args of
+                [a] => a
+                _ => IApp fc (IVar fc (un "concat")) (asList args)
+            ])
+
+    -- Generate the type of the show function
+    let ty = MkTy fc fc showName $ withParams fc (paramConstraints ns) params
+           $ `(Prec -> ~(t) -> String)
+    logMsg "derive.show.clauses" 1 $
+      joinBy "\n" ("" :: ("  " ++ show (mapITy cleanup ty))
+                      :: map (("  " ++) . showClause InDecl . mapClause cleanup) cls)
+
+    -- Define the instance
+    check $ ILocal fc
+      [ IClaim fc MW vis [Totality treq] ty
+      , IDef fc showName cls
+      ] `(fromShowPrec ~(IVar fc showName))
+
+  ||| Derive an implementation of Show for a type constructor.
+  ||| This can be used like so:
+  ||| ```
+  ||| data Tree a = Leaf a | Node (Tree a) (Tree a)
+  ||| treeShow : Show a => Show (Tree a)
+  ||| treeShow = %runElab derive
+  ||| ```
+  export
+  derive : {default Private vis : Visibility} ->
+           {default Total treq : TotalReq} ->
+           {default [] mutualWith : List Name} ->
+           Elab (Show f)
+  derive = do
+    res <- runEitherT {e = Error, m = Elab} (derive' {vis, treq, mutualWith})
+    case res of
+      Left err => fail (show err)
+      Right prf => pure prf
diff --git a/libs/base/Deriving/Traversable.idr b/libs/base/Deriving/Traversable.idr
index 60ab5abe0..a849f0a84 100644
--- a/libs/base/Deriving/Traversable.idr
+++ b/libs/base/Deriving/Traversable.idr
@@ -89,7 +89,7 @@ isFreeOf' x ty = case isFreeOf x ty of
 ||| @ t  the name of the data type whose constructors are being analysed
 ||| @ x  the name of the type variable that the traversable action will act on
 ||| @ ty the type being analysed
-||| The inductive type delivers a proof that x can be folded over in ty,
+||| The inductive type delivers a proof that x can be traversed over in ty,
 ||| assuming that t also is traversable.
 public export
 data IsTraversableIn : (t, x : Name) -> (ty : TTImp) -> Type where
@@ -122,7 +122,7 @@ parameters
   {auto error : MonadError Error m}
   {auto cs : MonadState Parameters m}
   (t : Name)
-  (ps : List Name)
+  (ps : List (Name, Nat))
   (x : Name)
 
   ||| When analysing the type of a constructor for the type family t,
@@ -140,7 +140,7 @@ parameters
   fromTypeView (Left prf) = prf
   fromTypeView (Right fo) = TIFree fo
 
-  ||| Hoping to observe that ty is functorial
+  ||| Hoping to observe that ty is traversable
   export
   typeView : (ty : TTImp) -> m (TypeView ty)
 
@@ -166,7 +166,7 @@ parameters
           Yes Refl => pure $ Left (TIRec prf sp)
           No diff => case !(hasImplementation Traversable f) of
             Just prf => pure (Left (TIFold isFO prf sp))
-            Nothing => case hd `elemPos` ps of
+            Nothing => case lookup hd ps of
               Just n => do
                 -- record that the nth parameter should be functorial
                 ns <- gets asTraversables
@@ -199,7 +199,7 @@ parameters
           Nothing => do
             let Just (MkAppView (_, hd) ts prf) = appView f
                | _ => throwError (NotAnApplication f)
-            case hd `elemPos` ps of
+            case lookup hd ps of
               Just n => do
                 -- record that the nth parameter should be bitraversable
                 ns <- gets asBitraversables
@@ -359,8 +359,9 @@ namespace Traversable
     (ns, cls) <- runStateT {m = m} initParameters $ for cs $ \ (cName, ty) =>
       withError (WhenCheckingConstructor cName) $ do
         -- Grab the types of the constructor's explicit arguments
-        let Just (MkConstructorView paras para args) = constructorView ty
+        let Just (MkConstructorView (paraz :< (para, _)) args) = constructorView ty
               | _ => throwError ConfusingReturnType
+        let paras = paraz <>> []
         logMsg "derive.traversable.clauses" 10 $
           "\{showPrefix True (dropNS cName)} (\{joinBy ", " (map (showPrec Dollar . mapTTImp cleanup . unArg . snd) args)})"
         let vars = map (map (IVar fc . un . ("x" ++) . show . (`minus` 1)))
diff --git a/libs/base/base.ipkg b/libs/base/base.ipkg
index 4b6412ba3..757075683 100644
--- a/libs/base/base.ipkg
+++ b/libs/base/base.ipkg
@@ -88,6 +88,7 @@ modules = Control.App,
           Deriving.Common,
           Deriving.Foldable,
           Deriving.Functor,
+          Deriving.Show,
           Deriving.Traversable,
 
           Decidable.Decidable,
diff --git a/tests/base/deriving_foldable/DeriveFoldable.idr b/tests/base/deriving_foldable/DeriveFoldable.idr
index 2e18f9708..9a93448fc 100644
--- a/tests/base/deriving_foldable/DeriveFoldable.idr
+++ b/tests/base/deriving_foldable/DeriveFoldable.idr
@@ -171,16 +171,16 @@ namespace MaybeT
 
 namespace TreeT
 
-  data TreeT : (Type -> Type -> Type) -> Type -> Type where
-    MkTreeT : layer a (TreeT layer a) -> TreeT layer a
+  data TreeT : (lbl : Type) -> (Type -> Type -> Type) -> Type -> Type where
+    MkTreeT : lbl -> layer a (TreeT lbl layer a) -> TreeT lbl layer a
 
   %hint
-  treeT : Bifoldable layer => Foldable (TreeT layer)
+  treeT : Bifoldable layer => Foldable (TreeT lbl layer)
   treeT = %runElab derive {treq = CoveringOnly}
 
   record Tree (a : Type) where
     constructor MkTree
-    runTree : TreeT Either a
+    runTree : TreeT () Either a
 
   tree : Foldable Tree
   tree = %runElab derive {treq = CoveringOnly}
diff --git a/tests/base/deriving_foldable/expected b/tests/base/deriving_foldable/expected
index 6332ccc1b..234237679 100644
--- a/tests/base/deriving_foldable/expected
+++ b/tests/base/deriving_foldable/expected
@@ -56,8 +56,8 @@ LOG derive.foldable.clauses:1:
   foldMapMaybeT f (MkMaybeT x2) = foldMap (foldMap f) x2
 LOG derive.foldable.assumption:10: I am assuming that the parameter layer is a Bifoldable
 LOG derive.foldable.clauses:1: 
-  foldMapTreeT : {0 layer : _} -> Bifoldable layer => {0 a, b : Type} -> Monoid b => (a -> b) -> TreeT layer a -> b
-  foldMapTreeT f (MkTreeT x2) = bifoldMap f (foldMapTreeT f) x2
+  foldMapTreeT : {0 lbl, layer : _} -> Bifoldable layer => {0 a, b : Type} -> Monoid b => (a -> b) -> TreeT lbl layer a -> b
+  foldMapTreeT f (MkTreeT x3 x4) = bifoldMap f (foldMapTreeT f) x4
 LOG derive.foldable.clauses:1: 
   foldMapTree : {0 a, b : Type} -> Monoid b => (a -> b) -> Tree a -> b
   foldMapTree f (MkTree x1) = foldMap f x1
@@ -65,7 +65,7 @@ LOG derive.foldable.clauses:1:
   foldMapIVect : {0 m : _} -> {0 a, b : Type} -> Monoid b => (a -> b) -> IVect {n = m} a -> b
   foldMapIVect f (MkIVect x2) = foldMap f x2
 LOG derive.foldable.clauses:1: 
-  foldMapEqMap : {0 key, eq : _} -> {0 a, b : Type} -> Monoid b => (a -> b) -> EqMap key {{conArg:5682} = eq} a -> b
+  foldMapEqMap : {0 key, eq : _} -> {0 a, b : Type} -> Monoid b => (a -> b) -> EqMap key {{conArg:5707} = eq} a -> b
   foldMapEqMap f (MkEqMap x3) = foldMap (foldMap f) x3
 LOG derive.foldable.clauses:1: 
   foldMapTree : {0 l : _} -> {0 a, b : Type} -> Monoid b => (a -> b) -> Tree l a -> b
diff --git a/tests/base/deriving_functor/DeriveFunctor.idr b/tests/base/deriving_functor/DeriveFunctor.idr
index e0b61ef1a..a0c3b8e25 100644
--- a/tests/base/deriving_functor/DeriveFunctor.idr
+++ b/tests/base/deriving_functor/DeriveFunctor.idr
@@ -167,16 +167,16 @@ namespace MaybeT
 
 namespace TreeT
 
-  data TreeT : (Type -> Type -> Type) -> Type -> Type where
-    MkTreeT : layer a (TreeT layer a) -> TreeT layer a
+  data TreeT : (lbl : Type) -> (Type -> Type -> Type) -> Type -> Type where
+    MkTreeT : lbl -> layer a (TreeT lbl layer a) -> TreeT lbl layer a
 
   %hint
-  treeT : Bifunctor layer => Functor (TreeT layer)
+  treeT : Bifunctor layer => Functor (TreeT lbl layer)
   treeT = %runElab derive {treq = CoveringOnly}
 
   record Tree (a : Type) where
     constructor MkTree
-    runTree : TreeT Either a
+    runTree : TreeT () Either a
 
   tree : Functor Tree
   tree = %runElab derive {treq = CoveringOnly}
diff --git a/tests/base/deriving_functor/expected b/tests/base/deriving_functor/expected
index dc436220d..ccc7fc223 100644
--- a/tests/base/deriving_functor/expected
+++ b/tests/base/deriving_functor/expected
@@ -66,8 +66,8 @@ LOG derive.functor.clauses:1:
   mapMaybeT f (MkMaybeT x2) = MkMaybeT (map (map f) x2)
 LOG derive.functor.assumption:10: I am assuming that the parameter layer is a Bifunctor
 LOG derive.functor.clauses:1: 
-  mapTreeT : {0 layer : _} -> Bifunctor layer => {0 a, b : Type} -> (a -> b) -> TreeT layer a -> TreeT layer b
-  mapTreeT f (MkTreeT x2) = MkTreeT (bimap f (mapTreeT f) x2)
+  mapTreeT : {0 lbl, layer : _} -> Bifunctor layer => {0 a, b : Type} -> (a -> b) -> TreeT lbl layer a -> TreeT lbl layer b
+  mapTreeT f (MkTreeT x3 x4) = MkTreeT x3 (bimap f (mapTreeT f) x4)
 LOG derive.functor.clauses:1: 
   mapTree : {0 a, b : Type} -> (a -> b) -> Tree a -> Tree b
   mapTree f (MkTree x1) = MkTree (map f x1)
@@ -75,20 +75,20 @@ LOG derive.functor.clauses:1:
   mapIVect : {0 m : _} -> {0 a, b : Type} -> (a -> b) -> IVect {n = m} a -> IVect {n = m} b
   mapIVect f (MkIVect x2) = MkIVect (map f x2)
 LOG derive.functor.clauses:1: 
-  mapEqMap : {0 key, eq : _} -> {0 a, b : Type} -> (a -> b) -> EqMap key {{conArg:5665} = eq} a -> EqMap key {{conArg:5665} = eq} b
+  mapEqMap : {0 key, eq : _} -> {0 a, b : Type} -> (a -> b) -> EqMap key {{conArg:5692} = eq} a -> EqMap key {{conArg:5692} = eq} b
   mapEqMap f (MkEqMap x3) = MkEqMap (map (map f) x3)
 LOG derive.functor.clauses:1: 
   mapCont : {0 r : _} -> {0 a, b : Type} -> (a -> b) -> Cont r a -> Cont r b
-  mapCont f (MkCont x2) = MkCont (\ {arg:6021} => x2 (\ {arg:6023} => {arg:6021} (f {arg:6023})))
+  mapCont f (MkCont x2) = MkCont (\ {arg:6048} => x2 (\ {arg:6050} => {arg:6048} (f {arg:6050})))
 LOG derive.functor.clauses:1: 
   mapCont2 : {0 r, e : _} -> {0 a, b : Type} -> (a -> b) -> Cont2 r e a -> Cont2 r e b
-  mapCont2 f (MkCont2 x3) = MkCont2 (\ {arg:6113} => \ {arg:6120} => x3 {arg:6113} (\ {arg:6122} => {arg:6120} (f {arg:6122})))
+  mapCont2 f (MkCont2 x3) = MkCont2 (\ {arg:6140} => \ {arg:6147} => x3 {arg:6140} (\ {arg:6149} => {arg:6147} (f {arg:6149})))
 LOG derive.functor.clauses:1: 
   mapCont2' : {0 r, e : _} -> {0 a, b : Type} -> (a -> b) -> Cont2' r e a -> Cont2' r e b
-  mapCont2' f (MkCont2' x3) = MkCont2' (\ {arg:6227} => x3 (mapFst (\ t => \ {arg:6229} => t (f {arg:6229})) {arg:6227}))
+  mapCont2' f (MkCont2' x3) = MkCont2' (\ {arg:6254} => x3 (mapFst (\ t => \ {arg:6256} => t (f {arg:6256})) {arg:6254}))
 LOG derive.functor.clauses:1: 
   mapCont2'' : {0 r, e : _} -> {0 a, b : Type} -> (a -> b) -> Cont2'' r e a -> Cont2'' r e b
-  mapCont2'' f (MkCont2'' x3) = MkCont2'' (\ {arg:6351} => x3 (Delay (mapFst (\ t => \ {arg:6354} => t (Delay (f {arg:6354}))) {arg:6351})))
+  mapCont2'' f (MkCont2'' x3) = MkCont2'' (\ {arg:6378} => x3 (Delay (mapFst (\ t => \ {arg:6381} => t (Delay (f {arg:6381}))) {arg:6378})))
 LOG derive.functor.clauses:1: 
   mapWithImplicits : {0 a, b : Type} -> (a -> b) -> WithImplicits a -> WithImplicits b
   mapWithImplicits f (MkImplicit {x = x1} x2) = MkImplicit {x = f x1} (f x2)
diff --git a/tests/base/deriving_show/DeriveShow.idr b/tests/base/deriving_show/DeriveShow.idr
new file mode 100644
index 000000000..e20224fbf
--- /dev/null
+++ b/tests/base/deriving_show/DeriveShow.idr
@@ -0,0 +1,194 @@
+module DeriveShow
+
+import Deriving.Show
+
+%language ElabReflection
+%default covering
+
+%logging "derive.show.clauses" 1
+%logging "derive.show.assumption" 10
+
+namespace Enum
+
+  data Enum = A | B | C
+
+  enumShow : Show Enum
+  enumShow = %runElab derive
+
+namespace Sum
+
+  data Sum : Type where
+    AString : String -> Sum
+    ANat : Nat -> Sum
+
+  sumShow : Show Sum
+  sumShow = %runElab derive
+
+list : Show a => Show (List a)
+list = %runElab derive
+
+maybe : Show a => Show (Maybe a)
+maybe = %runElab derive
+
+either : (Show err, Show a) => Show (Either err a)
+either = %runElab derive
+
+namespace Constant
+
+  record Constant (a, b : Type) where
+    constructor MkConstant
+    runConstant : a
+
+  constant : Show a => Show (Constant a b)
+  constant = %runElab derive
+
+namespace Vect
+
+  public export
+  data Vect : Nat -> Type -> Type where
+    Nil : Vect Z a
+    (::) : a -> Vect n a -> Vect (S n) a
+
+  export %hint
+  total
+  vect : Show a => Show (Vect n a)
+  vect = %runElab derive
+
+namespace BigTree
+
+  data BigTree a
+    = End a
+    | Branch String (List a) (Bool -> BigTree a)
+    | Rose (List (BigTree a))
+
+  failing "Unsupported type"
+    bigTree : Show a => Show (BigTree a)
+    bigTree = %runElab derive
+
+namespace Matrix
+
+  record Matrix m n a where
+    constructor MkMatrix
+    runMatrix : Vect m (Vect n a)
+
+  total
+  matrix : Show a => Show (Matrix m n a)
+  matrix = %runElab derive
+
+namespace Tm
+
+  public export
+  data Op : Nat -> Type where
+    Neg : Op 1
+    Add : Op 2
+
+  %hint
+  op : Show (Op n)
+  op = %runElab derive
+
+  public export
+  data Tm : Type -> Type where
+    Var : a -> Tm a
+    Call : Op n -> Vect n (Tm a) -> Tm a
+    Lam : Tm (Maybe a) -> Tm a
+
+  public export total %hint
+  tm : Show a => Show (Tm a)
+  tm = %runElab derive
+
+namespace Forest
+
+  data Tree : Type -> Type
+  data Forest : Type -> Type
+
+  data Tree : Type -> Type where
+    Leaf : a -> Tree a
+    Node : Forest a -> Tree a
+
+  data Forest : Type -> Type where
+    Empty : Forest a
+    Plant : Tree a -> Forest a -> Forest a
+
+  %hint total tree : Show a => Show (Tree a)
+  %hint total forest : Show a => Show (Forest a)
+
+  tree = %runElab derive {mutualWith = [`{Forest}]}
+  forest = %runElab derive {mutualWith = [`{Tree}]}
+
+namespace List1
+
+  data List1 : Type -> Type where
+    MkList1 : (a, Maybe (List1 a)) -> List1 a
+
+  total %hint
+  list1 : Show a => Show (List1 a)
+  list1 = %runElab derive
+
+namespace Full
+
+  data Full a = Leaf a | Node (Full (a, a))
+
+  total %hint
+  full : Show a => Show (Full a)
+  full = %runElab derive
+
+failing "Unsupported type"
+
+  data NOT : Type -> Type where
+    MkNOT : (a -> Void) -> NOT a
+
+  total
+  negative : Show a => Show (NOT a)
+  negative = %runElab derive
+
+namespace Colist
+
+  data Colist a = Nil | (::) a (Inf (Colist a))
+
+  failing "Cannot show an infinite structure"
+
+    total
+    colist : Show a => Show (Colist a)
+    colist = %runElab derive
+
+namespace LAZY
+
+  record LAZY (a : Type) where
+    constructor MkLAZY
+    wrapped : Lazy a
+
+  total
+  lazy : Show a => Show (LAZY a)
+  lazy = %runElab derive
+
+namespace Implicit
+
+  data IVect : {n : Nat} -> (a : Type) -> Type where
+    MkIVect : (v : Vect n a) -> IVect {n} a
+
+  ivect : {m : Nat} -> Show a => Show (IVect {n = m} a)
+  ivect = %runElab derive
+
+namespace EqMap
+
+  data EqMap : (key : Type) -> Eq key => (val : Type) -> Type where
+    MkEqMap : (eq : Eq key) => List (key, val) -> EqMap key @{eq} val
+
+  empty : Eq key => EqMap key val
+  empty = MkEqMap []
+
+  insert : (eq : Eq key) => key -> val -> EqMap key @{eq} val -> EqMap key @{eq} val
+  insert k v (MkEqMap kvs) = MkEqMap ((k, v) :: filter ((k /=) . fst) kvs)
+
+  fromList : Eq key => List (key, val) -> EqMap key val
+  fromList = foldr (uncurry insert) empty
+
+  toList : EqMap key @{eq} val -> List (key, val)
+  toList (MkEqMap kvs) = kvs
+
+  test : EqMap.toList (fromList [(1,2), (1,3), (2, 4), (5, 3), (1, 0)])
+         === [(1,2), (2, 4), (5, 3)]
+  test = Refl
+
+  eqMap : (eq : Eq key) => Show key => Show val => Show (EqMap key @{eq} val)
+  eqMap = %runElab derive
diff --git a/tests/base/deriving_show/Search.idr b/tests/base/deriving_show/Search.idr
new file mode 100644
index 000000000..ec41c7f24
--- /dev/null
+++ b/tests/base/deriving_show/Search.idr
@@ -0,0 +1,12 @@
+module Search
+
+import Language.Reflection
+import Language.Reflection.TTImp
+
+%language ElabReflection
+
+nothing : Maybe (Not Nat)
+nothing = %runElab (search ?)
+
+test : Search.nothing === Nothing
+test = Refl
diff --git a/tests/base/deriving_show/expected b/tests/base/deriving_show/expected
new file mode 100644
index 000000000..ef1b1c15f
--- /dev/null
+++ b/tests/base/deriving_show/expected
@@ -0,0 +1,88 @@
+1/1: Building DeriveShow (DeriveShow.idr)
+LOG derive.show.clauses:1: 
+  showPrecEnum : Prec -> Enum -> String
+  showPrecEnum d A = "A"
+  showPrecEnum d B = "B"
+  showPrecEnum d C = "C"
+LOG derive.show.clauses:1: 
+  showPrecSum : Prec -> Sum -> String
+  showPrecSum d (AString x0) = showCon d "AString" (showArg x0)
+  showPrecSum d (ANat x0) = showCon d "ANat" (showArg x0)
+LOG derive.show.assumption:10: I am assuming that the parameter a can be shown
+LOG derive.show.clauses:1: 
+  showPrecList : {0 a : _} -> Show a => Prec -> List a -> String
+  showPrecList d Nil = "Nil"
+  showPrecList d (x0 :: x1) = showCon d "(::)" (concat ((showArg x0) :: ((assert_total (showArg x1)) :: Nil)))
+LOG derive.show.assumption:10: I am assuming that the parameter ty can be shown
+LOG derive.show.clauses:1: 
+  showPrecMaybe : {0 a : _} -> Show a => Prec -> Maybe a -> String
+  showPrecMaybe d Nothing = "Nothing"
+  showPrecMaybe d (Just x0) = showCon d "Just" (showArg x0)
+LOG derive.show.assumption:10: I am assuming that the parameter a can be shown
+LOG derive.show.assumption:10: I am assuming that the parameter b can be shown
+LOG derive.show.clauses:1: 
+  showPrecEither : {0 err : _} -> Show err => {0 a : _} -> Show a => Prec -> Either err a -> String
+  showPrecEither d (Left x0) = showCon d "Left" (showArg x0)
+  showPrecEither d (Right x0) = showCon d "Right" (showArg x0)
+LOG derive.show.assumption:10: I am assuming that the parameter a can be shown
+LOG derive.show.clauses:1: 
+  showPrecConstant : {0 a : _} -> Show a => {0 b : _} -> Prec -> Constant a b -> String
+  showPrecConstant d (MkConstant x0) = showCon d "MkConstant" (showArg x0)
+LOG derive.show.assumption:10: I am assuming that the parameter a can be shown
+LOG derive.show.clauses:1: 
+  showPrecVect : {0 n, a : _} -> Show a => Prec -> Vect n a -> String
+  showPrecVect d Nil = "Nil"
+  showPrecVect d (x0 :: x1) = showCon d "(::)" (concat ((showArg x0) :: ((assert_total (showArg x1)) :: Nil)))
+LOG derive.show.assumption:10: I am assuming that the parameter a can be shown
+LOG derive.show.assumption:10: I am assuming that the parameter a can be shown
+LOG derive.show.assumption:10: I am assuming that the parameter a can be shown
+LOG derive.show.clauses:1: 
+  showPrecMatrix : {0 m, n, a : _} -> Show a => Prec -> Matrix m n a -> String
+  showPrecMatrix d (MkMatrix x0) = showCon d "MkMatrix" (showArg x0)
+LOG derive.show.clauses:1: 
+  showPrecOp : {0 n : _} -> Prec -> Op n -> String
+  showPrecOp d Neg = "Neg"
+  showPrecOp d Add = "Add"
+LOG derive.show.assumption:10: I am assuming that the parameter a can be shown
+LOG derive.show.clauses:1: 
+  showPrecTm : {0 a : _} -> Show a => Prec -> Tm a -> String
+  showPrecTm d (Var x0) = showCon d "Var" (showArg x0)
+  showPrecTm d (Call x0 x1) = showCon d "Call" (concat ((showArg x0) :: ((assert_total (showArg x1)) :: Nil)))
+  showPrecTm d (Lam x0) = showCon d "Lam" (assert_total (showArg x0))
+LOG derive.show.assumption:10: I am assuming that the parameter a can be shown
+LOG derive.show.assumption:10: I am assuming that the parameter a can be shown
+LOG derive.show.clauses:1: 
+  showPrecTree : {0 a : _} -> Show a => Prec -> Tree a -> String
+  showPrecTree d (Leaf x0) = showCon d "Leaf" (showArg x0)
+  showPrecTree d (Node x0) = showCon d "Node" (assert_total (showArg x0))
+LOG derive.show.assumption:10: I am assuming that the parameter a can be shown
+LOG derive.show.clauses:1: 
+  showPrecForest : {0 a : _} -> Show a => Prec -> Forest a -> String
+  showPrecForest d Empty = "Empty"
+  showPrecForest d (Plant x0 x1) = showCon d "Plant" (concat ((assert_total (showArg x0)) :: ((assert_total (showArg x1)) :: Nil)))
+LOG derive.show.assumption:10: I am assuming that the parameter a can be shown
+LOG derive.show.clauses:1: 
+  showPrecList1 : {0 a : _} -> Show a => Prec -> List1 a -> String
+  showPrecList1 d (MkList1 x0) = showCon d "MkList1" (assert_total (showArg x0))
+LOG derive.show.assumption:10: I am assuming that the parameter a can be shown
+LOG derive.show.clauses:1: 
+  showPrecFull : {0 a : _} -> Show a => Prec -> Full a -> String
+  showPrecFull d (Leaf x0) = showCon d "Leaf" (showArg x0)
+  showPrecFull d (Node x0) = showCon d "Node" (assert_total (showArg x0))
+LOG derive.show.assumption:10: I am assuming that the parameter a can be shown
+LOG derive.show.assumption:10: I am assuming that the parameter a can be shown
+LOG derive.show.clauses:1: 
+  showPrecLAZY : {0 a : _} -> Show a => Prec -> LAZY a -> String
+  showPrecLAZY d (MkLAZY x0) = showCon d "MkLAZY" (showArg (Force x0))
+LOG derive.show.assumption:10: I am assuming that the parameter a can be shown
+LOG derive.show.clauses:1: 
+  showPrecIVect : {0 m, a : _} -> Show a => Prec -> IVect {n = m} a -> String
+  showPrecIVect d (MkIVect x0) = showCon d "MkIVect" (showArg x0)
+LOG derive.show.assumption:10: I am assuming that the parameter key can be shown
+LOG derive.show.assumption:10: I am assuming that the parameter val can be shown
+LOG derive.show.clauses:1: 
+  showPrecEqMap : {0 key : _} -> Show key => {0 eq, val : _} -> Show val => Prec -> EqMap key {{conArg:5125} = eq} val -> String
+  showPrecEqMap d (MkEqMap x0) = showCon d "MkEqMap" (showArg x0)
+DeriveShow> "Lam (Call Add ((::) (Var Nothing) ((::) (Var (Just ())) Nil)))"
+DeriveShow> 
+Bye for now!
diff --git a/tests/base/deriving_show/input b/tests/base/deriving_show/input
new file mode 100644
index 000000000..038292893
--- /dev/null
+++ b/tests/base/deriving_show/input
@@ -0,0 +1,2 @@
+show (Lam (Call Add [Var Nothing, Var (Just ())]))
+:q
\ No newline at end of file
diff --git a/tests/base/deriving_show/run b/tests/base/deriving_show/run
new file mode 100755
index 000000000..21c937511
--- /dev/null
+++ b/tests/base/deriving_show/run
@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner DeriveShow.idr < input
\ No newline at end of file
diff --git a/tests/base/deriving_traversable/expected b/tests/base/deriving_traversable/expected
index 9530a9de8..74b69f663 100644
--- a/tests/base/deriving_traversable/expected
+++ b/tests/base/deriving_traversable/expected
@@ -68,7 +68,7 @@ LOG derive.traversable.clauses:1:
   traverseIVect : {0 m : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> IVect {n = m} a -> f (IVect {n = m} b)
   traverseIVect f (MkIVect x2) = MkIVect <$> (traverse f x2)
 LOG derive.traversable.clauses:1: 
-  traverseEqMap : {0 key, eq : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> EqMap key {{conArg:13793} = eq} a -> f (EqMap key {{conArg:13793} = eq} b)
+  traverseEqMap : {0 key, eq : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> EqMap key {{conArg:13922} = eq} a -> f (EqMap key {{conArg:13922} = eq} b)
   traverseEqMap f (MkEqMap x3) = MkEqMap <$> (traverse (traverse f) x3)
 LOG derive.traversable.clauses:1: 
   traverseTree : {0 l : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> Tree l a -> f (Tree l b)