The plugin (or GHC?) seems to think that (0 + n) + (k - n) == n + n

[Mikolaj]

Tested with GHC 9.8.1. The repro (cabal build --allow-newer is enough) is at https://github.com/Mikolaj/horde-ad/tree/repro-of-nkn. The full error is the one that shows last on the screen:

src/HordeAd/Core/TensorADVal.hs:812:49: error: [GHC-25897]
    • Could not deduce ‘(n + n :: GHC.Num.Natural.Natural)
                        ~ (k :: GHC.TypeNats.Nat)’
      from the context: (ADReady ranked,
                         ADReadySmall
                           (ADVal @GHC.TypeNats.Nat ranked)
                           (ADVal @[GHC.TypeNats.Nat] shaped),
                         CRankedIP ranked (IsPrimal @GHC.TypeNats.Nat),
                         UnletGradient @GHC.TypeNats.Nat ranked,
                         UnletGradient @[GHC.TypeNats.Nat] shaped)
        bound by the instance declaration
        at src/HordeAd/Core/TensorADVal.hs:(346,10)-(349,55)
      Expected: DeltaS
                  shaped rm ((:) @GHC.Num.Natural.Natural ((0 + n) + (k - n)) shm)
        Actual: Dual
                  @[GHC.TypeNats.Nat] shaped rm ((:) @GHC.TypeNats.Nat k shm)
      ‘k’ is a rigid type variable bound by
        the type signature for:
          sscan :: forall rn rm (sh :: [GHC.TypeNats.Nat])
                          (shm :: [GHC.TypeNats.Nat]) (k :: GHC.TypeNats.Nat).
                   (GoodScalar rn, GoodScalar rm, OS.Shape sh, OS.Shape shm,
                    KnownNat k) =>
                   (forall (f :: TensorType [GHC.TypeNats.Nat]).
                    ADReadyS f =>
                    f rn sh -> f rm shm -> f rn sh)
                   -> ADVal @[GHC.TypeNats.Nat] shaped rn sh
                   -> ADVal
                        @[GHC.TypeNats.Nat] shaped rm ((:) @GHC.TypeNats.Nat k shm)
                   -> ADVal @[GHC.TypeNats.Nat] shaped rn ((:) @GHC.TypeNats.Nat k sh)
        at src/HordeAd/Core/TensorADVal.hs:(772,12)-(777,36)
    • In the fifth argument of ‘SliceS’, namely ‘as'’
      In the third argument of ‘h’, namely
        ‘(SliceS @_ @0 @k1 @(k - k1) as')’
      In the expression:
        h @k1 (sslice @_ @_ @_ @(k - k1) (Proxy @0) (Proxy @k1) as)
          (SliceS @_ @0 @k1 @(k - k1) as')
    • Relevant bindings include
        scanAsFold :: DeltaS shaped rn ((:) @GHC.TypeNats.Nat k sh)
          (bound at src/HordeAd/Core/TensorADVal.hs:801:9)
        pShared :: shaped rn ((:) @GHC.TypeNats.Nat k sh)
          (bound at src/HordeAd/Core/TensorADVal.hs:800:14)
        p :: shaped rn ((:) @GHC.TypeNats.Nat k sh)
          (bound at src/HordeAd/Core/TensorADVal.hs:799:9)
        as' :: Dual
                 @[GHC.TypeNats.Nat] shaped rm ((:) @GHC.TypeNats.Nat k shm)
          (bound at src/HordeAd/Core/TensorADVal.hs:778:34)
        as :: shaped rm ((:) @GHC.TypeNats.Nat k shm)
          (bound at src/HordeAd/Core/TensorADVal.hs:778:31)
        sscan :: (forall (f :: TensorType [GHC.TypeNats.Nat]).
                  ADReadyS f =>
                  f rn sh -> f rm shm -> f rn sh)
                 -> ADVal @[GHC.TypeNats.Nat] shaped rn sh
                 -> ADVal
                      @[GHC.TypeNats.Nat] shaped rm ((:) @GHC.TypeNats.Nat k shm)
                 -> ADVal @[GHC.TypeNats.Nat] shaped rn ((:) @GHC.TypeNats.Nat k sh)
          (bound at src/HordeAd/Core/TensorADVal.hs:778:3)
    |
812 |                     (SliceS @_ @0 @k1 @(k - k1) as')

[Mikolaj]

Please don't mind me. That's the effect of my unwittingly telling the plugin that k1 == k - k1 and then the compiler getting desperate. Closing.