In addition to the promoted and singled versions of the Show class that singletons provides, it is also useful to be able to directly define Show instances for singleton types themselves. Doing so is almost entirely straightforward, as a derived Show instance does 90 percent of the work. The last 10 percent—getting the right instance context—is a bit tricky, and that's where ShowSing comes into play.

As an example, let's consider the singleton type for lists. We want to write an instance with the following shape:

instance ??? => Show (SList (z :: [k])) where
  showsPrec p SNil = showString "SNil"
  showsPrec p (SCons sx sxs) =
    showParen (p > 10) $ showString "SCons " . showsPrec 11 sx
                       . showSpace . showsPrec 11 sxs

To figure out what should go in place of ???, observe that we require the type of each field to also be Show instances. In other words, we need something like (Show (Sing (a :: k))). But this isn't quite right, as the type variable a doesn't appear in the instance head. In fact, this a type is really referring to an existentially quantified type variable in the SCons constructor, so it doesn't make sense to try and use it like this.

Luckily, the QuantifiedConstraints language extension provides a solution to this problem. This lets you write a context of the form (forall a. Show (Sing (a :: k))), which demands that there be an instance for Show (Sing (a :: k)) that is parametric in the use of a. This lets us write something closer to this:

instance (forall a. Show (Sing (a :: k))) => SList (Sing (z :: [k])) where ...

The ShowSing class is a thin wrapper around (forall a. Show (Sing (a :: k))). With ShowSing, our final instance declaration becomes this:

instance ShowSing k => Show (SList (z :: [k])) where
  showsPrec p SNil = showString "SNil"
  showsPrec p (SCons (sx :: Sing x) (sxs :: Sing xs)) =
    (showParen (p > 10) $ showString "SCons " . showsPrec 11 sx
                        . showSpace . showsPrec 11 sxs)
      :: (ShowSing' x, ShowSing' xs) => ShowS

(Note that the actual definition of ShowSing is slightly more complicated than what this documentation might suggest. For the full story, as well as an explanation of why we need an explicit (ShowSing' x, ShowSing' xs) => ShowS signature at the end, refer to the documentation for ShowSing`.)

When singling a derived Show instance, singletons will also generate a Show instance for the corresponding singleton type using ShowSing. In other words, if you give singletons a derived Show instance, then you'll receive the following in return:

• A promoted (PShow) instance
• A singled (SShow) instance
• A Show instance for the singleton type

What a bargain!

The workhorse that powers ShowSing. The only reason that ShowSing` exists is to work around GHC's inability to put type families in the head of a quantified constraint (see this GHC issue for more details on this point). In other words, GHC will not let you define ShowSing like so:

class (forall (z :: k). Show (Sing z)) => ShowSing k

By replacing Show (Sing z) with ShowSing' z, we are able to avoid this restriction for the most part. There is one major downside to using ShowSing', however: deriving Show instances for singleton types does not work out of the box. In other words, if you try to do this:

deriving instance ShowSing k => Show (SList (z :: [k]))

Then GHC will complain to the effect that it could not deduce a Show (Sing x) constraint. This is due to another unfortunate GHC bug that prevents GHC from realizing that ShowSing k implies Show (Sing (x :: k)). The workaround is to force GHC to come to its senses by using an explicit type signature:

instance ShowSing k => Show (SList (z :: [k])) where
  showsPrec p SNil = showString "SNil"
  showsPrec p (SCons (sx :: Sing x) (sxs :: Sing xs)) =
    (showParen (p > 10) $ showString "SCons " . showsPrec 11 sx
                        . showSpace . showsPrec 11 sxs)
      :: (ShowSing' x, ShowSing' xs) => ShowS

The use of ShowSing' x in the signature is sufficient to make the constraint solver connect the dots between ShowSing k and Show (Sing (x :: k)). (The ShowSing' xs constraint is not strictly necessary, but it is shown here since that is in fact the code that singletons will generate for this instance.)

Because deriving Show will not insert these explicit signatures for us, it is not possible to derive Show instances for singleton types. Thankfully, singletons' Template Haskell machinery can do this manual gruntwork for us 99% of the time, but if you ever find yourself in a situation where you must define a Show instance for a singleton type by hand, this is important to keep in mind.

Note that there is one potential future direction that might alleviate this pain. We could define ShowSing` like this instead:

class (forall sing. sing ~ Sing => Show (sing z)) => ShowSing' z
instance Show (Sing z) => ShowSing' z

For many examples, this lets you just derive Show instances for singleton types like you would expect. Alas, this topples over on Bar in the following example:

newtype Foo a = MkFoo a
data SFoo :: forall a. Foo a -> Type where
  SMkFoo :: Sing x -> SFoo (MkFoo x)
type instance Sing = SFoo
deriving instance ShowSing a => Show (SFoo (z :: Foo a))

newtype Bar a = MkBar (Foo a)
data SBar :: forall a. Bar a -> Type where
  SMkBar :: Sing x -> SBar (MkBar x)
type instance Sing = SBar
deriving instance ShowSing (Foo a) => Show (SBar (z :: Bar a))

This fails because of—you guessed it—another GHC bug. Bummer. Unless that bug were to be fixed, the current definition of ShowSing` is the best that we can do.