Improving the instances of Data.Functor.{Product,Sum}

Oleg Grenrus oleg.grenrus at
Sat Mar 14 15:43:26 UTC 2020

QuantifiedConstraints are not buggy, but they are not _complete_
(I do mean that as "buggy" = not sound, properly expressive = complete).

There are at least three issues:

1. Instance definition need UndecidableInstances (in my opinion this is 
big deal)
2. Instances are not elegant (easy to write, but not elegant).
3. QuantifiedConstraints resists to be abstracted over

See for
the standalone code file.

For the reasons below I wouldn't recommend using QuantifiedConstraints.
I very like them, but I'm not convinced the feature is ready for "prime 
To put into perspective, I think code classes of `singletons` are more 
ready to
be included in `base` than changing instances of Data.Functor.Sum and 
I do use singletons in my code more than QuantifiedConstraints. :)

I'm very worried how this change will affect libraries like `free` and
`recursion-schemes` and what builds on top of them.
This is not only change to `base`, it strongly guides how downstream
libraries should be written (or changed) as well.

On the other hand, I don't feel strongly about

     instance (Eq (f a), Eq (g a)) => Eq (Product f g a)

Yet, in the light of `free` it is "a step backwards".


Simple example with `newtype Fix f = Fix (f (Fix f))`

     class Eq1 f where
         liftEq :: (a -> b -> Bool) -> f a -> f b -> Bool

     class Eq1 f => Ord1 f where
         liftCompare :: (a -> b -> Ordering) -> f a -> f b -> Ordering

     instance Eq1 f => Eq (Fix f) where
         (==) = eq where eq (Fix x) (Fix y) = liftEq eq x y

     instance Ord1 f => Ord (Fix f) where
         compare = cmp where cmp (Fix x) (Fix y) = liftCompare cmp x y

works. It's boilerplate, but it's already written.

However, if we want to use QuantifiedConstraints,
then we

1. need UndecidableInstances
2. and then the code turns out to be less elegant:

instance (forall x. Eq x => Eq (f x)) => Eq (Fix f) where
     (==) = eq where eq (Fix x) (Fix y) = x == y

instance (forall x. Ord x => Ord (f x)) => Ord (Fix f) where
     compare = cmp where cmp (Fix x) (Fix y) = compare x y

fails to compile with

     GHCi, version 8.8.3:  :? for help
     [1 of 1] Compiling Main             ( Ord1.hs, interpreted )

     Ord1.hs:28:10: error:
         • Could not deduce (Ord x)
             arising from the superclasses of an instance declaration

we need to write Ord instance differently

    instance (forall x. Ord x => Ord (f x), forall x. Eq x => Eq (f x)) 
=> Ord (Fix f) where
        compare = cmp where cmp (Fix x) (Fix y) = compare x y

This _cannot_ be made to work:

     forall x. Ord x => Ord (f x)

doesn't entail

     forall x. Eq x => Eq (f x)

If you try to write defaultLiftEq using liftCompare

     defaultLiftEq :: Ord1 f => (a -> b -> Bool) -> f a -> f b -> Bool
     defaultLiftEq eq x y = EQ == liftCompare _problem_ x y

then you will se a problem.


Third issue is that We cannot abstract over QuantifiedConstraints.

Take an example `Dict`. We can use `Dict` for various things.

     data Dict :: (k -> Constraint) -> k -> * where
         Dict :: c a => Dict c a

It nicely uses PolyKinds extension so we can write:

     eqInt :: Dict Eq Int
     eqInt = Dict

     eq1List :: Dict Eq1 []
     eq1List = Dict

And we can use Dict to *manually* thread information

     entail :: Dict Ord1 f -> Dict Eq1 f
     entail Dict = Dict

The selling pitch of QuantifiedConstraints, that we could get this for free.
Above Ord (Fix) example however makes me suspicious. Let's try:

     eqQList :: Dict (forall x. Eq x => Eq (f x)) []
     eqQList = undefined

But it doesn't work!

     Ord1.hs:53:28: error:
         • Expected kind ‘(* -> *) -> Constraint’,
             but ‘Eq (f x)’ has kind ‘*’
         • In the first argument of ‘Dict’, namely
             ‘(forall x. Eq x => Eq (f x))’
           In the type signature:
             eqQList :: Dict (forall x. Eq x => Eq (f x)) []
     53 | eqQList :: Dict (forall x. Eq x => Eq (f x)) []

     Ord1.hs:53:36: error:
         • Expected a type, but ‘Eq (f x)’ has kind ‘Constraint’
         • In the first argument of ‘Dict’, namely
             ‘(forall x. Eq x => Eq (f x))’
           In the type signature:
             eqQList :: Dict (forall x. Eq x => Eq (f x)) []
     53 | eqQList :: Dict (forall x. Eq x => Eq (f x)) []
        |                                    ^^^^^^^^

Then we remember that we have seen that,
we **cannot define** type synonyms for quantified constraints

     type Eq1' f = forall x. Eq x => Eq (f x)

errors with

     Ord1.hs:56:33: error:
         • Expected a type, but ‘Eq (f x)’ has kind ‘Constraint’

Luckily GHC-8.10.1 (which is not released at the moment of writing)
will give us ability to say

     type Eq1' :: (* -> *) -> Constraint
     type Eq1' f = forall x. Eq x => Eq (f x)

This is promising! Let's try to fix eqQList

     eqQList2 :: Dict Eq1' []
     eqQList2 = undefined

But that doesn't work. Type-aliases have to be fully applied!

How in Haskell we fix issues when type-aliases (of classes) need to be 
evaluated? We defined

     class ... => Example a b c
     instance ... => Example a b c

Third try

     eqQList3 :: Dict Eq1'' f
     eqQList3 = Dict

The type signature is accepted, but the implementation is not

    Ord1.hs:67:12: error:
        • Could not deduce (Eq (f x)) arising from a use of ‘Dict’

At this point I'm clueless.


Best regards,

P.S. If we would like to take QuantifiedConstraints somewhere into use, 
then IMO we should start with MonadTrans class. IIRC it's well motivated 
in the paper. But UndecidableInstances is very unfortunate.

On 14.3.2020 16.10, chessai . wrote:
> I can second Richard's estimation of QuantifiedConstraints, I have 
> used them a lot in my own code since they were in HEAD. I consider it 
> a sufficiently stable feature to include in base or any library.
> On Sat, Mar 14, 2020, 4:16 AM Richard Eisenberg <rae at 
> <mailto:rae at>> wrote:
>>     On Mar 14, 2020, at 4:14 AM, Eric Mertens <emertens at
>>     <mailto:emertens at>> wrote:
>>     The last thing I'd heard about quantified constraints was that
>>     they were buggy and I've been avoiding relying on them. (I should
>>     probably review that assumptions at some point.)
>     Without expressing an opinion about chessai's proposal (which I
>     have not really thought about): quantified constraints are in good
>     shape and ready for prime time. They have limitations (e.g. you
>     can't mention a type family to the right of the =>), but when they
>     are valid, they work well. I'll never swear that a feature is
>     bug-free, but I think it's reasonable to consider using quantified
>     constraints in `base`.
>     Richard
> _______________________________________________
> Libraries mailing list
> Libraries at
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <>

More information about the Libraries mailing list