Soundness violation around subtraction

[mniip]

{- cabal:
build-depends: base, ghc-typelits-natnormalise
-}
{-# LANGUAGE AllowAmbiguousTypes, DataKinds, ExplicitForAll, TypeApplications, TypeFamilies, TypeOperators #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}

import Data.Type.Equality
import GHC.TypeNats

urk :: False :~: True
urk = case sub @0 of Refl -> ineq @(0 - 1)
  where
    ineq :: forall k. (1 <=? 1 + k) :~: True
    ineq = Refl

    sub :: forall n m. (m ~ (n - 1)) => 1 + (n - 1) :~: n
    sub = Refl -- bogus

Note that the additional (redundant!) m type variable is necessary, without it the constraint is correctly rejected.

[christiaanb]

So here's what's going on.

1. In https://github.com/clash-lang/ghc-typelits-natnormalise/blob/3289e1a25df3d7752d6734aa83ba04782d6e43cd/src/GHC/TypeLits/Normalise/Unify.hs#L153 we remember that: whenever we see a - b, we must emit a b <= a constraint when we solve a constraint.
2. Sometimes we find a "unifiers", such as the m ~ (n - 1), and them as substitution ([m := n - 1] when we follow the example), as we continue solving: https://github.com/clash-lang/ghc-typelits-natnormalise/blob/3289e1a25df3d7752d6734aa83ba04782d6e43cd/src-ghc-9.4/GHC/TypeLits/Normalise.hs#L491-L500
3. We apply these substitutions before we start solving equations: https://github.com/clash-lang/ghc-typelits-natnormalise/blob/3289e1a25df3d7752d6734aa83ba04782d6e43cd/src-ghc-9.4/GHC/TypeLits/Normalise.hs#L479-L481
4. When we actually solve an equation we create a proof (in the form of a "BelieveMe"), but also emit any b <= a constraints we collected in step 1. https://github.com/clash-lang/ghc-typelits-natnormalise/blob/3289e1a25df3d7752d6734aa83ba04782d6e43cd/src-ghc-9.4/GHC/TypeLits/Normalise.hs#L484-L485 It's the subToPred opts leqT k part.
5. The issue is that we do not carry over any b <= a constraints from step 2 to step 4. We only emit the b <= a constraints belonging to the constraint from before substitution we do in step 3.

So the solution is that whenever we create the substitution in step 2, we remember if we need to tag any b <= a constraints with them. And then in step 3, whenever a substitution carrying one of these constraints with them succeeds, we need to also emit those b <= a constraints in step 4.