`Nat` (in)equality transitivity or congruence regression in GHC 9.8.1-alpha1: Cannot satisfy: OS.Rank sh2 <= 1 + OS.Rank sh1

[Mikolaj]

This ticket is moved here from https://gitlab.haskell.org/ghc/ghc/-/issues/23763.

Repro with GHC 9.8.1-alpha1 and head.hackage (http://ghc.gitlab.haskell.org/head.hackage/):

• clone https://github.com/Mikolaj/horde-ad/commit/e76ff6c2f2b1fc53a00c6b78f74cb1ab8b94790d

• cabal build

• you get

src/HordeAd/Core/AstSimplify.hs:1192:9: error: [GHC-64725]
    • Cannot satisfy: OS.Rank sh2 <= 1 + OS.Rank sh1
    • In the first argument of ‘($)’, namely ‘astTransposeS @zsuccPerm’
      In the second argument of ‘($)’, namely
        ‘astTransposeS @zsuccPerm $ astReplicateS @n v’
      In the second argument of ‘($)’, namely
        ‘trustMeThisIsAPermutation @zsuccPerm
           $ astTransposeS @zsuccPerm $ astReplicateS @n v’
     |
1192 |       $ astTransposeS @zsuccPerm $ astReplicateS @n v

It works fine with GHC <= 9.6 and also after patching it in the following way:

https://github.com/Mikolaj/horde-ad/commit/0417f413051f1739fe32cfaf7869755276171449

My guess is that previously GHC could deduce:

OS.Rank zsuccPerm <= 1 + OS.Rank sh1

from (note that sh2 that GHC invents here in just zsuccPerm -- this obfuscation in error messages is already reported in one of my older tickets)

OS.Rank zsuccPerm :~: 1 + OS.Rank perm

and

OS.Rank perm <= OS.Rank sh1

but now it can't.

The issue may be in GHC itself or in how plugin GHC.TypeLits.Normalise has been updated to 9.8.1-alpha1, but I doubt the latter, because it's been updated on head.hackage by people that know what they are doing.

I have now tried with HEADs of the github repos of GHC.TypeLits.Normalise and the other plugins and with GHC 9.8.1-alpha1 and the results are the same as with the versions of the plugins from head.hackage.