Derive a <= Max x (Max a y)

[isovector]

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]

I believe that's hardcoded here:

ghc-typelits-extra/src/GHC/TypeLits/Extra/Solver.hs

Lines 210 to 211 in 055f5c8

	(p, Max x y)
	| b && (p == x || p == y) -> simples (((,) <$> evMagic ct <*> pure ct):evs) news eqs'

[christiaanb]

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