`Nat` (in)equality transitivity or congruence regression in GHC 9.8.1-alpha1: Cannot satisfy: OS.Rank sh2 <= 1 + OS.Rank sh1
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 haven't tried with HEAD of the github repo of GHC.TypeLits.Normalise
and GHC 9.6, but I don't think GHC.TypeLits.Normalise
has been modified vs the version on Hackage (GHC.TypeLits.KnownNat.Solver
has been, but it seem unrelated).
CC: @christiaanb