Copyright | (C) 2017 Ryan Scott |
---|---|

License | BSD-style (see LICENSE) |

Maintainer | Ryan Scott |

Stability | experimental |

Portability | non-portable |

Safe Haskell | None |

Language | Haskell2010 |

# The

`ShowSing`

type

class (forall (z :: k). ShowSing' z) => ShowSing k Source #

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 `(`

. But this isn't quite right, as the
type variable `Show`

(`Sing`

(a :: k)))`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. `

, which demands that there be an instance
for `Show`

(`Sing`

(a :: k)))

that is parametric in the use of `Show`

(`Sing`

(a :: k))`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. `

. With `Show`

(`Sing`

(a :: k)))`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!

#### Instances

(forall (z :: k). ShowSing' z) => ShowSing k Source # | |

Defined in Data.Singletons.ShowSing |

# Internal utilities

class Show (Sing z) => ShowSing' z Source #

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

with `Show`

(`Sing`

z)`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

constraint. This is due to
another unfortunate GHC bug
that prevents GHC from realizing that `Show`

(`Sing`

x)

implies
`ShowSing`

k

. The workaround is to force GHC to come to its
senses by using an explicit type signature:`Show`

(`Sing`

(x :: k))

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

and
`ShowSing`

k

. (The `Show`

(`Sing`

(x :: k))`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 `

will not insert these explicit signatures for us,
it is not possible to derive `Show`

`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.