packages feed

ghc-typelits-natnormalise 0.7.2 → 0.7.3

raw patch · 7 files changed

+184/−31 lines, 7 filesdep +ghc-bignumdep −sybdep ~ghcPVP ok

version bump matches the API change (PVP)

Dependencies added: ghc-bignum

Dependencies removed: syb

Dependency ranges changed: ghc

API changes (from Hackage documentation)

Files

CHANGELOG.md view
@@ -1,5 +1,8 @@ # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package +## 0.7.3 *January 1st 2021*+* Build on GHC 9.0.1-rc1+ ## 0.7.2 *March 9 2020* * Fixes [#44](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/44) infinite loop due to boxed equality
ghc-typelits-natnormalise.cabal view
@@ -1,5 +1,5 @@ name:                ghc-typelits-natnormalise-version:             0.7.2+version:             0.7.3 synopsis:            GHC typechecker plugin for types of kind GHC.TypeLits.Nat description:   A type checker plugin for GHC that can solve /equalities/ and /inequalities/@@ -49,7 +49,7 @@                      CHANGELOG.md cabal-version:       >=1.10 tested-with:         GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.4, GHC == 8.6.5,-                     GHC == 8.8.1, GHC == 8.10.1+                     GHC == 8.8.4, GHC == 8.10.3, GHC == 9.0.1  source-repository head   type: git@@ -67,11 +67,13 @@                        GHC.TypeLits.Normalise.Unify   build-depends:       base                >=4.9   && <5,                        containers          >=0.5.7.1 && <0.7,-                       ghc                 >=8.0.1 && <8.11,+                       ghc                 >=8.0.1 && <9.2,                        ghc-tcplugins-extra >=0.3.1,-                       integer-gmp         >=1.0   && <1.1,-                       syb                 >=0.7.1 && <0.8,                        transformers        >=0.5.2.0 && < 0.6+  if impl(ghc >= 9.0.0)+    build-depends:     ghc-bignum >=1.0 && <1.1+  else+    build-depends:     integer-gmp >=1.0 && <1.1   hs-source-dirs:      src   default-language:    Haskell2010   other-extensions:    CPP
src/GHC/TypeLits/Normalise.hs view
@@ -164,6 +164,7 @@ #endif import Control.Monad.Trans.Writer.Strict import Data.Either         (partitionEithers, rights)+import Data.IORef import Data.List           (intersect, partition, stripPrefix, find) import Data.Maybe          (mapMaybe, catMaybes) import Data.Set            (Set, empty, toList, notMember, fromList, union)@@ -175,6 +176,31 @@ import Text.Read           (readMaybe)  -- GHC API+#if MIN_VERSION_ghc(9,0,0)+import GHC.Builtin.Names (knownNatClassName, eqTyConKey, heqTyConKey, hasKey)+import GHC.Builtin.Types (promotedFalseDataCon, promotedTrueDataCon, typeNatKind)+import GHC.Builtin.Types.Literals+  (typeNatAddTyCon, typeNatExpTyCon, typeNatLeqTyCon, typeNatMulTyCon,+   typeNatSubTyCon)+import GHC.Core (Expr (..))+import GHC.Core.Coercion (CoercionHole, Role (..), mkUnivCo)+import GHC.Core.Predicate+  (EqRel (NomEq), Pred (EqPred), classifyPredType, getEqPredTys, mkClassPred,+   mkPrimEqPred, isEqPred, isEqPrimPred)+import GHC.Core.TyCo.Rep (Type (..), UnivCoProvenance (..))+import GHC.Core.Type+  (Kind, PredType, eqType, mkTyVarTy, tyConAppTyCon_maybe, typeKind)+import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin)+import GHC.Tc.Plugin+  (TcPluginM, newCoercionHole, tcLookupClass, tcPluginTrace, tcPluginIO)+import GHC.Tc.Types (TcPlugin (..), TcPluginResult (..))+import GHC.Tc.Types.Constraint+  (Ct, CtEvidence (..), CtLoc, TcEvDest (..), ShadowInfo (WDeriv), ctEvidence,+   ctLoc, ctLocSpan, isGiven, isWanted, mkNonCanonical, setCtLoc, setCtLocSpan,+   isWantedCt, ctEvLoc, ctEvPred, ctEvExpr)+import GHC.Tc.Types.Evidence (EvTerm (..), evCast)+import GHC.Utils.Outputable (Outputable (..), (<+>), ($$), text)+#else #if MIN_VERSION_ghc(8,5,0) import CoreSyn    (Expr (..)) #endif@@ -207,7 +233,6 @@  import TcTypeNats (typeNatLeqTyCon) import TysWiredIn (promotedFalseDataCon, promotedTrueDataCon)-import Data.IORef  #if MIN_VERSION_ghc(8,10,0) import Constraint@@ -248,6 +273,7 @@ #if MIN_VERSION_ghc(8,10,0) import TcType (isEqPrimPred) #endif+#endif  -- internal import GHC.TypeLits.Normalise.SOP@@ -479,11 +505,13 @@       _  -> do         tcPluginTrace ("simplifyNats(backtrack: " ++ show (length fancyGivens) ++ ")")                       (ppr varEqs)-        foldr findFirstSimpliedWanted (Simplified []) <$>-              mapM (\v -> do let eqs = v ++ eqsW-                             tcPluginTrace "simplifyNats" (ppr eqs)-                             simples [] [] [] [] eqs)-              fancyGivens++        allSimplified <- forM fancyGivens $ \v -> do+          let eqs = v ++ eqsW+          tcPluginTrace "simplifyNats" (ppr eqs)+          simples [] [] [] [] eqs++        pure (foldr findFirstSimpliedWanted (Simplified []) allSimplified)   where     simples :: [CoreUnify]             -> [((EvTerm, Ct), [Ct])]
src/GHC/TypeLits/Normalise/SOP.hs view
@@ -73,6 +73,9 @@ x^(y*z) @ -}++{-# LANGUAGE CPP #-}+ module GHC.TypeLits.Normalise.SOP   ( -- * SOP types     Symbol (..)@@ -94,7 +97,11 @@ import Data.List   (sort)  -- GHC API-import Outputable  (Outputable (..), (<+>), text, hcat, integer, punctuate)+#if MIN_VERSION_ghc(9,0,0)+import GHC.Utils.Outputable (Outputable (..), (<+>), text, hcat, integer, punctuate)+#else+import Outputable (Outputable (..), (<+>), text, hcat, integer, punctuate)+#endif  data Symbol v c   = I Integer                 -- ^ Integer constant
src/GHC/TypeLits/Normalise/Unify.hs view
@@ -48,13 +48,11 @@  -- External import Control.Arrow (first, second)-import Control.Monad.Trans.Maybe import Control.Monad.Trans.Writer.Strict import Data.Function (on)-import Data.List     ((\\), intersect, mapAccumL, nub)-import Data.Maybe    (fromMaybe, mapMaybe)+import Data.List     ((\\), intersect, nub)+import Data.Maybe    (fromMaybe, mapMaybe, isJust) import Data.Set      (Set)-import Data.Generics (mkM, everywhereM) import qualified Data.Set as Set  import GHC.Base               (isTrue#,(==#))@@ -62,10 +60,26 @@ import GHC.Integer.Logarithms (integerLogBase#)  -- GHC API+#if MIN_VERSION_ghc(9,0,0)+import GHC.Builtin.Types (boolTy, promotedTrueDataCon, typeNatKind)+import GHC.Builtin.Types.Literals+  (typeNatAddTyCon, typeNatExpTyCon, typeNatLeqTyCon, typeNatMulTyCon, typeNatSubTyCon)+import GHC.Core.Predicate (EqRel (NomEq), Pred (EqPred), classifyPredType, mkPrimEqPred)+import GHC.Core.TyCon (TyCon)+import GHC.Core.Type+  (PredType, TyVar, coreView, eqType, mkNumLitTy, mkTyConApp, mkTyVarTy, nonDetCmpType, typeKind)+import GHC.Core.TyCo.Rep (Kind, Type (..), TyLit (..))+import GHC.Tc.Plugin (TcPluginM, tcPluginTrace)+import GHC.Tc.Types.Constraint (Ct, ctEvidence, ctEvId, ctEvPred, isGiven)+import GHC.Types.Unique.Set+  (UniqSet, unionManyUniqSets, emptyUniqSet, unionUniqSets, unitUniqSet)+import GHC.Utils.Outputable (Outputable (..), (<+>), ($$), text)+#else import Outputable    (Outputable (..), (<+>), ($$), text) import TcPluginM     (TcPluginM, tcPluginTrace) import TcTypeNats    (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon,                       typeNatSubTyCon, typeNatLeqTyCon)+import TyCon         (TyCon) import Type          (TyVar,                       coreView, eqType, mkNumLitTy, mkTyConApp, mkTyVarTy,                       nonDetCmpType, PredType, typeKind)@@ -82,6 +96,7 @@ import TcRnTypes  (ctEvPred) import Type       (EqRel (NomEq), PredTree (EqPred), classifyPredType, mkPrimEqPred) #endif+#endif  -- Internal import GHC.TypeLits.Normalise.SOP@@ -123,19 +138,50 @@   | tc == typeNatExpTyCon = normaliseExp <$> normaliseNat x <*> normaliseNat y normaliseNat t = return (S [P [C (CType t)]]) --- | Applies 'normaliseNat' and 'simplifySOP' to type or predicats---   to reduce any occurence of sub-terms---   of /kind/ 'GHC.TypeLits.Nat'.---   If the result is the same as input, returns @'Nothing'@.-normaliseNatEverywhere-  :: Type -> Writer [(Type, Type)] (Maybe Type)-normaliseNatEverywhere ty-  | typeKind ty `eqType` typeNatKind = do-      ty' <- normaliseSimplifyNat ty-      return $ if ty `eqType` ty' then Nothing else Just ty'-  | otherwise = do-      ty' <- everywhereM (mkM normaliseSimplifyNat) ty-      return $ if ty `eqType` ty' then Nothing else Just ty'+-- | Runs writer action. If the result /Nothing/ writer actions will be+-- discarded.+maybeRunWriter+  :: Monoid a+  => Writer a (Maybe b)+  -> Writer a (Maybe b)+maybeRunWriter w =+  case runWriter w of+    (Nothing, _) -> pure Nothing+    (b, a) -> tell a >> pure b++-- | 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 :: Type -> Writer [(Type, Type)] (Maybe Type)+normaliseNatEverywhere ty0+  | TyConApp tc _fields <- ty0+  , tc `elem` knownTyCons = do+    -- Normalize under current type constructor application. 'go' skips all+    -- known type constructors.+    ty1M <- maybeRunWriter (go ty0)+    let ty1 = fromMaybe ty0 ty1M++    -- Normalize (subterm-normalized) type given to 'normaliseNatEverywhere'+    ty2 <- normaliseSimplifyNat ty1+    -- TODO: 'normaliseNat' could keep track whether it changed anything. That's+    -- TODO: probably cheaper than checking for equality here.+    pure (if ty2 `eqType` ty1 then ty1M else Just ty2)+  | otherwise = go ty0+ where+  knownTyCons :: [TyCon]+  knownTyCons = [typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon, typeNatAddTyCon]++  -- Normalize given type, but ignore all top-level+  go :: Type -> Writer [(Type, Type)] (Maybe Type)+  go (TyConApp tc_ fields0_) = do+    fields1_ <- mapM (maybeRunWriter . cont) fields0_+    if any isJust fields1_ then+      pure (Just (TyConApp tc_ (zipWith fromMaybe fields0_ fields1_)))+    else+      pure Nothing+   where+    cont = if tc_ `elem` knownTyCons then go else normaliseNatEverywhere+  go _ = pure Nothing  normaliseSimplifyNat :: Type -> Writer [(Type, Type)] Type normaliseSimplifyNat ty
tests/ErrorTests.hs view
@@ -29,9 +29,15 @@ testProxy1 = id  testProxy1Errors =+#if __GLASGOW_HASKELL__ >= 900+  ["Expected: Proxy (x + 1) -> Proxy (2 + x)"+  ,"  Actual: Proxy (x + 1) -> Proxy (x + 1)"+  ]+#else   ["Expected type: Proxy (x + 1) -> Proxy (2 + x)"   ,"Actual type: Proxy (2 + x) -> Proxy (2 + x)"   ]+#endif  type family GCD (x :: Nat) (y :: Nat) :: Nat type instance GCD 6 8 = 2@@ -41,9 +47,15 @@ testProxy2 = id  testProxy2Errors =+#if __GLASGOW_HASKELL__ >= 900+  ["Expected: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6)"+  ,"  Actual: Proxy (2 + x) -> Proxy (2 + x)"+  ]+#else   ["Expected type: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6)"   ,"Actual type: Proxy (x + 3) -> Proxy (x + 3)"   ]+#endif  proxyFun3 :: Proxy (x + x + x) -> () proxyFun3 = const ()@@ -52,9 +64,15 @@ testProxy3 = proxyFun3  testProxy3Errors =+#if __GLASGOW_HASKELL__ >= 900+  ["Expected: Proxy 8 -> ()"+  ,"  Actual: Proxy ((x0 + x0) + x0) -> ()"+  ]+#else   ["Expected type: Proxy 8 -> ()"   ,"Actual type: Proxy ((x0 + x0) + x0) -> ()"   ]+#endif  proxyFun4 :: Proxy ((2*y)+4) -> () proxyFun4 = const ()@@ -63,17 +81,29 @@ testProxy4 = proxyFun4  testProxy4Errors =+#if __GLASGOW_HASKELL__ >= 900+  ["Expected: Proxy 2 -> ()"+  ,"  Actual: Proxy ((2 * y0) + 4) -> ()"+  ]+#else   ["Expected type: Proxy 2 -> ()"   ,"Actual type: Proxy ((2 * y0) + 4) -> ()"   ]+#endif  testProxy5 :: Proxy 7 -> () testProxy5 = proxyFun4  testProxy5Errors =+#if __GLASGOW_HASKELL__ >= 900+  ["Expected: Proxy 7 -> ()"+  ,"  Actual: Proxy ((2 * y1) + 4) -> ()"+  ]+#else   ["Expected type: Proxy 7 -> ()"   ,"Actual type: Proxy ((2 * y1) + 4) -> ()"   ]+#endif  proxyFun6 :: Proxy (2^k) -> Proxy (2^k) proxyFun6 = const Proxy@@ -82,9 +112,15 @@ testProxy6 = proxyFun6 (Proxy :: Proxy 7)  testProxy6Errors =+#if __GLASGOW_HASKELL__ >= 900+  ["Expected: Proxy (2 ^ k0)"+  ,"  Actual: Proxy 7"+  ]+#else   ["Expected type: Proxy (2 ^ k0)"   ,"Actual type: Proxy 7"   ]+#endif  proxyFun7 :: Proxy (2^k) -> Proxy k proxyFun7 = const Proxy@@ -93,9 +129,15 @@ testProxy8 = id  testProxy8Errors =+#if __GLASGOW_HASKELL__ >= 900+  ["Expected: Proxy x -> Proxy (y + x)"+  ,"  Actual: Proxy x -> Proxy x"+  ]+#else   ["Expected type: Proxy x -> Proxy (y + x)"   ,"Actual type: Proxy x -> Proxy x"   ]+#endif  proxyInEq :: (a <= b) => Proxy a -> Proxy b -> () proxyInEq _ _ = ()@@ -170,9 +212,15 @@ testProxy15 = id  testProxy15Errors =+#if __GLASGOW_HASKELL__ >= 900+  ["Expected: Proxy n -> Proxy (n + d)"+  ,"  Actual: Proxy n -> Proxy n"+  ]+#else   ["Expected type: Proxy n -> Proxy (n + d)"   ,"Actual type: Proxy n -> Proxy n"   ]+#endif  data Fin (n :: Nat) where   FZ :: Fin (n + 1)
tests/Tests.hs view
@@ -282,7 +282,7 @@   -> (forall (m :: Nat) . f (m + k) -> r)   -- ^ Function with the @(n + k)@ constraint   -> r-leToPlus _ a f = f @ (n-k) a+leToPlus _ a f = f @(n-k) a  data BNat :: Nat -> Type where   BT :: BNat 0@@ -340,6 +340,25 @@   -> Proxy x proxyEq3 _ _ x = x +-- Would yield (b <=? c) ~ 'True+proxyEq4+  :: forall a b c+   . (KnownNat a, c <= b, b <= a)+  => Proxy b+  -> Proxy c+  -> Proxy a+  -> Proxy (((a - b) + c) + (b - c))+proxyEq4 = theProxy+ where+  theProxy+    :: forall a b c+     . (KnownNat (((a - b) + c) + (b - c)), c <= b, b <= a)+    => Proxy b+    -> Proxy c+    -> Proxy a+    -> Proxy (((a - b) + c) + (b - c))+  theProxy _ _ = id+ proxyInEqImplication :: (2 <= (2 ^ (n + d)))   => Proxy d   -> Proxy n@@ -557,7 +576,7 @@       , testCase "2a <=? 4a ~ False" $ testProxy14 `throws` testProxy14Errors       , testCase "Show (Boo n) => Show (Boo (n - 1 + 1))" $           testProxy17 `throws` test17Errors-      , testCase "1 <= m, m <= rp implies 1 <= rp - m" $ (testProxy19 (Proxy @ 1) (Proxy @ 1)) `throws` test19Errors+      , testCase "1 <= m, m <= rp implies 1 <= rp - m" $ (testProxy19 (Proxy @1) (Proxy @1)) `throws` test19Errors       ]     ]   ]