Restriction of restrictions

Question

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 everything's good. Presumably, GHC can get Integralout Num, so all is well.

I can get a little confused, but still good:

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, let's say I want to summarize it like this:

g :: c2 a => (forall b. c1 b => b) -> a
g = id

Now it’s obvious that this will affect the dummy because the GHC cannot get c2out c1, because it is c2not limited.

What needs to be added to the type signature gto say that "you can get c2from c1"?

Answer 1

The package constraintsprovides a solution to this problem using the :-("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

, , :

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

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

, g \\:

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

g' = flip (\\)

, "Type Classes vs the World" - , .