singletons-2.5 regression: derived Show instances for recursive singleton types loop at compile time

[RyanGlScott]

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.

[RyanGlScott]

#372 would fix this.

[goldfirere]

I don't agree with the analysis here. Let's re-examine:

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

(Surely you meant it with those extra parens toward the end.) I say show SX1. That gives us a Wanted Show (Sing X1). GHC will choose the first instance. Then, we get a Wanted forall z. Show (Sing (z :: Y alpha)) (where alpha is the unification variable invented because we don't know the X1's kind's index). GHC invents an arbitrary z :: Y alpha (this is skolemization) and tries to solve Show (Sing z). This uses the second instance. GHC now invents an arbitrary z1 :: X alpha and tries to solve Show (Sing z1). Now we go back to the first instance. And so it goes.

In contrast to the analysis above, the problem isn't from overlapping instances. That would happen only with Givens (say, when type-checking the instances), but everything here is a Wanted. No, the problem is that GHC's solver can't deal with this scenario. It would need to remember that it's really solving, e.g. forall (z :: X alpha). Show (Sing z) instead of solving for some specific (but arbitrary) z. Then, when it recurs, it can find the quantified constraint in its inert set, and build a recursive dictionary the way it normally does in mutually-recursive instance scenarios. I don't think this would be too hard, actually.

I think this is squarely GHC's problem, not ours.

Of course, we don't want our users to suffer just because we haughtily declare that we're right and GHC is wrong. So bring on #372, while posting this to GHC proper.

[goldfirere]

Minimized example, about to be posted to GHC:

data T1 a
data T2 a

class C a where
  meth :: a

instance (forall a. C (T2 a)) => C (T1 a) where
  meth = error "instance T1"

instance (forall a. C (T1 a)) => C (T2 a) where
  meth = error "instance T2"

example :: T1 Int
example = meth

[goldfirere]

Posted #15888.

[RyanGlScott]

Well, I'm glad that someone in the know thinks that this behavior of GHC is a bug. My fear was that if I posted the actual place where I discovered this bug:

deriving instance (forall z. Show (Sing (z :: a)), forall z. Show (Sing (z :: [a])))
  => Show (Sing (z :: [a])))

Then it would be written off as an obvious infinite loop (due to the fact that we have Show (Sing (z :: [a])) directly in both the context and the instance head). Are you claiming that this instance shouldn't loop either?

[goldfirere]

That instance should be OK, too. After all, GHC accepts instance C a => C a today.

[RyanGlScott]

In that case, I'll update #372 to indicate that the whole thing is a workaround for Trac #15888, then land it and make a point release.

[RyanGlScott]

Now that I've released singletons-2.5.1 to Hackage, this should finally be resolved.