search

clash-lang / ghc-typelits-extra

Extra type-level operations on GHC.TypeLits.Nat and a custom solver
Other
16 stars 9 forks source link

`*Log b (b^n)` is wrongly reduced to `n` if `b` is not a literal #44

Open rowanG077 opened 2 years ago

rowanG077 commented 2 years ago

While working on https://github.com/clash-lang/ghc-typelits-extra/pull/43 I noticed this bug. It is not allowed to reduce because if b <= 1 then the logarithm will never reduce. This check is already applied if b is a literal but not in the general case.

Easy fix is just adding that check. Which sucks because now existing code will break. Better would be to start emitting new constraints, similar to how ghc-typelits-natnormalise does it. This will still break existing code. But at least the only thing that would need to happen is add the appropriate constraints.

christiaanb commented 2 years ago

I’m okay with breaking code, since the check is obviously needed in order to be correct.

I agree that we should go the route of emitting new constraints in this case.