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 )
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
Description: | modified (diff) |
---|
comment:2 Changed 18 months ago by
comment:3 Changed 16 months ago by
Keywords: | wipT2893 removed |
---|
comment:4 Changed 12 months ago by
Priority: | normal → low |
---|
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.
Interesting.
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, sinceEq a
is a superclass ofOrd a
, we discard it. So we infer a type likeNow 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.