6

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"?

Clinton
  • 22,361
  • 15
  • 67
  • 163
  • 1
    When you say "derive X from Y", I'd rather say "derive Y from X". In your first example, we have that `Integral t` implies `Num t`, and not the other way around. GHC has to extract a `Num` dictionary from the passed `Integral` one. And similarly for the other cases you mention below. – chi May 07 '17 at 05:16

1 Answers1

7

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.

Lambda Fairy
  • 13,814
  • 7
  • 42
  • 68