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.

Chicanery

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.

Stan

The error message No instance for (Typeable (Constraint -> Constraint -> Constraint) (,)) seems to imply that a type constructor exists internally somehow. If it only had a name we could get at... – Hammerskjold

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

Photoneutron

Your comment about kmett it harmful to the community. Not disparaging his abilities in the least, but let's not have gods. – Supergalaxy

@Supergalaxy Very well, replaced by something hopefully innocuous. – Hammerskjold