Feature request: product inequality

[gergoerdi]

For some constants a and b, and type variables x and y, would it be possible to solve a * b <= x * y from (a <= x, b <= y)?

[christiaanb]

Could you check if the thing you want to do works with:

• https://github.com/clash-lang/ghc-typelits-sopsat
• Which needs: https://github.com/clash-lang/sop-satisfier

My plan is to make the above package subsume ghc-typelits-natnormalise as it has a much better approach for solving inequalities.

[gergoerdi]

Using ghc-typelits-sopsat at 87e632bf0d I got my intended use case to work!

foo :: forall n m. (1 <= n * m * m * n) => SNat n -> SNat m -> ()
foo _ _ = ()

bar :: forall n m. (1 <= n, 1 <= m) => SNat n -> SNat m -> ()
bar = foo