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

Derive `a <= Max x (Max a y)` #37

Open isovector opened 3 years ago

isovector commented 3 years ago

ghc-typelits-extra doesn't take advantage of the semilattice on max. But this is a strange state of affairs, since the following reduces correctly:

a <= Max a (Max x y)

martijnbastiaan commented 3 years ago

I believe that's hardcoded here:

https://github.com/clash-lang/ghc-typelits-extra/blob/055f5c88502d3fa23b4c1ca127d960a0a10f2b0c/src/GHC/TypeLits/Extra/Solver.hs#L210-L211

christiaanb commented 3 years ago

No, that indeed observes: x <= Max x y and y <= Max x y.