Constraining constraints

constraint-kinds, ghc, haskell

Solution

The `constraints` package provides a solution to this problem, via its `:-` ("entails") type:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}

import GHC.Exts

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

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

g, g' :: c2 a => c2 a :- c1 a -> (forall b. c1 b => b) -> a
g (Sub Dict) x = x

Then, by passing in an appropriate witness, we can recover the original example:

integralImpliesNum :: Integral a :- Num a
integralImpliesNum = Sub Dict

f :: Integral a => (forall b. Num b => b) -> a
f = g integralImpliesNum

In fact, this `g` is merely a flipped and specialized version of the `\\` operator:

(\\) :: a => (b => r) -> (a :- b) -> r
r \\ Sub Dict = r
infixl 1 \\

g' = flip (\\)

If you have the time, Edward Kmett's talk "Type Classes vs the World" is a great introduction to how this all works.

Problem

I can write the following: ``` {-# LANGUAGE RankNTypes #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE ConstraintKinds #-} f :: Integral a => (forall b. Num b => b) -> a f = id ``` And all is good. Presumably GHC can derive `Integral` from `Num` so all is well. I can be a bit tricker, yet I'm still fine: ``` class Integral x => MyIntegral x instance Integral x => MyIntegral x class Num x => MyNum x instance Num x => MyNum x f' :: MyIntegral a => (forall b. MyNum b => b) -> a f' = id ``` So lets say I want to generalise this, like so: ``` g :: c2 a => (forall b. c1 b => b) -> a g = id ``` Now obviously this will spit the dummy, because GHC can not derive `c2` from `c1`, as `c2` is not constrained. What do I need to add to the type signature of `g` to say that "you can derive `c2` from `c1`"?

Original source