Typeable instance for Constraint tupling

Question

I'm trying to derive a Typeable instance for tupled constraints. See the following code:

{-# LANGUAGE ConstraintKinds, GADTs #-}
{-# LANGUAGE DataKinds, PolyKinds, AutoDeriveTypeable #-}
{-# LANGUAGE StandaloneDeriving, DeriveDataTypeable #-}

import Data.Proxy
import Data.Typeable

data Foo (p :: (*, *))

data Dict ctx where
    Dict :: ctx => Dict ctx
  deriving (Typeable)

deriving instance Typeable '(,)
deriving instance Typeable Typeable
deriving instance Typeable Show

works :: IO ()
works = print (typeRep (Proxy :: Proxy (Foo '(Bool, Char))))

alsoWorks :: IO ()
alsoWorks = print (typeRep (Dict :: Dict (Show Bool)))

fails :: IO ()
fails = print (typeRep (Dict :: Dict (Show Bool, Typeable Bool)))

main :: IO ()
main = works >> alsoWorks >> fails

If you compile this with -fprint-explicit-kinds, the following error is given:

    No instance for (Typeable
                   (Constraint -> Constraint -> Constraint) (,))

Is there a way to derive such an instance? Everything I try refuses to disambiguate from the ★ -> ★ -> ★ constructor.

Answer 1

GHC can not currently make a Typeable instance, or any other instance, for (,) :: Constraint -> Constraint -> Constraint. The type constructor (,) only has kind * -> * -> *. There is no type constructor for products of the kind Constraint -> Constraint -> Constraint. The constructor (,) is overloaded to construct both tuples and products of Constraints, but has no corresponding type constructor when used to make a product of Constraints.

If we did have a type constructor for products of Constraints we should be able to define an instance as follows. For this, we'll pretend (,) is also a type constructor with kind (,) :: Constraint -> Constraint -> Constraint. To define an instance for it, we'd use KindSignatures and import GHC.Exts.Constraint to be able to talk about the kind of constraints explicitly

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE KindSignatures #-}

import GHC.Exts (Constraint)
import Data.Typeable

deriving instance Typeable ((,) :: Constraint -> Constraint -> Constraint)

If we do this now, it results in the following error, due to the kind of the (,) type constructor.

The signature specified kind `Constraint
                              -> Constraint -> Constraint',
  but `(,)' has kind `* -> * -> *'
In the stand-alone deriving instance for
  `Typeable ((,) :: Constraint -> Constraint -> Constraint)'

The constraints package also works with products of constraints, and includes the following note.

due to the hack for the kind of (,) in the current version of GHC we can't actually make instances for (,) :: Constraint -> Constraint -> Constraint

I presume the hack Edward Kmett is referring to is the overloading of the (,) constructor for Constraints without a corresponding type constructor.

Answer 2

It seems that it is not currently possible. There's a revealing comment in the latest version of constraint:

due to the hack for the kind of (,) in the current version of GHC we can't actually make instances for (,) :: Constraint -> Constraint -> Constraint