ghc-typelits-natnormalise 0.9.6 → 0.9.7

raw patch · 10 files changed

+187/−69 lines, 10 filesdep +singletonsdep ~ghcdep ~ghc-tcplugin-apiPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: singletons

Dependency ranges changed: ghc, ghc-tcplugin-api

API changes (from Hackage documentation)

Files

• CHANGELOG.md +6/−0
• README.md +0/−1
• ghc-typelits-natnormalise.cabal +10/−6
• src/GHC/TypeLits/Normalise.hs +12/−14
• src/GHC/TypeLits/Normalise/Compat.hs +17/−14
• src/GHC/TypeLits/Normalise/SOP.hs +1/−0
• src/GHC/TypeLits/Normalise/Unify.hs +3/−3
• tests/ShouldError/Tasty.hs +57/−31
• tests/Tests.hs +6/−0
• tests/WithTimeout/Test131.hs +75/−0

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

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

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

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

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

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

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

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

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

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