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

Question

I'm playing around with the `ConstraintKinds` extension of GHC. I have the following data type, which is just a box for things fulfilling some one parameter constraint `c`: ``` data Some (c :: * -> Constraint) where Some :: forall a. c a => a -> Some c ``` For example, I could construct a box with some kind of number (arguably not very useful). ``` x :: Some Num x = Some (1 :: Int) ``` Now, as long as `c` includes the constraint `Show`, I could provide an instance of `Show (Some c)`. ``` instance ??? => Show (Some c) where show (Some x) = show x -- Show dictionary for type of x should be in scope here ``` But how do I express this requirement in the instance context (marked with `???`)? I cannot use an equality constraint (`c ~ Show`), because the two are not necessarily equal. `c` could be `Num`, which implies, but is not equal to, `Show`. Edit I realised that this cannot be possible in general. If you have two values of type `Some Eq`, it is not possible to compare them for equality…

Accepted Answer

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 `class`es 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
```

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

Solution

Problem

Related problems