ghc-typelits-natnormalise 0.8.1 → 0.9.0

raw patch · 5 files changed

+43/−40 lines, 5 filesdep ~containersPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: containers

API changes (from Hackage documentation)

Files

• CHANGELOG.md +5/−0
• ghc-typelits-natnormalise.cabal +2/−2
• src/GHC/TypeLits/Normalise.hs +16/−17
• src/GHC/TypeLits/Normalise/SOP.hs +2/−1
• src/GHC/TypeLits/Normalise/Unify.hs +18/−20

@@ -1,5 +1,10 @@ # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package +## 0.9.0 *October 17th 2025*+* Drop `TyConSubst` argument from `normaliseNat`, `normaliseNatEverywhere` and `normaliseSimplifyNat`.+* Expose `GHC.TypeLits.Normalise.Compat`+* Report contractions for equations such as `1 + k <= n; n ~ 0` in "solve givens" phase+ ## 0.8.1 *October 1st 2025* * Fixes [#85](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/85) Deriving equalities from inequalities produces a misleading error message * Fixes [#94](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/94) Normalization fails when adding an equality constraint with substraction

@@ -1,6 +1,6 @@ cabal-version:       3.0 name:                ghc-typelits-natnormalise-version:             0.8.1+version:             0.9.0 synopsis:            GHC typechecker plugin for types of kind GHC.TypeLits.Nat description:   A type checker plugin for GHC that can solve /equalities/ and /inequalities/@@ -64,9 +64,9 @@  library   exposed-modules:     GHC.TypeLits.Normalise,+                       GHC.TypeLits.Normalise.Compat,                        GHC.TypeLits.Normalise.SOP,                        GHC.TypeLits.Normalise.Unify-  other-modules:       GHC.TypeLits.Normalise.Compat   build-depends:       base                >=4.9   && <5,                        containers          >=0.5.7.1 && <0.8,                        ghc                 >=8.8.1 && <9.15,

@@ -283,7 +283,7 @@    do     let       givensTyConSubst = mkTyConSubst givens-    (redGivens, _) <- reduceGivens False opts tcs givensTyConSubst givens+    (redGivens, _) <- reduceGivens False opts tcs givens      tcPluginTrace "decideEqualSOP Givens {" $       vcat [ text "givens:" <+> ppr givens ]@@ -318,10 +318,10 @@                         . ctEvidence )                  wanteds -    (redGivens, negWanteds) <- reduceGivens True opts tcs givensTyConSubst givens+    (redGivens, negWanteds) <- reduceGivens True opts tcs givens     reducible_wanteds       <- catMaybes <$> mapM (\ct -> fmap (ct,) <$>-                                    reduceNatConstr givensTyConSubst redGivens ct)+                                    reduceNatConstr redGivens ct)                             nonEqs      tcPluginTrace "decideEqualSOP Wanteds {" $@@ -378,14 +378,14 @@ type NatInEquality = (Ct,(CoreSOP,CoreSOP,Bool))  reduceGivens :: Bool -- ^ allow generating new "non-negative" Wanteds-             -> Opts -> LookedUpTyCons -> TyConSubst+             -> Opts -> LookedUpTyCons              -> [Ct]              -> TcPluginM Solve ([Ct], Map CType CtLoc)-reduceGivens gen_wanteds opts tcs givensTyConSubst origGivens = go [] Map.empty origGivens+reduceGivens gen_wanteds opts tcs origGivens = go [] Map.empty origGivens   where     go rev_acc_gs acc_ws [] = return ( reverse rev_acc_gs, acc_ws )     go rev_acc_gs acc_ws (g:gs) =-      case tryReduceGiven opts tcs givensTyConSubst origGivens g of+      case tryReduceGiven opts tcs origGivens g of         Just ( pred', evExpr, ws )           | gen_wanteds || null ws || negNumbers opts           -> do@@ -402,12 +402,11 @@  tryReduceGiven   :: Opts -> LookedUpTyCons-  -> TyConSubst   -> [Ct] -> Ct   -> Maybe (PredType, EvTerm, [PredType])-tryReduceGiven opts tcs givensTyConSubst simplGivens ct = do+tryReduceGiven opts tcs simplGivens ct = do     let (mans, ws) =-          runWriter $ normaliseNatEverywhere givensTyConSubst $+          runWriter $ normaliseNatEverywhere $           ctEvPred $ ctEvidence ct         ws' = [ p               | p <- subToPred opts tcs ws@@ -425,10 +424,10 @@ fromNatEquality (Left  (ct, _, _)) = ct fromNatEquality (Right (ct, _))    = ct -reduceNatConstr :: TyConSubst -> [Ct] -> Ct -> TcPluginM Solve (Maybe (EvTerm, [(Type, Type)], [Ct]))-reduceNatConstr givensTyConSubst givens ct = do+reduceNatConstr :: [Ct] -> Ct -> TcPluginM Solve (Maybe (EvTerm, [(Type, Type)], [Ct]))+reduceNatConstr givens ct = do   let pred0 = ctEvPred $ ctEvidence ct-      (mans, tests) = runWriter $ normaliseNatEverywhere givensTyConSubst pred0+      (mans, tests) = runWriter $ normaliseNatEverywhere pred0        -- Even if we didn't rewrite the Wanted,       -- we may still be able to solve it from a (rewritten) Given.@@ -666,8 +665,8 @@ toNatEquality tcs givensTyConSubst ct0   | Just (((x,y), mbLTE), cos0) <- isNatRel tcs givensTyConSubst pred0   , let-      ((x', cos1),k1) = runWriter (normaliseNat givensTyConSubst x)-      ((y', cos2),k2) = runWriter (normaliseNat givensTyConSubst y)+      ((x', cos1),k1) = runWriter (normaliseNat x)+      ((y', cos2),k2) = runWriter (normaliseNat y)       ks      = k1 ++ k2   = case mbLTE of       Nothing ->@@ -685,7 +684,7 @@         -- See https://github.com/clash-lang/ghc-typelits-natnormalise/issues/94.         | isGiven (ctEvidence ct0)         , className kn == knownNatClassName-        , let ((x', cos0), ks) = runWriter (normaliseNat givensTyConSubst x)+        , let ((x', cos0), ks) = runWriter (normaliseNat x)         -> [(Right (ct0, (S [], x', True)), ks, cos0)]       _ -> []   where@@ -716,8 +715,8 @@     rewrite x y       | isNatKind (typeKind x)       , isNatKind (typeKind y)-      , let ((x', cos1),k1) = runWriter (normaliseNat givensTyConSubst x)-      , let ((y', cos2),k2) = runWriter (normaliseNat givensTyConSubst y)+      , let ((x', cos1),k1) = runWriter (normaliseNat x)+      , let ((y', cos2),k2) = runWriter (normaliseNat y)       = [(Left (ct0,x',y'),k1 ++ k2, cos1 ++ cos2)]       | otherwise       = []

@@ -128,7 +128,8 @@   (S ps1) == (S ps2)      = ps1 == ps2  instance (Outputable v, Outputable c) => Outputable (SOP v c) where-  ppr = hcat . punctuate (text " + ") . map ppr . unS+  ppr (S []) = integer 0+  ppr (S s) = hcat . punctuate (text " + ") . map ppr $ s  instance (Outputable v, Outputable c) => Outputable (Product v c) where   ppr = hcat . punctuate (text " * ") . map ppr . unP

@@ -79,8 +79,6 @@  -- ghc-tcplugin-api import GHC.TcPlugin.API-import GHC.TcPlugin.API.TyConSubst-  ( TyConSubst ) import GHC.Utils.Outputable  @@ -113,8 +111,8 @@ -- * literals -- * type variables -- * Applications of the arithmetic operators @(+,-,*,^)@-normaliseNat :: TyConSubst -> Type -> Writer [(Type,Type)] (CoreSOP, [Coercion])-normaliseNat givensTyConSubst ty+normaliseNat :: Type -> Writer [(Type,Type)] (CoreSOP, [Coercion])+normaliseNat ty   | Just (tc, xs) <- splitTyConApp_maybe ty   = goTyConApp tc xs   | Just i <- isNumLitTy ty@@ -127,21 +125,21 @@       goTyConApp :: TyCon -> [Type] -> Writer [(Type,Type)] (CoreSOP, [Coercion])       goTyConApp tc [x,y]         | tc == typeNatAddTyCon =-            do (x', cos1) <- normaliseNat givensTyConSubst x-               (y', cos2) <- normaliseNat givensTyConSubst y+            do (x', cos1) <- normaliseNat x+               (y', cos2) <- normaliseNat y                return (mergeSOPAdd x' y', cos1 ++ cos2)         | tc == typeNatSubTyCon = do-          (x', cos1) <- normaliseNat givensTyConSubst x-          (y', cos2) <- normaliseNat givensTyConSubst y+          (x', cos1) <- normaliseNat x+          (y', cos2) <- normaliseNat y           tell [(reifySOP $ simplifySOP x', reifySOP $ simplifySOP y')]           return (mergeSOPAdd x' (mergeSOPMul (S [P [I (-1)]]) y'), cos1 ++ cos2)         | tc == typeNatMulTyCon =-          do (x', cos1) <- normaliseNat givensTyConSubst x-             (y', cos2) <- normaliseNat givensTyConSubst y+          do (x', cos1) <- normaliseNat x+             (y', cos2) <- normaliseNat y              return (mergeSOPMul x' y', cos1 ++ cos2)         | tc == typeNatExpTyCon =-          do (x', cos1) <- normaliseNat givensTyConSubst x-             (y', cos2) <- normaliseNat givensTyConSubst y+          do (x', cos1) <- normaliseNat x+             (y', cos2) <- normaliseNat y              return (normaliseExp x' y', cos1 ++ cos2)       goTyConApp tc xs         = return (S [P [C (CType $ mkTyConApp tc xs)]], [])@@ -164,8 +162,8 @@ -- | Applies 'normaliseNat' and 'simplifySOP' to type or predicates to reduce -- any occurrences of sub-terms of /kind/ 'GHC.TypeLits.Nat'. If the result is -- the same as input, returns @'Nothing'@.-normaliseNatEverywhere :: TyConSubst -> Type -> Writer [(Type, Type)] (Maybe (Type, [Coercion]))-normaliseNatEverywhere givensTyConSubst ty0+normaliseNatEverywhere :: Type -> Writer [(Type, Type)] (Maybe (Type, [Coercion]))+normaliseNatEverywhere ty0   | Just (tc, fields) <- splitTyConApp_maybe ty0   =   if tc `elem` knownTyCons       then do@@ -174,7 +172,7 @@         ty1M <- maybeRunWriter (go tc fields)         let (ty1, cos1) = fromMaybe (ty0, []) ty1M         -- Normalize (subterm-normalized) type given to 'normaliseNatEverywhere'-        (ty2, cos2) <- normaliseSimplifyNat givensTyConSubst ty1+        (ty2, cos2) <- normaliseSimplifyNat ty1         -- TODO: 'normaliseNat' could keep track whether it changed anything. That's         -- TODO: probably cheaper than checking for equality here.         pure $@@ -205,12 +203,12 @@       , Just (tc', flds') <- splitTyConApp_maybe ty'       = go tc' flds'       | otherwise-      = normaliseNatEverywhere givensTyConSubst ty'+      = normaliseNatEverywhere ty' -normaliseSimplifyNat :: TyConSubst -> Type -> Writer [(Type, Type)] (Type, [Coercion])-normaliseSimplifyNat givensTyConSubst ty+normaliseSimplifyNat :: Type -> Writer [(Type, Type)] (Type, [Coercion])+normaliseSimplifyNat ty   | typeKind ty `eqType` natKind = do-      (ty', cos1) <- normaliseNat givensTyConSubst ty+      (ty', cos1) <- normaliseNat ty       return $ (reifySOP $ simplifySOP ty', cos1)   | otherwise = return (ty, []) @@ -790,7 +788,7 @@   = any canBeZero bs   | otherwise   = True-canBeZero (V {}) = True -- e.g. 'tau' where 'tau' is an unfilled metavariable+canBeZero (V v) = isMetaTyVar v -- e.g. 'tau' where 'tau' is an unfilled metavariable  -- | Try to solve inequalities solveIneq