Try and outright solve substituted constraint

Partially Fixes [#65]#65.

CHANGELOG.md

@@ -2,6 +2,7 @@
 
 ## Unreleased
 * Solve unflattened wanteds instead of the wanteds passed to the plugin. Fixes [#1901]https://github.com/clash-lang/clash-compiler/issues/1901.
+* Try and outright solve substituted constraint, the same as is done with the unsubstituted constraint. Partially Fixes [#65]https://github.com/clash-lang/ghc-typelits-natnormalise/issues/65.
 
 ## 0.7.6 *June 20th 2021*
 * Do not vacuously solve `forall a b . 1 <=? a^b ~ True`

src/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