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

   ghc-typelits-natnormalise/src/GHC/TypeLits/Normalise/Unify.hs

   Line 153 in 3289e1a

   tell [(x,y)]

   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:

   ghc-typelits-natnormalise/src-ghc-9.4/GHC/TypeLits/Normalise.hs

   Lines 491 to 500 in 3289e1a

   	Draw subst' -> do
   	evM <- evMagic ct empty (map unifyItemToPredType subst' ++
   	subToPred opts leqT k)
   	let leqsG' | isGiven (ctEvidence ct) = eqToLeq u' v' ++ leqsG
   	| otherwise = leqsG
   	case evM of
   	Nothing -> simples subst evs leqsG' xs eqs'
   	Just ev ->
   	simples (substsSubst subst' subst ++ subst')
   	(ev:evs) leqsG' [] (xs ++ eqs')

3. We apply these substitutions before we start solving equations:

   ghc-typelits-natnormalise/src-ghc-9.4/GHC/TypeLits/Normalise.hs

   Lines 479 to 481 in 3289e1a

   	let u' = substsSOP subst u
   	v' = substsSOP subst v
   	ur <- unifyNats ct u' v'

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.

   ghc-typelits-natnormalise/src-ghc-9.4/GHC/TypeLits/Normalise.hs

   Lines 484 to 485 in 3289e1a

   	Win -> do
   	evs' <- maybe evs (:evs) <$> evMagic ct empty (subToPred opts leqT k)

   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.