Redundant constraints sometimes inferred and/or required
Summary
GHC sometimes infers or requires constraints with type families that are actually redundant due to a superclass constraint.
Steps to reproduce, and expected behavior
Load this code into GHCi:
{-# LANGUAGE TypeFamilies #-}
import Control.Monad.Trans.State
import Data.Bitraversable
import Data.Functor.Identity
import Data.Functor.Foldable
mapAccum func x ys = embed $ fmap (mapAccum func x') ys' where
(ys', x') = runState (bitraverse (\y -> StateT (\x -> Identity $ func x y)) pure (project ys)) x
Do :t mapAccum
and you'll get this:
mapAccum
:: (Base a ~ t1 t2, Base b ~ t1 c, Bitraversable t1, Recursive a,
Corecursive b, Functor (t1 c)) =>
(t3 -> t2 -> (c, t3)) -> t3 -> a -> b
But Functor (t1 c)
is redundant due to the presence of Corecursive b
and Base b ~ t1 c
. (In this case, manually specifying the type signature without the redundant constraint works fine.)
For another example, load this code into GHCi:
{-# LANGUAGE TypeFamilies #-}
type family SomeTypeFamily a :: * -> *
class Functor (SomeTypeFamily a) => SomeClass a where
foo :: SomeTypeFamily a b -> a -> b
bar :: t a b
bar = undefined
baz = foo (fmap id bar)
Do :t baz
and you'll get this:
baz
:: forall {k} {a1} {t :: k -> * -> *} {a2 :: k} {b}.
(SomeTypeFamily a1 ~ t a2, SomeClass a1, Functor (t a2)) =>
a1 -> b
I was hoping for just baz :: SomeClass a => a -> b
, since the information from the other constraints is already guaranteed by the superclass constraint on SomeClass
. (In this case, manually specifying that type signature doesn't work.)
Environment
- GHC version used: 9.2.1
Optional:
- Operating System: Ubuntu 20.04
- System Architecture: x86_64