ghc-typelits-natnormalise

ghc-typelits-natnormalise copied to clipboard

Soundness issue with inequalities and subtraction.

1

While #34 appears to be fixed, another issue around inequalities and subtraction occurs. The following invalid inference rule is accepted: ```haskell invalid :: forall x y n. (x - n...

soundlogic2236

This happens with: ```haskell type family F (a :: Nat) (b :: Nat) :: Nat proxyEq5 :: forall a b . KnownNat (F (a * 3) b * 3) =>...

christiaanb

solve more inequalities involving exponentiation

1

strake