The plugin seem not able to use associativity of addition

[Mikolaj]

The plugin can't solve: Expected: ShapeInt (((m6 + k1) + n14) + (n + k3)) Actual: ShapeInt ((((m6 + k1) + n14) + n) + k3).

A longer fragment of the error message with GHC 9.4.4:

simplified/HordeAd/Core/AstVectorize.hs:435:42: error:
    • Could not deduce (((k2 + m7) - 1) ~ n14)
      from the context: (KnownNat n13, (1 + n13) ~ ((k1 + k2) + k3))
        bound by a pattern with pattern synonym:
                   :. :: forall (n1 :: GHC.TypeNats.Nat) i.
                         KnownNat n1 =>
                         forall (n :: GHC.TypeNats.Nat).
                         (KnownNat n, (1 + n) ~ n1) =>
                         i -> Index n i -> Index n1 i,
                 in an equation for ‘projectGatherN’
        at simplified/HordeAd/Core/AstVectorize.hs:425:26-36
      or from: ((m7 + k2) ~ (1 + n14), KnownNat n14)
        bound by a pattern with constructor:
                   ::: :: forall (n1 :: GHC.TypeNats.Nat) i.
                          KnownNat n1 =>
                          i -> SizedList n1 i -> SizedList (1 + n1) i,
                 in an equation for ‘projectGatherN’
        at simplified/HordeAd/Core/AstVectorize.hs:426:26-57
      or from: (KnownNat n15,
                (1 + n15) ~ (((((m6 + k1) + m7) + k2) + n) + k3))
        bound by a pattern with pattern synonym:
                   :$ :: forall (n1 :: GHC.TypeNats.Nat) i.
                         KnownNat n1 =>
                         forall (n :: GHC.TypeNats.Nat).
                         (KnownNat n, (1 + n) ~ n1) =>
                         i -> Shape n i -> Shape n1 i,
                 in an equation for ‘projectGatherN’
        at simplified/HordeAd/Core/AstVectorize.hs:427:22-67
      Expected: ShapeInt (((m6 + k1) + n14) + (n + k3))
        Actual: ShapeInt ((((m6 + k1) + n14) + n) + k3)
      ‘n14’ is a rigid type variable bound by

To reproduce, compile the following branch: https://github.com/Mikolaj/horde-ad/tree/plugin-associativity

Use allow-newer if needed.