singletons-3.0.3: Basic singleton types and definitions

Copyright | (C) 2017 Ryan Scott
License | BSD-style (see LICENSE)
Maintainer | Ryan Scott
Stability | experimental
Portability | non-portable
Safe Haskell | Safe-Inferred
Language | Haskell2010

Data.Singletons.ShowSing

Contents

- The `ShowSing` type
- Internal utilities
- Orphan instances

Description

Defines the class `ShowSing` which is useful for defining `Show` instances for singleton types. Because `ShowSing` crucially relies on `QuantifiedConstraints`, it is only defined if this library is built with GHC 8.6 or later.

Synopsis

- class (forall (z :: k). ShowSing' z) => ShowSing (k :: Type)
- class (forall (sing :: k -> Type). sing ~ Sing => Show (sing z)) => ShowSing' (z :: k)

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

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

Instances details

(forall (z :: k). ShowSing' z) => ShowSing k Source # |
Instance details 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 ``Show` (`Sing` z)` with `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 ``Show` (sing z)` will match a `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 ``Show` (sing z)`, and GHC will get confused as a result. Consider this example:

    -- 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 ``show` = defaultShow`, where `defaultShow :: `Show` (`WrappedSing` a) => `WrappedSing` a -> `String``. GHC's constraint solver has two possible ways to satisfy the ``Show` (`WrappedSing` a)` constraint for `defaultShow`:

1. The top-level instance declaration for ``Show` (`WrappedSing` (a :: k))` itself, and
2. ``Show` (sing (z :: k))` from the head of the quantified constraint arising from ``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 `Show`` is a no-go for `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 ``Show` (sing (z :: k))`, where `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.

#### Instances

Instances details

Show (Sing z) => ShowSing' (z :: k) Source # |
Instance details Defined in Data.Singletons.ShowSing

# Orphan instances

ShowSing k => Show (WrappedSing a) Source # |
Instance details Methods showsPrec :: Int -> WrappedSing a -> ShowS Source # show :: WrappedSing a -> String Source # showList :: [WrappedSing a] -> ShowS Source #
ShowSing k => Show (SWrappedSing ws) Source # |
Instance details Methods showsPrec :: Int -> SWrappedSing ws -> ShowS Source # show :: SWrappedSing ws -> String Source # showList :: [SWrappedSing ws] -> ShowS Source #