{-# LANGUAGE CPP #-}

#if __GLASGOW_HASKELL__ >= 806
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

#if __GLASGOW_HASKELL__ >= 810
{-# LANGUAGE StandaloneKindSignatures #-}
#endif
#endif

-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Singletons.ShowSing
-- Copyright   :  (C) 2017 Ryan Scott
-- License     :  BSD-style (see LICENSE)
-- Maintainer  :  Ryan Scott
-- Stability   :  experimental
-- Portability :  non-portable
--
-- 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.
--
----------------------------------------------------------------------------

module Data.Singletons.ShowSing (
#if __GLASGOW_HASKELL__ >= 806
  -- * The 'ShowSing' type
  ShowSing,

  -- * Internal utilities
  ShowSing'
#endif
  ) where

#if __GLASGOW_HASKELL__ >= 806
import Data.Kind
import Data.Singletons
import Text.Show

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

-- One might wonder we we simply don't define ShowSing as
-- @type ShowSing k = (forall (z :: k). ShowSing' z)@ instead of going the
-- extra mile to define it as a class.
-- See Note [Define ShowSing as a class, not a type synonym] for an explanation.
#if __GLASGOW_HASKELL__ >= 810
type ShowSing :: Type -> Constraint
#endif
class    (forall (z :: k). ShowSing' z) => ShowSing (k :: Type)
instance (forall (z :: k). ShowSing' z) => ShowSing (k :: Type)

-- | 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
-- <https://gitlab.haskell.org/ghc/ghc/issues/14860 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.
#if __GLASGOW_HASKELL__ >= 810
type ShowSing' :: k -> Constraint
#endif
class    (forall (sing :: k -> Type). sing ~ Sing => Show (sing z))
                       => ShowSing' (z :: k)
instance Show (Sing z) => ShowSing' (z :: k)

{-
Note [Define ShowSing as a class, not a type synonym]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In an ideal world, we would simply define ShowSing like this:

  type ShowSing k = (forall (z :: k). ShowSing' z) :: Constraint)

In fact, I used to define ShowSing in a manner similar to this in version 2.5
of singletons. However, I realized some time after 2.5's release that the
this encoding is unfeasible at the time being due to GHC Trac #15888.

To be more precise, the exact issue involves an infelicity in the way
QuantifiedConstraints interacts with recursive type class instances.
Consider the following example (from #371):

  $(singletons [d|
    data X a = X1 | X2 (Y a) deriving Show
    data Y a = Y1 | Y2 (X a) deriving Show
    |])

This will generate the following instances:

  deriving instance ShowSing (Y a) => Show (Sing (z :: X a))
  deriving instance ShowSing (X a) => Show (Sing (z :: Y a))

So far, so good. Now, suppose you try to actually `show` a singleton for X.
For example:

  show (sing @(X1 :: X Bool))

Somewhat surprisingly, this will be rejected by the typechecker with the
following error:

    • Reduction stack overflow; size = 201
      When simplifying the following type: Show (Sing z)

To see why this happens, observe what goes on if we expand the occurrences of
the ShowSing type synonym in the generated instances:

  deriving instance (forall z. ShowSing' (z :: Y a)) => Show (Sing (z :: X a))
  deriving instance (forall z. ShowSing' (z :: X a)) => Show (Sing (z :: Y a))

Due to the way QuantifiedConstraints currently works (as surmised in Trac
#15888), when GHC has a Wanted `ShowSing' (X1 :: X Bool)` constraint, it
chooses the appropriate instance and emits a Wanted
`forall z. ShowSing' (z :: Y Bool)` constraint (from the instance context).
GHC skolemizes the `z` to `z1` and tries to solve a Wanted
`ShowSing' (z1 :: Y Bool)` constraint. GHC chooses the appropriate instance
and emits a Wanted `forall z. ShowSing' (z :: X Bool)` constraint. GHC
skolemizes the `z` to `z2` and tries to solve a Wanted
`ShowSing' (z2 :: X Bool)` constraint... we repeat the process and find
ourselves in an infinite loop that eventually overflows the reduction stack.
Eep.

Until Trac #15888 is fixed, there are two possible ways to work around this
problem:

1. Make derived instances' type inference more clever. If you look closely,
   you'll notice that the `ShowSing (X a)`/`ShowSing (Y a)` constraints in
   the generated instances are entirely redundant and could safely be left
   off. But determining this would require significantly improving singletons-th'
   Template Haskell capabilities for type inference, which is a path that we
   usually spurn in favor of keeping the generated code dumb but predictable.
2. Define `ShowSing` as a class (with a single instance) instead of a type
   synonym. `ShowSing`-as-a-class ties the recursive knot during instance
   resolution and thus avoids the problems that the type synonym version
   currently suffers from.

Given the two options, (2) is by far the easier option, so that is what we
ultimately went with.
-}

------------------------------------------------------------
-- (S)WrappedSing instances
------------------------------------------------------------

-- Note that we cannot derive this Show instance due to
-- https://gitlab.haskell.org/ghc/ghc/-/issues/17934. The Haddocks for
-- ShowSing' contain a lengthier explanation of how GHC#17934 relates to
-- ShowSing.
instance ShowSing k => Show (WrappedSing (a :: k)) where
  showsPrec :: Int -> WrappedSing a -> ShowS
showsPrec = Int -> WrappedSing a -> ShowS
forall k (a :: k). ShowSing k => Int -> WrappedSing a -> ShowS
showsWrappedSingPrec
  show :: WrappedSing a -> String
show WrappedSing a
x = Int -> WrappedSing a -> ShowS
forall k (a :: k). ShowSing k => Int -> WrappedSing a -> ShowS
showsWrappedSingPrec Int
0 WrappedSing a
x String
""
  showList :: [WrappedSing a] -> ShowS
showList = (WrappedSing a -> ShowS) -> [WrappedSing a] -> ShowS
forall a. (a -> ShowS) -> [a] -> ShowS
showListWith (Int -> WrappedSing a -> ShowS
forall k (a :: k). ShowSing k => Int -> WrappedSing a -> ShowS
showsWrappedSingPrec Int
0)

showsWrappedSingPrec :: ShowSing k => Int -> WrappedSing (a :: k) -> ShowS
showsWrappedSingPrec :: Int -> WrappedSing a -> ShowS
showsWrappedSingPrec Int
p (WrapSing Sing a
s) = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
  String -> ShowS
showString String
"WrapSing {unwrapSing = " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Sing a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
0 Sing a
s ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
'}'

deriving instance ShowSing k => Show (SWrappedSing (ws :: WrappedSing (a :: k)))
#endif