Try and outright solve substituted constraint

Partially Fixes [#65](#65)

CHANGELOG.md

@@ -1,5 +1,8 @@
 # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package
 
+## Unreleased
+* Try and outright solve substituted constraints, the same as is done with the unsubstituted constraint. Partially Fixes [#65](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/65).
+
 ## 0.7.7 *October 10th 2022*
 * Solve unflattened wanteds instead of the wanteds passed to the plugin. Fixes [#1901]https://github.com/clash-lang/clash-compiler/issues/1901.
 * Add support for GHC 9.4

src-ghc-9.4/GHC/TypeLits/Normalise.hs

@@ -514,6 +514,7 @@ simplifyNats opts@Opts {..} leqT eqsG eqsW = do
                  -- `1 <= x^y`
                  -- OR
                 (instantSolveIneq depth u:
+                instantSolveIneq depth uS:
                 -- This inequality is either a given constraint, or it is a wanted
                 -- constraint, which in normal form is equal to another given
                 -- constraint, hence it can be solved.

src-pre-ghc-9.4/GHC/TypeLits/Normalise.hs

@@ -659,6 +659,7 @@ simplifyNats opts@Opts {..} ordCond eqsG eqsW = do
                  -- `1 <= x^y`
                  -- OR
                 (instantSolveIneq depth u:
+                instantSolveIneq depth uS:
                 -- This inequality is either a given constraint, or it is a wanted
                 -- constraint, which in normal form is equal to another given
                 -- constraint, hence it can be solved.

tests/Tests.hs

@@ -498,6 +498,12 @@ tyFamMonotonicityFun _ = ()
 tyFamMonotonicity :: (2 <= F2 dom) => Proxy (dom :: Symbol) -> ()
 tyFamMonotonicity dom = tyFamMonotonicityFun dom
 
+oneLtPowSubst :: forall a b. (b ~ (2^a)) => Proxy a -> Proxy a
+oneLtPowSubst = go
+  where
+    go :: 1 <= b => Proxy a -> Proxy a
+    go = id 
+
 main :: IO ()
 main = defaultMain tests
 
@@ -598,6 +604,9 @@ tests = testGroup "ghc-typelits-natnormalise"
     , testCase "2 <= P (G2 dom) implies 1 <= P (G2 dom)" $
       show (tyFamMonotonicity (Proxy :: Proxy Dom)) @?=
       "()"
+    , testCase "b ~ (2^a) => 1 <= b" $
+      show (oneLtPowSubst (Proxy :: Proxy 0)) @?=
+      "Proxy"
     ]
   , testGroup "errors"
     [ testCase "x + 2 ~ 3 + x" $ testProxy1 `throws` testProxy1Errors