Opened 19 months ago

Last modified 12 months ago

#14896 new bug

QuantifiedConstraints: GHC does doesn't discharge constraints if they are quantified

Reported by: Iceland_jack Owned by:
Priority: low Milestone:
Component: Compiler Version: 8.5
Keywords: QuantifiedConstraints Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by Iceland_jack)

This came up on a reddit thread,

{-# Language QuantifiedConstraints #-}

class (forall aa. Functor (bi aa)) => Bifunctor bi where
  first :: (a -> a') -> (bi a b -> bi a' b)

bimap :: Bifunctor bi => (a -> a') -> (b -> b') -> (bi a b -> bi a' b')
bimap f g = first f . fmap g

This is the type we want for bimap even if we mix & match Bifunctor and Functor. We already know that we can fmap @(bi xx) for any xx but this is not the inferred type.

Instead GHC infers a type (tidied up) with a superfluous Functor constraint

bimap :: (Bifunctor bi, Functor (bi a)) => (a -> a') -> (b -> b') -> (bi a b -> bi a' b')

Indeed post-composing with a superfluous fmap @(bi a') id incurs yet another Functor constraint

bimap :: (Bifunctor bi, Functor (bi a), Functor (bi a')) => (a -> a') -> (b -> b') -> (bi a b -> bi a' b')
bimap f g = fmap id . first f . fmap g

A terminology question, I'm not sure how to phrase what GHC isn't doing to the Functor constraints: ‘discharge’?

Change History (4)

comment:1 Changed 19 months ago by Iceland_jack

Description: modified (diff)

comment:2 Changed 18 months ago by simonpj


When inferring a type, GHC finds all the unsolved constraints. Supopse they are (Eq a, Ord a). Then it minimises them in a very simple-minded way, dicarding any that are implied by the superclasses of some other constraint. So, since Eq a is a superclass of Ord a, we discard it. So we infer a type like

f :: Ord a => blah

Now suppose we have (Bifunctor bi, Functor (bi a)). Yes, the latter is implied by the former, but now it is much more indirect.

I'm not yet sure how to do a better job here.

comment:3 Changed 16 months ago by RyanGlScott

Keywords: wipT2893 removed

comment:4 Changed 12 months ago by dfeuer

Priority: normallow

Reducing the priority for now. I'll bump it back up if someone comes up with a situation where this actually prevents valid code from compiling.

Note: See TracTickets for help on using tickets.