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