You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
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.
While #34 appears to be fixed, another issue around inequalities and subtraction occurs.
The following invalid inference rule is accepted:
As demonstrated below, this is unsound:
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 ifx
itself can't reduce, resulting in assertions like0 <= 2 - 5
which should never be turned into5 <= 2
.The text was updated successfully, but these errors were encountered: