Unfortunately, I inadvertently introduced a regression in the way derived Show instances for recursive singleton types work. To explain what I mean, consider the following code:

{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE UndecidableInstances #-}

#if __GLASGOW_HASKELL__ >= 806
{-# LANGUAGE QuantifiedConstraints #-}
#endif
module Bug where

import Data.Kind
import Data.Singletons.TH

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

main :: IO ()
main = print (sing :: Sing (X1 :: X Bool))

This compiles without issue in singletons-2.4. In singletons-2.5, however, it fails to compile with the following error:

$ /opt/ghc/8.6.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:27:8: error:
    • Reduction stack overflow; size = 201
      When simplifying the following type: Show (Sing z)
      Use -freduction-depth=0 to disable this check
      (any upper bound you could choose might fail unpredictably with
       minor updates to GHC, so disabling the check is recommended if
       you're sure that type checking should terminate)
    • In the expression: print (sing :: Sing (X1 :: X Bool))
      In an equation for ‘main’:
          main = print (sing :: Sing (X1 :: X Bool))
   |
27 | main = print (sing :: Sing (X1 :: X Bool))
   |        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

To see why this happens, consider the code that gets generated for the derived Show instances for X and Y:

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

This part typechecks fine. It's when you actually try to use it, as in print (sing :: Sing (X1 :: X Bool)), where the typechecker loops forever. Recall that ShowSing was changed in singletons-2.5 to be a type synonym:

type ShowSing k = (forall (z :: k). Show (Sing z) :: Constraint)

If you expand both occurrences of the ShowSing type synonym in the generated instances, you'll get:

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

Due to the way QuantifiedConstraints works, GHC will always favor local, quantified constraints in the instance contexts over top-level instances. Notice that there is both a top-level instance for Y a as well as a local, quantified instance for Y a in scope in the Show instance for X a, so GHC will favor the local instance during instance resolution. But when resolving the local instance for Y a, we are back in the same situation: there is both a top-level and local instance for X a, so the local instance is picked. When resolving that instance... we repeat the process and find ourselves in an infinite loop that eventually overflows the reduction stack. Eep.

I think the simplest solution to make ShowSing a class again. That is, redefine it like this:

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

All existing singletons code should continue to work with this version of ShowSing, and since using a class ties the recursive knot, it doesn't suffer from the infinite looping issue that is described above. As an added bonus, users no longer have to enable QuantifiedConstraints in all every module that singles a derived Show instance, since the use of QuantifiedConstraints is now localized entirely to the module that defines the ShowSing class.

Does this sound reasonable, @goldfirere? If so, this might be worth releasing a singletons-2.5.1 point release for, since this is a pretty nasty regression that prevents things like show (sing :: Sing '[True]) from typechecking, as I recently discovered.