Hack attempt #2

Author: rowanG077

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

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

tests/Tests.hs

@@ -509,8 +509,12 @@ oneLtPowSubst = go
     go = id
 
 givenLEZeroNotImpossible :: forall (a :: Nat) . Proxy a -> a <= 0 => ()
-givenLEZeroNotImpossible _ = go (Proxy @(a + a - a))
+givenLEZeroNotImpossible p = go (go2 p)
   where
+    -- Ensure the plugin is called
+    go2 :: Proxy (b + 0) -> Proxy b
+    go2 p = p
+
     go :: Proxy b -> b <= 0 => ()
     go _ = ()