From 1eed8d3de637a115dad12e2cb722cb0a3bc761ea Mon Sep 17 00:00:00 2001
From: Christiaan Baaij <christiaan.baaij@gmail.com>
Date: Wed, 3 Apr 2024 16:00:16 +0200
Subject: [PATCH] Parse `Assert`-based constraints in GHC 9.4+ (#51)

So we can create new wanted constraints from them. Before, we
would only recognise `~`-based constraints. We need to parse
`Assert`-based constraints because it is used to implement `<=`.

Also, we no longer silently fails when it's unexpected constraint.
---
 CHANGELOG.md                             |  3 +++
 ghc-typelits-extra.cabal                 |  2 +-
 src-ghc-9.4/GHC/TypeLits/Extra/Solver.hs |  5 +++--
 tests/Main.hs                            | 11 +++++++++++
 4 files changed, 18 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index c87495b..ad33ad8 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,8 @@
 # Changelog for the [`ghc-typelits-extra`](http://hackage.haskell.org/package/ghc-typelits-extra) package
 
+# 0.4.7
+* Fix Plugin silently fails when normalizing <= in GHC 9.4+ [#50](https://github.com/clash-lang/ghc-typelits-extra/issues/50)
+
 # 0.4.6 *October 10th 2023*
 * Support for GHC-9.8.1
 
diff --git a/ghc-typelits-extra.cabal b/ghc-typelits-extra.cabal
index 77851bd..1c4147d 100644
--- a/ghc-typelits-extra.cabal
+++ b/ghc-typelits-extra.cabal
@@ -1,5 +1,5 @@
 name:                ghc-typelits-extra
-version:             0.4.6
+version:             0.4.7
 synopsis:            Additional type-level operations on GHC.TypeLits.Nat
 description:
   Additional type-level operations on @GHC.TypeLits.Nat@:
diff --git a/src-ghc-9.4/GHC/TypeLits/Extra/Solver.hs b/src-ghc-9.4/GHC/TypeLits/Extra/Solver.hs
index 809d3e2..80340a9 100644
--- a/src-ghc-9.4/GHC/TypeLits/Extra/Solver.hs
+++ b/src-ghc-9.4/GHC/TypeLits/Extra/Solver.hs
@@ -29,7 +29,7 @@ import GHC.TcPluginM.Extra
   (evByFiat, lookupModule, lookupName, tracePlugin, newWanted)
 
 -- GHC API
-import GHC.Builtin.Names (eqPrimTyConKey, hasKey)
+import GHC.Builtin.Names (eqPrimTyConKey, hasKey, getUnique)
 import GHC.Builtin.Types (promotedTrueDataCon, promotedFalseDataCon)
 import GHC.Builtin.Types (boolTy, naturalTy, cTupleDataCon, cTupleTyCon)
 import GHC.Builtin.Types.Literals (typeNatTyCons)
@@ -289,7 +289,8 @@ createWantedFromNormalised defs sct = do
   let (ct, t1, t2) = extractCtSides sct
   newPredTy <- case splitTyConApp_maybe $ ctEvPred $ ctEvidence ct of
     Just (tc, [a, b, _, _]) | tc `hasKey` eqPrimTyConKey -> pure (mkTyConApp tc [a, b, t1, t2])
-    _ -> fail "Nothing"
+    Just (tc, [_, b]) | tc `hasKey` getUnique (assertTC defs) -> pure (mkTyConApp tc [t1,b])
+    _ -> error "Impossible: neither (<=?) nor Assert"
   ev <- newWanted (ctLoc ct) newPredTy
   let ctN = case ct of
               CQuantCan qc -> CQuantCan (qc { qci_ev = ev})
diff --git a/tests/Main.hs b/tests/Main.hs
index 4fa8382..d260275 100644
--- a/tests/Main.hs
+++ b/tests/Main.hs
@@ -223,6 +223,17 @@ test57
   -> Proxy True
 test57 _ _ = id
 
+test58a
+  :: 1 <= n
+  => Proxy n
+  -> Proxy n
+test58a = id
+
+test58b
+  :: Proxy (Max (n+2) 1)
+  -> Proxy (Max (n+2) 1)
+test58b = test58a
+
 main :: IO ()
 main = defaultMain tests