search

clash-lang / ghc-typelits-natnormalise

Normalise GHC.TypeLits.Nat equations
Other
43 stars 15 forks source link

Any natural multiplied with a negative number doesn't have to be a non-natural #48

Closed rowanG077 closed 2 years ago

rowanG077 commented 4 years ago

Should fix https://github.com/clash-lang/clash-compiler/issues/1518

christiaanb commented 4 years ago

Can you give an example of a natural number, besides zero, when multiplied with a negative integer does not result in a negative integer?

rowanG077 commented 4 years ago

No. But zero could possibly be in the set that can contain any natural number.

christiaanb commented 4 years ago

So shouldn't you check that then? instead of returning WriterT Nothing ? Like, if we know it's zero, we return True. If we know it's positive we return False. And if we don't know whether it's positive or zero, we return WriterT Nothing.

rowanG077 commented 4 years ago

Isn't it already guarantied that the SOP contains only irreducable type classes at the point when isNatural is called?

christiaanb commented 4 years ago

Ah yes, you're right. Could you add that as a comment?

christiaanb commented 4 years ago

And perhaps a regression test? :)

rowanG077 commented 4 years ago

Yes will add a test later tonight or tommorow.

The change in isNatural had some fallout that it could result in a unifier that is not a natural number. So I added a simple check to ensure this doesn't happen.

rowanG077 commented 4 years ago

Actually it won't work like this because the ghc-typelits-extra plugin relies on -1 * n to not be a natural number :(.

in the mergeMax and mergeMin functions ghc-typelits-extra tries to subtract the LHS from the RHS and check if the result is a natural to decide whether it can reduce the Max or Min. But with this change that fails. For example:

Max (1+n) 1 -> 1 - 1 * (1 + n) -> 1 - 1 - 1 * n -> - 1 * n

Which is now not considered to be confirmed to be a non-natural number. So Max/Min does not get reduced. So to keep the current behaviour we would need to try the subtraction both ways around and see if either can be reduced....