A type equality constraint is necessary despite GHC warning that it's redundant

Summary

The first type equality in this type signature

cfwd
  :: forall r y f vals advals.
     ( RankedOf f ~ Flip OR.Array
     , AdaptableHVector (ADVal (Flip OR.Array)) advals
     , AdaptableHVector (ADVal (Flip OR.Array)) (ADVal f r y)
     , AdaptableHVector (Flip OR.Array) vals
     , AdaptableHVector (Flip OR.Array) (f r y)
     , DualNumberValue advals, vals ~ DValue advals )
  => (advals -> ADVal f r y) -> vals -> vals -> f r y

is reported as redundant by GHC 9.8.1 (with both -O0 and -O1, with GHC 9.6.4 only with -O1) but the typing fails with the equality removed with

test/simplified/TestAdaptorSimplified.hs:1629:22: error: [GHC-40404]
    • Reduction stack overflow; size = 201
      When simplifying the following type:
        Show
          (HordeAd.Core.Delta.DeltaS
             (ShapedOf
                @GHC.TypeNats.Nat
                (RankedOf
                   @[GHC.TypeNats.Nat]
                   (ShapedOf
                      @GHC.TypeNats.Nat
                      (RankedOf
                         @[GHC.TypeNats.Nat]
                         (ShapedOf

etc.

Steps to reproduce

Checkout https://github.com/Mikolaj/horde-ad/blob/b42aeabc0cb9fdbc8933ddd444143d008a5b986f.

Run with GHC 9.8.1 or later (probably):

cabal test simplifiedOnlyTest -ftest_seq --test-options='-p 4Sin' --allow-newer --disable-optimization

After a dozen files tt should warn the equality is redundant and after another dozen it should start running the tests (all run fine). Remove the equality, run again, a few files later the error from above should pop up.

Expected behavior

I have no idea if the type equality is really needed (or maybe a much weaker equality would be enough, e.g., RankedOf (ShapedOf ranked) ~ ranked?). I expect GHC to tell what it is so that I don't have to think.

Environment

• GHC version used: 9.8.1 and 9.6.4