From 3bc9f4dd1c742a4509f264d0a496ee9dbdaef7a9 Mon Sep 17 00:00:00 2001
From: Rowan Goemans <goemansrowan@gmail.com>
Date: Tue, 11 Jun 2024 20:24:27 +0200
Subject: [PATCH] Hack attempt #2

---
 src-ghc-9.4/GHC/TypeLits/Normalise.hs     | 7 ++++---
 src-pre-ghc-9.4/GHC/TypeLits/Normalise.hs | 7 ++++---
 src/GHC/TypeLits/Normalise/Unify.hs       | 6 +++---
 tests/Tests.hs                            | 9 +++------
 4 files changed, 14 insertions(+), 15 deletions(-)

diff --git a/src-ghc-9.4/GHC/TypeLits/Normalise.hs b/src-ghc-9.4/GHC/TypeLits/Normalise.hs
index 5f1bbe2..fed6d56 100644
--- a/src-ghc-9.4/GHC/TypeLits/Normalise.hs
+++ b/src-ghc-9.4/GHC/TypeLits/Normalise.hs
@@ -507,8 +507,9 @@ simplifyNats opts@Opts {..} leqT eqsG eqsW = do
           x'    = substsSOP subst x
           y'    = substsSOP subst y
           uS    = (x',y',b)
-          leqsG' | isGiven (ctEvidence ct) = (x',y',b):leqsG
-                 | otherwise               = leqsG
+          isG   = isGiven (ctEvidence ct)
+          leqsG' | isG       = (x',y',b):leqsG
+                 | otherwise = leqsG
           ineqs = concat [ leqsG
                          , map (substLeq subst) leqsG
                          , map snd (rights (map fst eqsG))
@@ -519,7 +520,7 @@ simplifyNats opts@Opts {..} leqT eqsG eqsW = do
           evs' <- maybe evs (:evs) <$> evMagic ct knW (subToPred opts leqT k)
           simples subst evs' leqsG' xs eqs'
 
-        Just (False,_) | null k -> return (Impossible (fst eq))
+        Just (False,_) | null k && not isG -> return (Impossible (fst eq))
         _ -> do
           let solvedIneq = mapMaybe runWriterT
                  -- it is an inequality that can be instantly solved, such as
diff --git a/src-pre-ghc-9.4/GHC/TypeLits/Normalise.hs b/src-pre-ghc-9.4/GHC/TypeLits/Normalise.hs
index e7300f1..12066ea 100644
--- a/src-pre-ghc-9.4/GHC/TypeLits/Normalise.hs
+++ b/src-pre-ghc-9.4/GHC/TypeLits/Normalise.hs
@@ -640,8 +640,9 @@ simplifyNats opts@Opts {..} ordCond eqsG eqsW = do
           x'    = substsSOP subst x
           y'    = substsSOP subst y
           uS    = (x',y',b)
-          leqsG' | isGiven (ctEvidence ct) = (x',y',b):leqsG
-                 | otherwise               = leqsG
+          isG   = isGiven (ctEvidence ct)
+          leqsG' | isG       = (x',y',b):leqsG
+                 | otherwise = leqsG
           ineqs = concat [ leqsG
                          , map (substLeq subst) leqsG
                          , map snd (rights (map fst eqsG))
@@ -652,7 +653,7 @@ simplifyNats opts@Opts {..} ordCond eqsG eqsW = do
           evs' <- maybe evs (:evs) <$> evMagic ct knW (subToPred opts ordCond k)
           simples subst evs' leqsG' xs eqs'
 
-        Just (False,_) | null k -> return (Impossible (fst eq))
+        Just (False,_) | null k && not isG -> return (Impossible (fst eq))
         _ -> do
           let solvedIneq = mapMaybe runWriterT
                  -- it is an inequality that can be instantly solved, such as
diff --git a/src/GHC/TypeLits/Normalise/Unify.hs b/src/GHC/TypeLits/Normalise/Unify.hs
index 94e3035..a212f85 100644
--- a/src/GHC/TypeLits/Normalise/Unify.hs
+++ b/src/GHC/TypeLits/Normalise/Unify.hs
@@ -568,8 +568,8 @@ unifiers' ct (S ((P [I i]):ps1)) (S ((P [I j]):ps2))
 unifiers' ct s1@(S ps1) s2@(S ps2) = case sopToIneq k1 of
   Just (s1',s2',_)
     | s1' /= s1 || s2' /= s1
-    , maybe False (uncurry (&&) . second Set.null) (runWriterT (isNatural s1'))
-    , maybe False (uncurry (&&) . second Set.null) (runWriterT (isNatural s2'))
+    , maybe True (uncurry (&&) . second Set.null) (runWriterT (isNatural s1'))
+    , maybe True (uncurry (&&) . second Set.null) (runWriterT (isNatural s2'))
     -> unifiers' ct s1' s2'
   _ | null psx
     , length ps1 == length ps2
@@ -655,7 +655,7 @@ isNatural (S [])           = return True
 isNatural (S [P []])       = return True
 isNatural (S [P (I i:ps)])
   | i >= 0    = isNatural (S [P ps])
-  | otherwise = WriterT Nothing
+  | otherwise = return False
   -- If i is not a natural number then their sum *might* be natural,
   -- but we simply can't be sure since ps might be zero
 isNatural (S [P (V _:ps)]) = isNatural (S [P ps])
diff --git a/tests/Tests.hs b/tests/Tests.hs
index a17045c..c2bbcc4 100644
--- a/tests/Tests.hs
+++ b/tests/Tests.hs
@@ -508,11 +508,8 @@ oneLtPowSubst = go
     go :: 1 <= b => Proxy a -> Proxy a
     go = id
 
-givenLEZeroNotImpossible :: forall (a :: Nat) . Proxy a -> a <= 0 => ()
-givenLEZeroNotImpossible _ = go (Proxy @(a + a - a))
-  where
-    go :: Proxy b -> b <= 0 => ()
-    go _ = ()
+givenLEZeroNotImpossible :: forall (a :: Nat) . Proxy (a <= 0) -> Proxy 'True
+givenLEZeroNotImpossible p = id (Proxy @(a + 0 <=? 0))
 
 main :: IO ()
 main = defaultMain tests
@@ -618,7 +615,7 @@ tests = testGroup "ghc-typelits-natnormalise"
       show (oneLtPowSubst (Proxy :: Proxy 0)) @?=
       "Proxy"
     , testCase "given a <= 0 is not impossible" $
-      givenLEZeroNotImpossible (Proxy @0) @?= ()
+      givenLEZeroNotImpossible (Proxy @(0 <=? 0)) @?= Proxy
     ]
   , testGroup "errors"
     [ testCase "x + 2 ~ 3 + x" $ testProxy1 `throws` testProxy1Errors