Typical Constraint Gating Instance

Question

I am trying to get a Typeable instance for limited restrictions. 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 any way to get such an instance? All that I'm trying to do does not eliminate the need for a constructor. ★ -> ★ -> ★ .

Answer 1

Currently, the GHC cannot create an instance of Typeable or any other instance for (,) :: Constraint -> Constraint -> Constraint . A constructor of type (,) has only * -> * -> * . There is no type constructor for such products Constraint -> Constraint -> Constraint . The constructor (,) overloaded to build both tuples and Constraint s products, but does not have an appropriate type constructor when used to create a Constraint s product.

If we had a type constructor for Constraint products, we could define an instance as follows. To do this, we will pretend that (,) also a type constructor with the form (,) :: Constraint -> Constraint -> Constraint . To define an instance for it, we will use KindSignatures and import GHC.Exts.Constraint to be able to explicitly talk about the types of constraints

 {-# 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 will result in the following error due to the type constructor of type (,) .

 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 constraint products and includes the following note .

due to a hack for type (,) in the current version of GHC, we can’t actually create instances for (,) :: Constraint -> Constraint -> Constraint

I assume Edward Kmett's hack is referring to constructor overloading (,) for Constraint without an appropriate type constructor.

Answer 2

It seems that this is currently not possible. There is a comment in the latest version of constraint :

due to hacking for the view (,) in the current version of GHC, we can’t actually create instances for (,) :: Constraint → Constraint → Constraint