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

@@ -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
 

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@:

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})

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