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.