ghc-typelits-natnormalise and ghc-typelits-extra don't always work together nicely

[leonschoorl]

Not sure yet if the problem is with ghc-typelits-natnormalise or ghc-typelits-extra.

{-# LANGUAGE TypeOperators,DataKinds #-}
{-# OPTIONS_GHC -fplugin=GHC.TypeLits.Extra.Solver #-}
{-# OPTIONS_GHC -fplugin=GHC.TypeLits.Normalise #-}

import GHC.TypeLits.Extra
import GHC.TypeLits
import Data.Proxy
import Prelude

-- ok
g0 :: Proxy n
   -> Proxy (Max (1+n) 1)
   -> Proxy (1+n)
g0 _ = id

-- ok
g1 :: Proxy n
   -> Proxy (Max (n+1) 1)
   -> Proxy (n+1)
g1 _ = id

-- should typecheck, but doesn't
g2 :: Proxy n
   -> Proxy (Max (1+n) 1)
   -> Proxy (n+1)
g2 _ = id

-- should typecheck, but doesn't
g3 :: Proxy n
   -> Proxy (Max (n+1) 1)
   -> Proxy (1+n)
g3 _ = id

-- ok
g4 :: Proxy n
   -> Proxy (Max (n+1) 1)
   -> Proxy (Max (1+n) 1)
g4 _ = id

-- should typecheck, but doesn't
g5 :: Proxy n
   -> Proxy (Max (n+2) 1)
   -> Proxy (Max (2+n) 2)
g5 _ = id

In g0 and g1 we see that typelits-extra can eliminate Maxs. But it seems natnormalise doesn't run on the result of this eliminations in g2 and g3. g4 shows that natnormalise does seem to work underneath a Max node.

[leonschoorl]

Ultimately we'd like to have it solve:

(Max (((2 ^ n) + 1) + ((2 ^ n) + 1)) 1) 
  ~  (2 + ((2 ^ n) * 2))

h :: Proxy n
  -> Proxy (Max (((2 ^ n) + 1) + ((2 ^ n) + 1)) 1)
  -> Proxy (2 + ((2 ^ n) * 2))
h _ = id

Which we need for (the current implementation of) the SatIndex PR: https://github.com/clash-lang/clash-compiler/pull/688