diff --git a/CHANGELOG.md b/CHANGELOG.md index 3c44908..57eaa74 100644 --- a/CHANGELOG.md +++ b/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 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 29fb186..a212f85 100644 --- a/src/GHC/TypeLits/Normalise/Unify.hs +++ b/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 diff --git a/tests/Tests.hs b/tests/Tests.hs index 3d5b02a..e9fa9be 100644 --- a/tests/Tests.hs +++ b/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