Fix n <= 0 constrained 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/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 True (uncurry (&&) . second Set.null) (runWriterT (isNatural s1'))
-    , maybe True (uncurry (&&) . second Set.null) (runWriterT (isNatural s2'))
+    , maybe False (uncurry (&&) . second Set.null) (runWriterT (isNatural s1'))
+    , maybe False (uncurry (&&) . second Set.null) (runWriterT (isNatural s2'))
     -> unifiers' ct s1' s2'
   _ | null psx
     , length ps1 == length ps2
@@ -655,7 +655,9 @@ isNatural (S [])           = return True
 isNatural (S [P []])       = return True
 isNatural (S [P (I i:ps)])
   | i >= 0    = isNatural (S [P ps])
-  | otherwise = return False
+  | otherwise = WriterT Nothing
+  -- 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,13 @@ 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) . Proxy a -> a <= 0 => ()
+givenLEZeroNotImpossible _ = go (Proxy @(a + a - a))
+  where
+    go :: Proxy b -> b <= 0 => ()
+    go _ = ()
 
 main :: IO ()
 main = defaultMain tests
@@ -611,6 +617,8 @@ tests = testGroup "ghc-typelits-natnormalise"
     , testCase "b ~ (2^a) => 1 <= b" $
       show (oneLtPowSubst (Proxy :: Proxy 0)) @?=
       "Proxy"
+    , testCase "given a <= 0 is not impossible" $
+      givenLEZeroNotImpossible (Proxy @0) @?= ()
     ]
   , testGroup "errors"
     [ testCase "x + 2 ~ 3 + x" $ testProxy1 `throws` testProxy1Errors