Constraint subset higher-order constraint

Question

Using the GHC.Exts.Constraint kind, I have a generalized existentially quantified data structure like this:

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

(In reality, my type is more complex than this; this is just a reduced example)

Now, let's say that I have a function which, for example, requires the Enum constraint, that I want to act on Some c's. What I need to do is to check whether the Enum constraint is implied by c:

succSome :: Enum ⊆ c => Some c -> Some c
succSome (Specimen a) = Specimen $ succ a

How would I implement the ⊆ operator in this case? Is it possible?

Answer 1

First note that Enum and c are not constraints by themselves: They have kind * -> Constraint, not kind Constraint. So what you want to express with Enum ⊆ c is: c a implies Enum a for all a.

Step 1 (explicit witnesses)

With :- from Data.Constraint, we can encode a witness of the constraint d ⊆ c at the value level:

type Impl c d = forall a . c a :- d a

We would like to use Impl in the definition of succSome as follows:

succSome :: Impl c Enum -> Some c -> Some c
succSome impl (Specimen a) = (Specimen $ succ a) \\ impl

But this fails with a type error, saying that GHC cannot deduce c a0 from c a. Looks like GHC chooses the very general type impl :: forall a0 . c a0 :- d a0 and then fails to deduce c a0. We would prefer the simpler type impl :: c a :- d a for the type variable a that was extracted from the Specimen. Looks like we have to help type inference along a bit.

Step 2 (explicit type annotation)

In order to provide an explicit type annotation to impl, we have to introduce the a and c type variables (using the ScopedTypeVariables extension).

succSome :: forall c . Impl c Enum -> Some c -> Some c
succSome impl (Specimen (a :: a)) = (Specimen $ succ a) \\ (impl :: c a :- Enum a)

This works, but it is not exactly what the questions asks for.

Step 3 (using a type class)

The questions asks for encoding the d ⊆ c constraint with a type class. We can achieve this by having a class with a single method:

class Impl c d where
  impl :: c a :- d a

succSome :: forall c . Impl c Enum => Some c -> Some c
succSome (Specimen (a :: a)) = (Specimen $ succ a) \\ (impl :: c a :- Enum a)

Step 4 (usage example)

To actually use this, we have to provide instances for Impl. For example:

instance Impl Integral Enum where
  impl = Sub Dict

value :: Integral a => a
value = 5

specimen :: Some Integral
specimen = Specimen value

test :: Some Integral
test = succSome specimen