How to put constraints on type variable of kind `Constraint`?

The new QuantifiedConstraints extension allows this.

class (a => b) => Implies a b where
instance (a => b) => Implies a b where
instance (forall a. c a `Implies` Show a) => Show (Some c) where
  show (Some x) = show x

Within the body of the Show instance, it is as if there is a

instance forall a. Implies (c a) (Show a)

in scope. If you then have T :: Type and know c T, then the superclass of c T => Show T of the specialized Implies (c T) (Show T) instance allows you to derive Show T. It is necessary to use Implies instead of a straight forall a. c a => Show a constraint. This incorrect constraint acts like

instance forall a. c a => Show a

which overlaps with every Show instance, causing weird breakage. Forcing an indirection through the superclass of an otherwise useless constraint fixes everything.

The closest we are able to get is a Class1 class that reifys the relationship between a class and a single superclass constraint as a class. It's based on the Class from constraints.

First, we'll take a short tour of the constraints package. A Dict captures the dictionary for a Constraint

data Dict :: Constraint -> * where
  Dict :: a => Dict a

:- captures that one constraint entails another. If we have a :- b, whenever we have the constraint a we can produce the dictionary for the constraint b.

newtype a :- b = Sub (a => Dict b)

We need a proof similar to :-, we need to know that forall a. h a :- b a, or h a => Dict (b a).

Single Inheritance

Actually implementing this for classes with just single inheritance requires the kitchen sink of language extensions, including OverlappingInstances.

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE OverlappingInstances #-}

import Data.Constraint

We'll define the class of constraints of kind k -> Constraint where the constraint has a single superclass.

class Class1 b h | h -> b where
    cls1 :: h a :- b a

We're now equipped to tackle our example problem. We have a class A that requires a Show instance.

 class Show a => A a
 instance A Int

Show is a superclass of A

instance Class1 Show A where
    cls1 = Sub Dict 

We want to write Show instances for Some

data Some (c :: * -> Constraint) where
    Some :: c a => a -> Some c

We can Show a Some Show.

instance Show (Some Show) where
    showsPrec x (Some a) = showsPrec x a

We can Show a Some h whenever h has a single superclass b and we could show Some b.

instance (Show (Some b), Class1 b h) => Show (Some h) where
    showsPrec x (Some (a :: a)) = 
        case cls1 :: h a :- b a of
            Sub Dict -> showsPrec x ((Some a) :: Some b)

This lets us write

x :: Some A
x = Some (1 :: Int)

main = print x