From 337386838985cea24fd802a1b99a08039a6d2aaa Mon Sep 17 00:00:00 2001
From: rowanG077 <goemansrowan@gmail.com>
Date: Thu, 18 Aug 2022 18:51:31 +0200
Subject: [PATCH] Try and outright solve substituted constraint
Partially Fixes [#65](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/65)
---
CHANGELOG.md | 3 ++-
src/GHC/TypeLits/Normalise.hs | 1 +
tests/Tests.hs | 9 +++++++++
3 files changed, 12 insertions(+), 1 deletion(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 0b9fa92..960a693 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,7 +1,8 @@
# Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package
## Unreleased
-* Solve unflattened wanteds instead of the wanteds passed to the plugin. Fixes [#1901]https://github.com/clash-lang/clash-compiler/issues/1901.
+* 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`
diff --git a/src/GHC/TypeLits/Normalise.hs b/src/GHC/TypeLits/Normalise.hs
index 0542191..e7300f1 100644
--- a/src/GHC/TypeLits/Normalise.hs
+++ b/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.
diff --git a/tests/Tests.hs b/tests/Tests.hs
index b2b4340..819f3ca 100644
--- a/tests/Tests.hs
+++ b/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