`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 Mikolaj/horde-ad@e76ff6c

• 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:

Mikolaj/horde-ad@0417f41

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.

[christiaanb]

So on GHC 9.6.2 the plugin sees the following constraints:

  given   = [[G] Rank perm <= Rank sh2,
             [G] Rank sh1 ~ (1 + Rank perm)]
  wanted  = [[W] (1 + Rank perm) <= (1 + Rank sh2)]

but on GHC 9.8.2-alpha1 the plugin sees the following constraints:

  given   = [[G] Rank perm <= Rank sh2,
             [G] (1 + Rank perm) ~ Rank sh1]
  wanted  = [[W] Rank sh1 <= (1 + Rank sh2)]

The problem is that the plugin cannot currently substitute Rank sh1 for 1 + Rank perm, so it cannot solve [W] Rank sh1 <= (1 + Rank sh2).

[rowanG077]

Maybe we should take a new look at clash-lang/ghc-typelits-knownnat#43 or something like it since we no longer get the flat constraints.

[christiaanb]

Sadly, we need something more than tyvar substitutions. In the above case we need to substitute Rank sh1 for 1 + Rank perm.

[rowanG077]

Yes I think maybe we should introduce flattening tyvars locally.

[christiaanb]

But this has nothing to do with (un)flattening! Because none of the equalities have a tyvar on the LHS or RHS. We have a TyFam app on the LHS and a TyFam app on the RHS.

[rowanG077]

I'm saying that we should add tyvars(Our own version of flattening skolems) so we recover t ~ P x if necessary and then apply the transitive closure.