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 :: Type) Source #

In addition to the promoted and singled versions of the `Show`

class that
`singletons-base`

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

In fact, this instance can be derived:

deriving instance`ShowSing`

k =>`Show`

(`SList`

(z :: [k]))

(Note that the actual definition of `ShowSing`

is slightly more complicated
than what this documentation might suggest. For the full story,
refer to the documentation for `ShowSing`

`.)

When singling a derived `Show`

instance, `singletons-th`

will also generate
a `Show`

instance for the corresponding singleton type using `ShowSing`

.
In other words, if you give `singletons-th`

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 (forall (sing :: k -> Type). sing ~ Sing => Show (sing z)) => ShowSing' (z :: k) 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.

The superclass of `ShowSing`

` is a bit peculiar:

class (forall (sing :: k -> Type). sing ~`Sing`

=>`Show`

(sing z)) =>`ShowSing`

` (z :: k)

One might wonder why this superclass is used instead of this seemingly more direct equivalent:

class`Show`

(`Sing`

z) =>`ShowSing`

` (z :: k)

Actually, these aren't equivalent! The latter's superclass mentions a type
family in its head, and this gives GHC's constraint solver trouble when
trying to match this superclass against other constraints. (See the
discussion beginning at
https://gitlab.haskell.org/ghc/ghc/-/issues/16365#note_189057 for more on
this point). The former's superclass, on the other hand, does *not* mention
a type family in its head, which allows it to match other constraints more
easily. It may sound like a small difference, but it's the only reason that
`ShowSing`

is able to work at all without a significant amount of additional
workarounds.

The quantified superclass has one major downside. Although the head of the
quantified superclass is more eager to match, which is usually a good thing,
it can bite under certain circumstances. Because

will
match a `Show`

(sing z)`Show`

instance for *any* types `sing :: k -> Type`

and `z :: k`

,
(where `k`

is a kind variable), it is possible for GHC's constraint solver
to get into a situation where multiple instances match

,
and GHC will get confused as a result. Consider this example:`Show`

(sing z)

-- As in Data.Singletons newtype`WrappedSing`

:: forall k. k -> Type where`WrapSing`

:: forall k (a :: k). {`unwrapSing`

::`Sing`

a } ->`WrappedSing`

a instance`ShowSing`

k =>`Show`

(`WrappedSing`

(a :: k)) where`showsPrec`

_ s =`showString`

"WrapSing {unwrapSing = " . showsPrec 0 s . showChar '}'

When typechecking the `Show`

instance for `WrappedSing`

, GHC must fill in a
default definition

, where
`show`

= defaultShow`defaultShow :: `

.
GHC's constraint solver has two possible ways to satisfy the
`Show`

(`WrappedSing`

a) => `WrappedSing`

a -> `String`

constraint for `Show`

(`WrappedSing`

a)`defaultShow`

:

- The top-level instance declaration for

itself, and`Show`

(`WrappedSing`

(a :: k))

from the head of the quantified constraint arising from`Show`

(sing (z :: k))

.`ShowSing`

k

In practice, GHC will choose (2), as local quantified constraints shadow
global constraints. This confuses GHC greatly, causing it to error out with
an error akin to `Couldn't match type Sing with WrappedSing`

. See
https://gitlab.haskell.org/ghc/ghc/-/issues/17934 for a full diagnosis of
the issue.

The bad news is that because of GHC#17934, we have to manually define `show`

(and `showList`

) in the `Show`

instance for `WrappedSing`

in order to avoid
confusing GHC's constraint solver. In other words, `deriving `

is a
no-go for `Show`

`WrappedSing`

. The good news is that situations like `WrappedSing`

are quite rare in the world of `singletons`

—most of the time, `Show`

instances for singleton types do *not* have the shape

, where `Show`

(sing (z :: k))`k`

is a polymorphic kind variable. Rather,
most such instances instantiate `k`

to a specific kind (e.g., `Bool`

, or
`[a]`

), which means that they will not overlap the head of the quantified
superclass in `ShowSing`

` as observed above.

Note that we define the single instance for `ShowSing`

` without the use of a
quantified constraint in the instance context:

instance`Show`

(`Sing`

z) =>`ShowSing`

` (z :: k)

We *could* define this instance with a quantified constraint in the instance
context, and it would be equally as expressive. But it doesn't provide any
additional functionality that the non-quantified version gives, so we opt
for the non-quantified version, which is easier to read.

# Orphan instances

ShowSing k => Show (WrappedSing a) Source # | |

showsPrec :: Int -> WrappedSing a -> ShowS # show :: WrappedSing a -> String # showList :: [WrappedSing a] -> ShowS # | |

ShowSing k => Show (SWrappedSing ws) Source # | |

showsPrec :: Int -> SWrappedSing ws -> ShowS # show :: SWrappedSing ws -> String # showList :: [SWrappedSing ws] -> ShowS # |