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