diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,11 @@ # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package +## Unreleased + +## 0.9.7 *September 19th 2026* +* Support for GHC 10.0 and 10.2 +* Fixes [#131](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/131) Compile-time loop when normalising exponentiation with a type family application as the base. + ## 0.9.6 *May 13th 2026* * Bump ghc-tcplugin-api to prepare for inclusion into stackage diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -2,7 +2,6 @@ [![Build Status](https://github.com/clash-lang/ghc-typelits-natnormalise/actions/workflows/haskell-ci.yml/badge.svg?branch=master)](https://github.com/clash-lang/ghc-typelits-natnormalise/actions) [![Hackage](https://img.shields.io/hackage/v/ghc-typelits-natnormalise.svg)](https://hackage.haskell.org/package/ghc-typelits-natnormalise) -[![Hackage Dependencies](https://img.shields.io/hackage-deps/v/ghc-typelits-natnormalise.svg?style=flat)](http://packdeps.haskellers.com/feed?needle=exact%3Aghc-typelits-natnormalise) A type checker plugin for GHC that can solve _equalities_ and _inequalities_ of types of kind `Nat`, where these types are either: diff --git a/ghc-typelits-natnormalise.cabal b/ghc-typelits-natnormalise.cabal --- a/ghc-typelits-natnormalise.cabal +++ b/ghc-typelits-natnormalise.cabal @@ -1,6 +1,6 @@ cabal-version: 3.0 name: ghc-typelits-natnormalise -version: 0.9.6 +version: 0.9.7 synopsis: GHC typechecker plugin for types of kind GHC.TypeLits.Nat description: A type checker plugin for GHC that can solve /equalities/ and /inequalities/ @@ -48,6 +48,7 @@ build-type: Simple extra-doc-files: README.md CHANGELOG.md +extra-source-files: tests/WithTimeout/Test131.hs tested-with: GHC == 8.8.4, GHC == 8.10.7, GHC == 9.0.2, GHC == 9.2.8, GHC == 9.4.8, GHC == 9.6.7, GHC == 9.8.4, GHC == 9.10.2, GHC == 9.12.2 @@ -69,8 +70,8 @@ GHC.TypeLits.Normalise.Unify build-depends: base >=4.9 && <5, containers >=0.5.7.1 && <0.9, - ghc >=8.8.1 && <9.15, - ghc-tcplugin-api >=0.19 && <0.20, + ghc >=8.8.1 && <10.3, + ghc-tcplugin-api >=0.20.1 && <0.21, transformers >=0.5.2 && < 0.7 if impl(ghc >= 9.0.0) build-depends: ghc-bignum >=1.0 && <1.5 @@ -79,9 +80,7 @@ mixins: ghc - ( TcTypeNats as GHC.Builtin.Types.Literals - , TyCon as GHC.Core.TyCon - , TysWiredIn as GHC.Builtin.Types + ( TyCon as GHC.Core.TyCon , Unique as GHC.Types.Unique , Util as GHC.Utils.Misc ) @@ -106,6 +105,11 @@ ghc-typelits-natnormalise, interpolate, process, + -- Not used by the test suite itself, but needed in the + -- build plan so the GHC spawned for + -- tests/WithTimeout/Test131.hs can find it through the + -- GHC environment file. + singletons, tasty >= 0.10, tasty-hunit >= 0.9, temporary diff --git a/src/GHC/TypeLits/Normalise.hs b/src/GHC/TypeLits/Normalise.hs --- a/src/GHC/TypeLits/Normalise.hs +++ b/src/GHC/TypeLits/Normalise.hs @@ -192,16 +192,14 @@ ( empty, insertWith, traverseWithKey ) -- ghc -import GHC.Builtin.Names - ( knownNatClassName ) -import GHC.Builtin.Types.Literals - ( typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon ) import GHC.Core.TyCon ( Injectivity (..), tyConInjectivityInfo, tyConArity ) import GHC.Utils.Misc ( filterByList ) -- ghc-tcplugin-api +import GHC.Builtins + ( typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon ) import GHC.TcPlugin.API import GHC.TcPlugin.API.TyConSubst ( TyConSubst, mkTyConSubst ) @@ -368,7 +366,7 @@ (redGivens, negWanteds) <- reduceGivens True opts tcs givens reducible_wanteds <- catMaybes <$> mapM (\ct -> fmap (ct,) <$> - reduceNatConstr redGivens ct) + reduceNatConstr tcs redGivens ct) nonEqs tcPluginTrace "decideEqualSOP Wanteds {" $ @@ -471,8 +469,8 @@ fromNatEquality (Left (ct, _, _)) = ct fromNatEquality (Right (ct, _)) = ct -reduceNatConstr :: [Ct] -> Ct -> TcPluginM Solve (Maybe (EvTerm, [(Type, Type)], [Ct])) -reduceNatConstr givens ct = do +reduceNatConstr :: LookedUpTyCons -> [Ct] -> Ct -> TcPluginM Solve (Maybe (EvTerm, [(Type, Type)], [Ct])) +reduceNatConstr tcs givens ct = do let pred0 = ctEvPred $ ctEvidence ct (mans, tests) = runWriter $ normaliseNatEverywhere pred0 @@ -483,7 +481,7 @@ -- No existing evidence found Nothing | ClassPred cls _ <- classifyPredType pred' - , className cls /= knownNatClassName + , cls /= knownNatClass tcs -- We actually did do some rewriting/normalisation. , Just {} <- mans @@ -829,7 +827,7 @@ -- From [G] KnownNat blah, also produce [G] 0 <= blah -- See https://github.com/clash-lang/ghc-typelits-natnormalise/issues/94. | isGiven (ctEvidence ct0) - , className kn == knownNatClassName + , kn == knownNatClass tcs , let ((x', cos0), ks) = runWriter (normaliseNat x) , let preds = subToPred opts tcs ks -> [NatCt (Right (ct0, (S [], x', True))) preds cos0] @@ -942,7 +940,7 @@ TcPluginM Solve (Maybe ((EvTerm, Ct), [Ct])) evMagic tcs ct deps knW preds = do holeWanteds <- evSubtPreds (ctLoc ct) preds - knWanted <- mapM (mkKnWanted (ctLoc ct)) (Set.elems knW) + knWanted <- mapM (mkKnWanted tcs (ctLoc ct)) (Set.elems knW) let newWant = knWanted ++ holeWanteds case classifyPredType $ ctEvPred $ ctEvidence ct of EqPred NomEq t1 t2 -> @@ -956,11 +954,11 @@ _ -> return Nothing mkKnWanted - :: CtLoc + :: LookedUpTyCons + -> CtLoc -> CType -> TcPluginM Solve Ct -mkKnWanted loc (CType ty) = do - kc_clas <- tcLookupClass knownNatClassName - let kn_pred = mkClassPred kc_clas [ty] +mkKnWanted tcs loc (CType ty) = do + let kn_pred = mkClassPred (knownNatClass tcs) [ty] wantedCtEv <- newWanted loc kn_pred return $ mkNonCanonical wantedCtEv diff --git a/src/GHC/TypeLits/Normalise/Compat.hs b/src/GHC/TypeLits/Normalise/Compat.hs --- a/src/GHC/TypeLits/Normalise/Compat.hs +++ b/src/GHC/TypeLits/Normalise/Compat.hs @@ -35,7 +35,7 @@ import Data.Foldable ( asum ) import GHC.TypeNats - ( CmpNat ) + ( CmpNat, KnownNat ) #if MIN_VERSION_ghc(9,3,0) import qualified GHC.TypeError ( Assert ) @@ -50,18 +50,6 @@ #endif -- ghc -import GHC.Builtin.Types - ( isCTupleTyConName - , promotedFalseDataCon, promotedTrueDataCon - , promotedLTDataCon, promotedEQDataCon, promotedGTDataCon - ) -#if MIN_VERSION_ghc(9,1,0) -import GHC.Builtin.Types - ( cTupleTyCon, cTupleDataCon ) -#else -import GHC.Builtin.Types - ( cTupleTyConName ) -#endif #if MIN_VERSION_ghc(9,7,0) import GHC.Types.Unique.Map ( UniqMap, intersectUniqMap_C, listToUniqMap, nonDetUniqMapToList ) @@ -73,6 +61,16 @@ #endif -- ghc-tcplugin-api +import GHC.Builtins + ( isCTupleTyConName + , promotedFalseDataCon, promotedTrueDataCon + , promotedLTDataCon, promotedEQDataCon, promotedGTDataCon +#if MIN_VERSION_ghc(9,1,0) + , cTupleTyCon, cTupleDataCon +#else + , cTupleTyConName +#endif + ) import GHC.TcPlugin.API import GHC.TcPlugin.API.TyConSubst ( TyConSubst, splitTyConApp_upTo ) @@ -97,12 +95,15 @@ #endif cmpNatTyCon :: TyCon, c0TyCon :: TyCon, - c0DataCon :: DataCon + c0DataCon :: DataCon, + -- | @KnownNat :: Nat -> Constraint@ + knownNatClass :: Class } lookupTyCons :: TcPluginM Init LookedUpTyCons lookupTyCons = do cmpNatT <- lookupTHName ''GHC.TypeNats.CmpNat >>= tcLookupTyCon + knownNatC <- lookupTHName ''GHC.TypeNats.KnownNat >>= tcLookupClass #if MIN_VERSION_ghc(9,3,0) assertT <- lookupTHName ''GHC.TypeError.Assert >>= tcLookupTyCon #endif @@ -119,6 +120,7 @@ , cmpNatTyCon = cmpNatT , c0TyCon = cTupleTyCon 0 , c0DataCon = cTupleDataCon 0 + , knownNatClass = knownNatC } #else leqT <- lookupTHName ''(GHC.TypeNats.<=) >>= tcLookupTyCon @@ -134,6 +136,7 @@ , c0TyCon = c0T , c0DataCon = c0D , cmpNatTyCon = cmpNatT + , knownNatClass = knownNatC } #endif diff --git a/src/GHC/TypeLits/Normalise/SOP.hs b/src/GHC/TypeLits/Normalise/SOP.hs --- a/src/GHC/TypeLits/Normalise/SOP.hs +++ b/src/GHC/TypeLits/Normalise/SOP.hs @@ -280,6 +280,7 @@ -- x^(2xy) ==> x^(2xy) normaliseExp b@(S [P [V _]]) (S [e]) = S [P [E b e]] +normaliseExp b@(S [P [C _]]) (S [e]) = S [P [E b e]] -- 2^(y^2) ==> 4^y normaliseExp b@(S [P [_]]) (S [e@(P [_])]) = S [P [reduceExp (E b e)]] diff --git a/src/GHC/TypeLits/Normalise/Unify.hs b/src/GHC/TypeLits/Normalise/Unify.hs --- a/src/GHC/TypeLits/Normalise/Unify.hs +++ b/src/GHC/TypeLits/Normalise/Unify.hs @@ -69,9 +69,6 @@ import qualified Data.Set as Set -- ghc -import GHC.Builtin.Types.Literals - ( typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon - ) import GHC.Types.Unique.Set ( UniqSet , emptyUniqSet, unionManyUniqSets, unionUniqSets, unitUniqSet @@ -79,6 +76,9 @@ ) -- ghc-tcplugin-api +import GHC.Builtins + ( typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon + ) import GHC.TcPlugin.API import GHC.Utils.Outputable diff --git a/tests/ShouldError/Tasty.hs b/tests/ShouldError/Tasty.hs --- a/tests/ShouldError/Tasty.hs +++ b/tests/ShouldError/Tasty.hs @@ -9,11 +9,14 @@ import System.IO import System.IO.Temp import System.Process +import System.Timeout (timeout) import Test.Tasty.HUnit --- | Assert that a Haskell code snippet fails to compile with expected error messages -assertCompileError :: String -> [String] -> Assertion -assertCompileError source expectedErrors = do +-- | Compile a Haskell code snippet with the plugin enabled, with an optional +-- timeout in seconds. Returns 'Nothing' if the timeout expired, otherwise the +-- exit code and stderr output of GHC. +runGhc :: Maybe Int -> String -> IO (Maybe (ExitCode, String)) +runGhc timeLimit source = do -- XXX: This will pick the wrong GHC if the HC environment variable (as seen on CI) -- isn't set and the test suite is compiled with a GHC compiler other than the -- system's default. @@ -21,34 +24,57 @@ withSystemTempFile "ShouldError.hs" $ \tempFile tempHandle -> do hPutStr tempHandle source hClose tempHandle - (exitCode, _, stderrOutput) <- readProcessWithExitCode hc - [ "-XCPP" - , "-XAllowAmbiguousTypes" - , "-XConstraintKinds" - , "-XDataKinds" - , "-XFlexibleContexts" - , "-XGADTs" - , "-XScopedTypeVariables" - , "-XStandaloneDeriving" - , "-XTypeApplications" - , "-XTypeFamilies" - , "-XTypeOperators" - , "-XUndecidableInstances" - , "-XNoStarIsType" - , "-fno-code" - , "-fplugin", "GHC.TypeLits.Normalise" - , tempFile - ] "" - case exitCode of - ExitSuccess -> assertFailure "Expected compilation to fail but it succeeded" - ExitFailure _ -> - let cleanedStderr = removeProblemChars stderrOutput - cleanedExpected = map removeProblemChars expectedErrors - in if all (`isInfixOf` cleanedStderr) cleanedExpected - then return () - else assertFailure $ "Error message mismatch:\n" ++ - "Expected substrings: " ++ show expectedErrors ++ "\n" ++ - "Actual output:\n" ++ stderrOutput + let compile = readProcessWithExitCode hc + [ "-XCPP" + , "-XAllowAmbiguousTypes" + , "-XConstraintKinds" + , "-XDataKinds" + , "-XFlexibleContexts" + , "-XGADTs" + , "-XScopedTypeVariables" + , "-XStandaloneDeriving" + , "-XTypeApplications" + , "-XTypeFamilies" + , "-XTypeOperators" + , "-XUndecidableInstances" + , "-XNoStarIsType" + , "-fno-code" + , "-fplugin", "GHC.TypeLits.Normalise" + , tempFile + ] "" + result <- case timeLimit of + Nothing -> Just <$> compile + -- 'timeout' interrupts 'readProcessWithExitCode' with an asynchronous + -- exception, upon which it kills the GHC process before returning. + Just seconds -> timeout (seconds * 1000000) compile + return (fmap (\(exitCode, _, stderrOutput) -> (exitCode, stderrOutput)) result) + +-- | Assert that a Haskell code snippet compiles successfully within the given +-- number of seconds +assertCompileSuccessWithin :: Int -> String -> Assertion +assertCompileSuccessWithin seconds source = do + result <- runGhc (Just seconds) source + case result of + Nothing -> assertFailure $ + "Compilation did not finish within " ++ show seconds ++ " seconds" + Just (ExitFailure _, stderrOutput) -> assertFailure $ + "Expected compilation to succeed but it failed:\n" ++ stderrOutput + Just (ExitSuccess, _) -> return () + +-- | Assert that a Haskell code snippet fails to compile with expected error messages +assertCompileError :: String -> [String] -> Assertion +assertCompileError source expectedErrors = do + Just (exitCode, stderrOutput) <- runGhc Nothing source + case exitCode of + ExitSuccess -> assertFailure "Expected compilation to fail but it succeeded" + ExitFailure _ -> + let cleanedStderr = removeProblemChars stderrOutput + cleanedExpected = map removeProblemChars expectedErrors + in if all (`isInfixOf` cleanedStderr) cleanedExpected + then return () + else assertFailure $ "Error message mismatch:\n" ++ + "Expected substrings: " ++ show expectedErrors ++ "\n" ++ + "Actual output:\n" ++ stderrOutput -- | Remove problematic characters that vary depending on locale -- The kind and amount of quotes in GHC error messages changes depending on diff --git a/tests/Tests.hs b/tests/Tests.hs --- a/tests/Tests.hs +++ b/tests/Tests.hs @@ -45,6 +45,7 @@ import Test.Tasty.HUnit import qualified ShouldError +import ShouldError.Tasty (assertCompileSuccessWithin) data Vec :: Nat -> Type -> Type where Nil :: Vec 0 a @@ -666,6 +667,11 @@ "Proxy" ] , ShouldError.tests + , testGroup "Should compile with timeout" + [ testCase "issue 131: exponentiation of type family application terminates" $ do + source <- readFile "tests/WithTimeout/Test131.hs" + assertCompileSuccessWithin 10 source + ] ] showFin :: forall n. KnownNat n => Fin n -> String diff --git a/tests/WithTimeout/Test131.hs b/tests/WithTimeout/Test131.hs new file mode 100644 --- /dev/null +++ b/tests/WithTimeout/Test131.hs @@ -0,0 +1,75 @@ +-- Test for https://github.com/clash-lang/ghc-typelits-natnormalise/issues/131 +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE RankNTypes #-} + +#if __GLASGOW_HASKELL__ >= 805 +{-# LANGUAGE NoStarIsType #-} +#endif + +{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} + +module Main where + +import GHC.TypeLits +-- This file is compiled by a bare GHC invocation (see the unit-tests suite), +-- so Cabal's MIN_VERSION macros are not available: base-4.18 came with GHC 9.6. +#if __GLASGOW_HASKELL__ >= 906 + hiding (type SNat) +#endif + +import Data.Singletons (Apply, TyFun, type (@@)) +import Data.Proxy (Proxy (..)) +import Data.Kind (Type) + + +data SNat (n :: Nat) = KnownNat n => SNat (Proxy n) + +data Vec :: Nat -> Type -> Type where + Nil :: Vec 0 a + (:>) :: a -> Vec n a -> Vec (n + 1) a + +data RTree :: Nat -> Type -> Type where + LR :: a -> RTree 0 a + BR :: RTree d a -> RTree d a -> RTree (d+1) a + +data PowT (k :: Nat) (a :: Type) (f :: TyFun Nat Type) :: Type +type instance Apply (PowT k a) d = Vec (k^(2^d)) (RTree d a) + +instance Functor (Vec n) where + fmap = undefined + +tdfold :: forall p k a . KnownNat k + => Proxy (p :: TyFun Nat Type -> Type) + -> (a -> (p @@ 0)) + -> (forall l . SNat l -> (p @@ l) -> (p @@ l) -> (p @@ (l+1))) + -> RTree k a + -> (p @@ k) +tdfold _ _f _g = undefined + +trepeat :: KnownNat d => a -> RTree d a +trepeat = undefined + +vConcatMap :: (a -> Vec m b) -> Vec n a -> Vec (n * m) b +vConcatMap _f _xs = undefined + +type family MyTF a :: Nat where + MyTF Int = 3 + MyTF _ = 5 + +t131 :: forall d a. KnownNat d => Vec (MyTF a) a -> Vec (MyTF a^(2^d)) (RTree d a) +t131 v = tdfold + (Proxy @(PowT (MyTF a) a)) + (const $ LR <$> v) + (\(_ :: SNat m) l r -> vConcatMap ((<$> r) . BR) l) + (trepeat @d ()) + +main :: IO () +main = putStrLn "OK"