Soundness issue with inequalities and subtraction.

[soundlogic2236]

While #34 appears to be fixed, another issue around inequalities and subtraction occurs. The following invalid inference rule is accepted:

invalid :: forall x y n. (x - n <=? y - n) :~: 'True -> (x <=? y) :~: 'True
invalid Refl = Refl

As demonstrated below, this is unsound:

absurdity :: 'True :~: 'False
absurdity = makeProof @5 @0 (allLe @5 @0) Refl where
    makeProof :: forall x y. (x <=? y) :~: 'True -> (x <=? y) :~: 'False -> 'True :~: 'False
    makeProof = worker where
        worker :: forall a' b'. (x <=? y) :~: a' -> (x <=? y) :~: b' -> a' :~: b'
        worker Refl Refl = Refl
    allLe :: forall x y. (x <=? y) :~: 'True
    allLe = worker where
        worker :: (x <=? y) :~: 'True
        worker = invalid @x @y @x worker'
        worker' :: (x - x <=? y - x) :~: 'True
        worker' = worker'' @(x - x) @(y - x) Refl
        worker'' :: forall n m. n :~: 0 -> (n <=? m) :~: 'True
        worker'' Refl = Refl

The fundamental problem is that the subtraction may reduce the left hand side to zero, and the rule forall x. 0 <= x then triggers even if x itself can't reduce, resulting in assertions like 0 <= 2 - 5 which should never be turned into 5 <= 2.

[christiaanb]

Ugh, I “hate” that subtraction was ever added to GHC.TypeLits… Thanks for the report though! I’ll have a think whether the plugin should either require n <= x and n <= y or some other preconditions to make the inference valid.