From adbed1de02595b055737d99be06c427f89e06daf Mon Sep 17 00:00:00 2001 From: Junji Hashimoto Date: Sun, 17 Dec 2023 08:20:24 +0000 Subject: [PATCH 1/2] Relaxed ghc's version --- typelevel-rewrite-rules.cabal | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/typelevel-rewrite-rules.cabal b/typelevel-rewrite-rules.cabal index 09a23b8..02547c4 100644 --- a/typelevel-rewrite-rules.cabal +++ b/typelevel-rewrite-rules.cabal @@ -48,7 +48,7 @@ library build-depends: base >=4.12 && <5 , containers >=0.6.2.1 - , ghc >=8.10.2 && <9.4 + , ghc >=8.10.2 && <9.8 , ghc-prim >=0.5.3 , term-rewriting >=0.3.0.1 , transformers >=0.5.6.2 From 54d087138afd86aea6de4bc7b9a17e3402978637 Mon Sep 17 00:00:00 2001 From: Junji Hashimoto Date: Sun, 21 Apr 2024 14:34:39 +0900 Subject: [PATCH 2/2] Fix codes for ghc-9.6 --- src/TypeLevel/Rewrite.hs | 118 +++++++++++++---------- src/TypeLevel/Rewrite/Internal/Lookup.hs | 8 ++ src/TypeLevel/Rewrite/Internal/TypeEq.hs | 3 + 3 files changed, 77 insertions(+), 52 deletions(-) diff --git a/src/TypeLevel/Rewrite.hs b/src/TypeLevel/Rewrite.hs index 5d1ef6a..45d2d36 100644 --- a/src/TypeLevel/Rewrite.hs +++ b/src/TypeLevel/Rewrite.hs @@ -8,7 +8,19 @@ import Data.Foldable import Data.Traversable -- GHC API -#if MIN_VERSION_ghc(9,0,0) +#if MIN_VERSION_ghc(9,6,0) +import GHC.Core.Coercion (Role(Representational), mkUnivCo) +import GHC.Tc.Types.Constraint (CtEvidence(ctev_loc), Ct, ctEvExpr, ctLoc, mkNonCanonical) +import GHC.Plugins (PredType, SDoc, fsep, ppr) +import GHC.Tc.Utils.TcType (eqType) +import GHC.Plugins (Plugin(pluginRecompile, tcPlugin), CommandLineOption, defaultPlugin, purePlugin) +import GHC.Tc.Types.Evidence (EvExpr, EvTerm, evCast) +import GHC.Tc.Plugin (newWanted) +import GHC.Core.TyCo.Rep (UnivCoProvenance(PluginProv)) +import GHC.Plugins (synTyConDefn_maybe) +import GHC.Tc.Types (TcPluginSolveResult(..), TcPluginM, ErrCtxt, pushErrCtxtSameOrigin, TcPlugin(..), TcPluginSolver) +import GHC.Types.Unique.FM ( emptyUFM ) +#elif MIN_VERSION_ghc(9,0,0) import GHC.Core.Coercion (Role(Representational), mkUnivCo) import GHC.Tc.Types.Constraint (CtEvidence(ctev_loc), Ct, ctEvExpr, ctLoc, mkNonCanonical) import GHC.Plugins (PredType, SDoc, eqType, fsep, ppr) @@ -50,9 +62,12 @@ data ReplaceCt = ReplaceCt , replacementConstraints :: [Ct] } + +-- See https://gitlab.haskell.org/ghc/ghc/-/commit/9d4ba36f1de7ced62e2c0c6a911411144e9a3b27 +-- Change TcPluginResult to TcPluginSolveResult. combineReplaceCts :: [ReplaceCt] - -> TcPluginResult + -> TcPluginSolveResult combineReplaceCts replaceCts = TcPluginOk (fmap solvedConstraint replaceCts) (foldMap replacementConstraints replaceCts) @@ -122,6 +137,7 @@ plugin = defaultPlugin { tcPlugin = \args -> Just $ TcPlugin { tcPluginInit = lookupTypeRules args , tcPluginSolve = solve + , tcPluginRewrite = \_ -> emptyUFM , tcPluginStop = \_ -> pure () } , pluginRecompile = purePlugin @@ -155,53 +171,51 @@ newRuleInducedWanted oldCt rule newPredType = do solve :: [TypeRule] - -> [Ct] -- ^ Given constraints - -> [Ct] -- ^ Derived constraints - -> [Ct] -- ^ Wanted constraints - -> TcPluginM TcPluginResult -solve _ _ _ [] = do - pure $ TcPluginOk [] [] -solve rules givens _ wanteds = do - typeSubst <- execWriterT $ do - for_ givens $ \given -> do - for_ (asEqualityConstraint given) $ \(lhs, rhs) -> do - -- lhs ~ rhs - -- where lhs is typically an expression and rhs is typically a variable - let var = TypeEq rhs - let val = toTypeTerm lhs - tell [(var, val)] - - replaceCts <- execWriterT $ do - for_ wanteds $ \wanted -> do - -- wanted => ... - for_ (asDecomposedConstraint wanted) $ \types -> do - -- C a b c => ... - - -- C a b c - let typeTerms = fmap toTypeTerm types - let predType = fromDecomposeConstraint types - - for_ (applyRules typeSubst rules typeTerms) $ \(rule, typeTerms') -> do - -- C a' b' c' - let types' = fmap fromTypeTerm typeTerms' - let predType' = fromDecomposeConstraint types' - - unless (eqType predType' predType) $ do - -- co :: C a' b' c' ~R C a b c - let co = mkUnivCo - (PluginProv "TypeLevel.Rewrite") - Representational - predType' - predType - evWanted' <- lift $ newRuleInducedWanted wanted rule predType' - let wanted' = mkNonCanonical evWanted' - let futureDict :: EvExpr - futureDict = ctEvExpr evWanted' - let replaceCt :: ReplaceCt - replaceCt = ReplaceCt - { evidenceOfCorrectness = evCast futureDict co - , replacedConstraint = wanted - , replacementConstraints = [wanted'] - } - tell [replaceCt] - pure $ combineReplaceCts replaceCts + -> TcPluginSolver +solve rules = \_ givens wanteds' -> + case wanteds' of + [] -> pure (TcPluginOk [] []) + wanteds -> do + typeSubst <- execWriterT $ do + for_ givens $ \given -> do + for_ (asEqualityConstraint given) $ \(lhs, rhs) -> do + -- lhs ~ rhs + -- where lhs is typically an expression and rhs is typically a variable + let var = TypeEq rhs + let val = toTypeTerm lhs + tell [(var, val)] + + replaceCts <- execWriterT $ do + for_ wanteds $ \wanted -> do + -- wanted => ... + for_ (asDecomposedConstraint wanted) $ \types -> do + -- C a b c => ... + + -- C a b c + let typeTerms = fmap toTypeTerm types + let predType = fromDecomposeConstraint types + + for_ (applyRules typeSubst rules typeTerms) $ \(rule, typeTerms') -> do + -- C a' b' c' + let types' = fmap fromTypeTerm typeTerms' + let predType' = fromDecomposeConstraint types' + + unless (eqType predType' predType) $ do + -- co :: C a' b' c' ~R C a b c + let co = mkUnivCo + (PluginProv "TypeLevel.Rewrite") + Representational + predType' + predType + evWanted' <- lift $ newRuleInducedWanted wanted rule predType' + let wanted' = mkNonCanonical evWanted' + let futureDict :: EvExpr + futureDict = ctEvExpr evWanted' + let replaceCt :: ReplaceCt + replaceCt = ReplaceCt + { evidenceOfCorrectness = evCast futureDict co + , replacedConstraint = wanted + , replacementConstraints = [wanted'] + } + tell [replaceCt] + pure $ combineReplaceCts replaceCts diff --git a/src/TypeLevel/Rewrite/Internal/Lookup.hs b/src/TypeLevel/Rewrite/Internal/Lookup.hs index e5708ea..d522a84 100644 --- a/src/TypeLevel/Rewrite/Internal/Lookup.hs +++ b/src/TypeLevel/Rewrite/Internal/Lookup.hs @@ -30,13 +30,21 @@ import TcPluginM import TcSMonad (getDynFlags) #endif +#if MIN_VERSION_ghc(9,6,0) +import GHC.Types.PkgQual (PkgQual(..)) +#endif + lookupModule :: String -- ^ module name -> TcPluginM Module lookupModule moduleNameStr = do let moduleName :: ModuleName moduleName = mkModuleName moduleNameStr +#if MIN_VERSION_ghc(9,6,0) + findImportedModule moduleName NoPkgQual >>= \case +#else findImportedModule moduleName Nothing >>= \case +#endif Found _ module_ -> do pure module_ findResult -> do diff --git a/src/TypeLevel/Rewrite/Internal/TypeEq.hs b/src/TypeLevel/Rewrite/Internal/TypeEq.hs index 53d2df5..4ad8f65 100644 --- a/src/TypeLevel/Rewrite/Internal/TypeEq.hs +++ b/src/TypeLevel/Rewrite/Internal/TypeEq.hs @@ -2,6 +2,9 @@ module TypeLevel.Rewrite.Internal.TypeEq where import Data.Function +#if MIN_VERSION_ghc(9,6,0) +import GHC.Plugins (Type) +import GHC.Tc.Utils.TcType (eqType) #if MIN_VERSION_ghc(9,0,0) import GHC.Plugins (Type, eqType) #else