diff --git a/CHANGELOG.md b/CHANGELOG.md --- 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 +## 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 diff --git a/ghc-typelits-natnormalise.cabal b/ghc-typelits-natnormalise.cabal --- a/ghc-typelits-natnormalise.cabal +++ b/ghc-typelits-natnormalise.cabal @@ -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 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 @@ -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])] 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 @@ -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 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 @@ -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 diff --git a/tests/ErrorTests.hs b/tests/ErrorTests.hs --- a/tests/ErrorTests.hs +++ b/tests/ErrorTests.hs @@ -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) diff --git a/tests/Tests.hs b/tests/Tests.hs --- a/tests/Tests.hs +++ b/tests/Tests.hs @@ -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 ] ] ]