Soundness issue around comparisons

[soundlogic2236]

An invalid inference rule is made when handling comparisons and subtraction. I believe similar issues also occur around strict less than, but less than or equal proved the easiest to minimize:

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.

[konn]

Thank you for reporting. That seems really a severe issue. I'm a bit busy these days, but I will investigate the issue as soon as possible.