WIP: Fix n <= 0 constraint being reported as impossible.

CHANGELOG.md

@@ -1,5 +1,8 @@
 # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package
 
+## Unreleased
+* Fix `n <= 0` constrained being reported as impossible.
+
 ## 0.7.10 *May 22nd 2024*
 * Support for GHC 9.10.1
 

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

src/GHC/TypeLits/Normalise/Unify.hs

@@ -656,6 +656,8 @@ isNatural (S [P []])       = return True
 isNatural (S [P (I i:ps)])
   | i >= 0    = isNatural (S [P ps])
   | 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])
 isNatural (S [P (E s p:ps)]) = do
   sN <- isNatural s

tests/Tests.hs

@@ -506,7 +506,10 @@ oneLtPowSubst :: forall a b. (b ~ (2^a)) => Proxy a -> Proxy a
 oneLtPowSubst = go
   where
     go :: 1 <= b => Proxy a -> Proxy a
-    go = id 
+    go = id
+
+givenLEZeroNotImpossible :: forall (a :: Nat) . a <= 0 => Proxy a -> Proxy 'True
+givenLEZeroNotImpossible p = Proxy @((a + a - a) <=? 0)
 
 main :: IO ()
 main = defaultMain tests
@@ -611,6 +614,8 @@ tests = testGroup "ghc-typelits-natnormalise"
     , testCase "b ~ (2^a) => 1 <= b" $
       show (oneLtPowSubst (Proxy :: Proxy 0)) @?=
       "Proxy"
+    , testCase "a <= 0 is not impossible" $
+      givenLEZeroNotImpossible (Proxy @0) @?= Proxy
     ]
   , testGroup "errors"
     [ testCase "x + 2 ~ 3 + x" $ testProxy1 `throws` testProxy1Errors