diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,2 +1,5 @@ +# effectful-plugin-1.1.0.0 (2023-01-23) +* Add support for GHC 9.4 and 9.6. + # effectful-plugin-1.0.0.0 (2022-07-13) * Initial release. diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -15,7 +15,7 @@ The following code: ```haskell -action :: [State Int, State String] :>> es => Eff es () +action :: (State Int :> es, State String :> es) => Eff es () action = do x <- get put (x + 1) @@ -26,7 +26,7 @@ polymorphic. You have to write: ```haskell -action :: [State Int, State String] :>> es => Eff es () +action :: (State Int :> es, State String :> es) => Eff es () action = do x <- get @Int put (x + 1) diff --git a/effectful-plugin.cabal b/effectful-plugin.cabal --- a/effectful-plugin.cabal +++ b/effectful-plugin.cabal @@ -1,7 +1,7 @@ cabal-version: 2.4 build-type: Simple name: effectful-plugin -version: 1.0.0.0 +version: 1.1.0.0 license: BSD-3-Clause license-file: LICENSE category: Control @@ -9,14 +9,15 @@ author: Andrzej Rybczak synopsis: A GHC plugin for improving disambiguation of effects. -description: Instruct GHC to do a better job with disambiguation of effects. - . - See the README for more information. +description: + Instruct GHC to do a better job with disambiguation of effects. + . + See the README for more information. extra-source-files: CHANGELOG.md README.md -tested-with: GHC ==8.8.4 || ==8.10.7 || ==9.0.2 || ==9.2.3 +tested-with: GHC ==8.8.4 || ==8.10.7 || ==9.0.2 || ==9.2.5 || ==9.4.4 bug-reports: https://github.com/haskell-effectful/effectful/issues source-repository head @@ -26,10 +27,6 @@ common language ghc-options: -Wall -Wcompat -Wno-unticked-promoted-constructors - -- The plugin doesn't build with GHC 9.4 yet. - if !impl(ghc < 9.3) - buildable: False - default-language: Haskell2010 default-extensions: BangPatterns @@ -58,15 +55,19 @@ import: language build-depends: base >= 4.13 && < 5 - , effectful-core >= 1.0.0.0 && < 1.0.1.0 + , effectful-core >= 1.0.0.0 && < 3.0.0.0 , containers >= 0.5 - , ghc >= 8.6 && < 9.3 - , ghc-tcplugins-extra >= 0.3 && < 0.5 + , ghc >= 8.6 && < 9.7 - hs-source-dirs: src + if impl(ghc < 9.4) + build-depends: ghc-tcplugins-extra >= 0.3 && < 0.5 + if impl(ghc < 9.4) + hs-source-dirs: src-legacy + else + hs-source-dirs: src + exposed-modules: Effectful.Plugin - Effectful.Plugin.Internal test-suite plugin-tests import: language diff --git a/src-legacy/Effectful/Plugin.hs b/src-legacy/Effectful/Plugin.hs new file mode 100644 --- /dev/null +++ b/src-legacy/Effectful/Plugin.hs @@ -0,0 +1,241 @@ +{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE CPP #-} +module Effectful.Plugin (plugin) where + +import Data.Function (on) +import Data.IORef (IORef, modifyIORef, newIORef, readIORef) +import Data.Maybe (isNothing, mapMaybe) +import Data.Set (Set) +import qualified Data.Set as Set +import Data.Traversable (for) +import GHC.TcPluginM.Extra (lookupModule, lookupName) + +#if __GLASGOW_HASKELL__ >= 900 +import GHC.Core.Class (Class) +import GHC.Core.InstEnv (InstEnvs, lookupInstEnv) +import GHC.Core.Unify (tcUnifyTy) +import GHC.Plugins (Outputable (ppr), Plugin (pluginRecompile, tcPlugin), PredType, + Role (Nominal), TCvSubst, Type, defaultPlugin, eqType, fsLit, mkModuleName, + mkTcOcc, nonDetCmpType, purePlugin, showSDocUnsafe, splitAppTys, substTys, + tyConClass_maybe) +import GHC.Tc.Plugin (tcLookupClass, tcPluginIO) +import GHC.Tc.Solver.Monad (newWantedEq, runTcSDeriveds) +import GHC.Tc.Types (TcM, TcPlugin (TcPlugin, tcPluginInit, tcPluginSolve, tcPluginStop), + TcPluginM, TcPluginResult (TcPluginOk), unsafeTcPluginTcM) +import GHC.Tc.Types.Constraint (Ct (CDictCan, CNonCanonical), CtEvidence (CtWanted), CtLoc, ctPred) +import GHC.Tc.Utils.Env (tcGetInstEnvs) +import GHC.Tc.Utils.TcType (tcSplitTyConApp) + +#else +import Class (Class) +#if __GLASGOW_HASKELL__ >= 810 +import Constraint (Ct (CDictCan, CNonCanonical), CtEvidence (CtWanted), CtLoc, ctPred) +#endif +import GhcPlugins (Outputable (ppr), Plugin (pluginRecompile, tcPlugin), PredType, + Role (Nominal), TCvSubst, Type, defaultPlugin, eqType, fsLit, mkModuleName, + mkTcOcc, nonDetCmpType, purePlugin, showSDocUnsafe, splitAppTys, substTys, + tyConClass_maybe) +import InstEnv (InstEnvs, lookupInstEnv) +import TcEnv (tcGetInstEnvs) +import TcPluginM (tcLookupClass, tcPluginIO) +import TcRnTypes +import TcSMonad (newWantedEq, runTcSDeriveds) +import TcType (tcSplitTyConApp) +import Unify (tcUnifyTy) +#endif + +plugin :: Plugin +plugin = makePlugin [("effectful", "Effectful.Internal.Effect", ":>")] + +-- | A list of unique, unambiguous Haskell names in the format of @(packageName, moduleName, identifier)@. +type Names = [(String, String, String)] + +-- | Make a @polysemy-plugin@-style effect disambiguation plugin that applies to all the "element-of" typeclasses +-- passed in. Each of the names passed in should have type @k -> [k] -> 'Data.Kind.Type'@ where @k@ can be either +-- polymorphic or monomorphic. +-- +-- Some examples include: +-- +-- @ +-- (\"cleff\", \"Cleff.Internal.Rec\", \":>\") +-- (\"polysemy\", \"Polysemy.Internal.Union\", \"Member\") +-- (\"effectful\", \"Effectful.Internal.Effect\", \":>\") +-- @ +-- +-- You can see the source code for notes on the implementation of the plugin. +makePlugin :: Names -> Plugin +makePlugin names = defaultPlugin + { tcPlugin = const (Just $ fakedep names) + , pluginRecompile = purePlugin + } + +fakedep :: Names -> TcPlugin +fakedep names = TcPlugin + { tcPluginInit = initFakedep names + , tcPluginSolve = solveFakedepForAllElemClasses + , tcPluginStop = const $ pure () + } + +liftTc :: TcM a -> TcPluginM a +liftTc = unsafeTcPluginTcM + +liftIo :: IO a -> TcPluginM a +liftIo = tcPluginIO +type VisitedSet = Set (OrdType, OrdType) + +initFakedep :: Names -> TcPluginM ([Class], IORef VisitedSet) +initFakedep names = do + classes <- for names \(packageName, elemModuleName, elemClassName) -> do + recMod <- lookupModule (mkModuleName elemModuleName) $ fsLit packageName + nm <- lookupName recMod $ mkTcOcc elemClassName + tcLookupClass nm + visited <- liftIo $ newIORef Set.empty + pure (classes, visited) + +data FakedepGiven = FakedepGiven + { givenEffHead :: Type + , givenEff :: Type + , givenEs :: Type + } + +instance Show FakedepGiven where + show (FakedepGiven _ e es) = "(Elem " <> showSDocUnsafe (ppr e) <> " " <> showSDocUnsafe (ppr es) <> ")" + +data FakedepWanted = FakedepWanted FakedepGiven CtLoc + +instance Show FakedepWanted where + show (FakedepWanted given _) = show given + +newtype OrdType = OrdType { unOrdType :: Type } + +instance Eq OrdType where + (==) = eqType `on` unOrdType + +instance Ord OrdType where + compare = nonDetCmpType `on` unOrdType + +solveFakedepForAllElemClasses :: ([Class], IORef VisitedSet) -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult +solveFakedepForAllElemClasses (elemClasses, visitedRef) givens _ wanteds = do + solns <- concat <$> for elemClasses \elemCls -> solveFakedep (elemCls, visitedRef) givens wanteds + pure $ TcPluginOk [] solns + +solveFakedep :: (Class, IORef VisitedSet) -> [Ct] -> [Ct] -> TcPluginM [Ct] +solveFakedep _ _ [] = pure [] +solveFakedep (elemCls, visitedRef) allGivens allWanteds = do + -- We're given two lists of constraints here: + -- - 'allGivens' are constraints already in our context, + -- - 'allWanteds' are constraints that need to be solved. + -- In the following notes, the words "give/given" and "want/wanted" all refer to this specific technical concept: + -- given constraints are those that we can use, and wanted constraints are those that we need to solve. + let + -- The only type of constraint we're interested in solving are 'Elem e es' constraints. Therefore, we extract these + -- constraints out of the 'allGivens' and 'allWanted's. + givens = mapMaybe relevantGiven allGivens + wanteds = mapMaybe relevantWanted allWanteds + -- We store a list of the types of all given constraints, which will be useful later. + allGivenTypes = ctPred <$> allGivens + -- We also store a list of wanted constraints that are /not/ 'Elem e es' for later use. + extraWanteds = ctPred <$> filter irrelevant allWanteds + + -- traceM $ "Givens: " <> show (showSDocUnsafe . ppr <$> allGivens) + -- traceM $ "Wanteds: " <> show (showSDocUnsafe . ppr <$> allWanteds) + + -- For each 'Elem e es' we /want/ to solve (the "goal"), we need to eventually correspond it to another unique + -- /given/ 'Elem e es' that will make the program typecheck (the "solution"). + globals <- liftTc tcGetInstEnvs -- Get the global instances environment for later use + let solns = mapMaybe (solve globals allGivenTypes extraWanteds givens) wanteds + + -- Now we need to tell GHC the solutions. The way we do this is to generate a new equality constraint, like + -- 'Elem (State e) es ~ Elem (State Int) es', so that GHC's constraint solver will know that 'e' must be 'Int'. + eqns <- for solns \(FakedepWanted (FakedepGiven _ goalEff _) loc, FakedepGiven _ solnEff _) -> do + (eqn, _) <- liftTc $ runTcSDeriveds $ newWantedEq loc Nominal goalEff solnEff + pure (CNonCanonical eqn, (OrdType goalEff, OrdType solnEff)) + + -- For any solution we've generated, we need to be careful not to generate it again, or we might end up generating + -- infinitely many solutions. So, we record any already generated solution in a set. + visitedSolnPairs <- liftIo $ readIORef visitedRef + let solnEqns = fst <$> flip filter eqns \(_, pair) -> Set.notMember pair visitedSolnPairs + liftIo $ modifyIORef visitedRef (Set.union $ Set.fromList $ snd <$> eqns) + + -- traceM $ "Emitting: " <> showSDocUnsafe (ppr solnEqns) + pure solnEqns -- Finally we tell GHC the solutions. + + where + + -- Determine if there is a unique solution to a goal from a set of candidates. + solve :: InstEnvs -> [PredType] -> [PredType] -> [FakedepGiven] -> FakedepWanted -> Maybe (FakedepWanted, FakedepGiven) + solve globals allGivenTypes extraWanteds givens goal@(FakedepWanted (FakedepGiven _ _ goalEs) _) = + let + -- Apart from 'Elem' constraints in the context, the effects already hardwired into the effect stack type, + -- like those in 'A : B : C : es', also need to be considered. So here we extract that for them to be considered + -- simultaneously with regular 'Elem' constraints. + cands = extractExtraGivens goalEs goalEs <> givens + -- The first criteria is that the candidate constraint must /unify/ with the goal. This means that the type + -- variables in the goal can be instantiated in a way so that the goal becomes equal to the candidate. + -- For example, the candidates 'Elem (State Int) es' and 'Elem (State String) es' both unify with the goal + -- 'Elem (State s) es'. + unifiableCands = mapMaybe (unifiableWith goal) cands + in case unifiableCands of + -- If there's already only one unique solution, commit to it; in the worst case where it doesn't actually match, + -- we get a cleaner error message like "Unable to match (State String) to (State Int)" instead of a type + -- ambiguity error. + [(soln, _)] -> Just (goal, soln) + _ -> + -- Otherwise, the second criteria comes in: the candidate must satisfy all other constraints we /want/ to solve. + -- For example, when we want to solve '(Elem (State a) es, Num a)`, the candidate 'Elem (State Int) es' will do + -- the job, because it satisfied 'Num a'; however 'Elem (State String) es' will be excluded. + let satisfiableCands = filter (satisfiable globals allGivenTypes extraWanteds) unifiableCands + -- Finally, if there is a unique candidate remaining, we use it as the solution; otherwise we don't solve anything. + in case satisfiableCands of + [(soln, _)] -> Just (goal, soln) + _ -> Nothing + + -- Extract the heads of a type like 'A : B : C : es' into 'FakedepGiven's. + extractExtraGivens :: Type -> Type -> [FakedepGiven] + extractExtraGivens fullEs es = case splitAppTys es of + (_colon, [_kind, e, es']) -> + let (dtHead, _tyArgs) = splitAppTys e + in FakedepGiven dtHead e fullEs : extractExtraGivens fullEs es' + _ -> [] + + -- Determine whether a given constraint is of form 'Elem e es'. + relevantGiven :: Ct -> Maybe FakedepGiven + relevantGiven (CDictCan _ cls [_kind, eff, es] _) -- Polymorphic case + | cls == elemCls = Just $ FakedepGiven (fst $ splitAppTys eff) eff es + relevantGiven (CDictCan _ cls [eff, es] _) -- Monomorphic case + | cls == elemCls = Just $ FakedepGiven (fst $ splitAppTys eff) eff es + relevantGiven _ = Nothing + + -- Determine whether a wanted constraint is of form 'Elem e es'. + relevantWanted :: Ct -> Maybe FakedepWanted + relevantWanted (CDictCan (CtWanted _ _ _ loc) cls [_kind, eff, es] _) -- Polymorphic case + | cls == elemCls = Just $ FakedepWanted (FakedepGiven (fst $ splitAppTys eff) eff es) loc + relevantWanted (CDictCan (CtWanted _ _ _ loc) cls [eff, es] _) -- Monomorphic case + | cls == elemCls = Just $ FakedepWanted (FakedepGiven (fst $ splitAppTys eff) eff es) loc + relevantWanted _ = Nothing + + -- Determine whether a constraint is /not/ of form 'Elem e es'. + irrelevant :: Ct -> Bool + irrelevant = isNothing . relevantGiven + + -- Given a wanted constraint and a given constraint, unify them and give back a substitution that can be applied + -- to the wanted to make it equal to the given. + unifiableWith :: FakedepWanted -> FakedepGiven -> Maybe (FakedepGiven, TCvSubst) + unifiableWith (FakedepWanted goal _) cand = + -- First, the 'es' type must be equal, and the datatype head of the effect must be equal too. + if givenEs goal `eqType` givenEs cand && givenEffHead goal `eqType` givenEffHead cand + then (cand, ) <$> tcUnifyTy (givenEff goal) (givenEff cand) -- Then the effect type must unify. + else Nothing + + -- Check whether a candidate can satisfy all tthe wanted constraints. + satisfiable :: InstEnvs -> [PredType] -> [PredType] -> (FakedepGiven, TCvSubst) -> Bool + satisfiable globals givens wanteds (_, subst) = + let + wantedsInst = substTys subst wanteds -- The wanteds after unification. + givensInst = Set.fromList $ OrdType <$> substTys subst givens -- The local given context after unification. + in flip all wantedsInst \want -> + if Set.member (OrdType want) givensInst then True -- Can we find this constraint in our local context? + else let (con, args) = tcSplitTyConApp want + in case tyConClass_maybe con of -- If not, lookup the global environment. + Nothing -> False + Just cls -> let (res, _, _) = lookupInstEnv False globals cls args in not $ null res diff --git a/src/Effectful/Plugin.hs b/src/Effectful/Plugin.hs --- a/src/Effectful/Plugin.hs +++ b/src/Effectful/Plugin.hs @@ -1,6 +1,280 @@ +{-# LANGUAGE CPP #-} module Effectful.Plugin (plugin) where -import Effectful.Plugin.Internal (Plugin, makePlugin) +import Data.Either +import Data.Function +import Data.IORef +import Data.Maybe +import Data.Set (Set) +import Data.Traversable +import qualified Data.Set as Set +import GHC.Core.Class (Class) +import GHC.Core.InstEnv (InstEnvs, lookupInstEnv) +import GHC.Core.TyCo.Rep (PredType, Type) +import GHC.Core.TyCo.Subst +import GHC.Core.TyCon (tyConClass_maybe) +import GHC.Core.Type (splitAppTys) +import GHC.Core.Unify (tcUnifyTy) +import GHC.Driver.Config.Finder (initFinderOpts) +import GHC.Driver.Env (hsc_home_unit, hsc_units) +import GHC.Driver.Env.Types (HscEnv (..)) +import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin) +import GHC.Tc.Plugin (getTopEnv, lookupOrig, tcLookupClass, tcPluginIO) +import GHC.Tc.Solver.Monad (newWantedEq, runTcSEarlyAbort) +import GHC.Tc.Types + ( TcPlugin (..) + , TcPluginM + , TcPluginSolveResult (..) + , unsafeTcPluginTcM + ) +import GHC.Tc.Types.Constraint + ( Ct (..) + , CtEvidence (..) + , CtLoc + , ctPred + , emptyRewriterSet + ) +import GHC.Tc.Types.Evidence (EvBindsVar, Role (..)) +import GHC.Tc.Utils.Env (tcGetInstEnvs) +import GHC.Tc.Utils.TcType (tcSplitTyConApp, eqType, nonDetCmpType) +import GHC.Types.Name (mkTcOcc) +import GHC.Types.Unique.FM (emptyUFM) +import GHC.Unit.Finder (FindResult (..), findPluginModule) +import GHC.Unit.Module (Module, ModuleName, mkModuleName) +import GHC.Utils.Outputable (Outputable (..), showSDocUnsafe) +import GHC.Utils.Panic (panicDoc) + +#if __GLASGOW_HASKELL__ >= 906 +type TCvSubst = Subst +#endif + plugin :: Plugin -plugin = makePlugin [("effectful", "Effectful.Internal.Effect", ":>")] +plugin = defaultPlugin + { tcPlugin = \_ -> Just TcPlugin + { tcPluginInit = initPlugin "Effectful.Internal.Effect" ":>" + , tcPluginRewrite = \_ -> emptyUFM + , tcPluginSolve = solveFakedep + , tcPluginStop = \_ -> pure () + } + , pluginRecompile = purePlugin + } + +---------------------------------------- + +data EffGiven = EffGiven + { givenEffHead :: Type + , givenEff :: Type + , givenEs :: Type + } + +instance Show EffGiven where + show (EffGiven _ e es) = + "[G] " ++ showSDocUnsafe (ppr e) <> " :> " <> showSDocUnsafe (ppr es) + +data EffWanted = EffWanted + { wantedEffHead :: Type + , wantedEff :: Type + , wantedEs :: Type + , wantedLoc :: CtLoc + } + +instance Show EffWanted where + show (EffWanted _ e es _) = + "[W] " <> showSDocUnsafe (ppr e) <> " :> " <> showSDocUnsafe (ppr es) + +newtype OrdType = OrdType {unOrdType :: Type} + +instance Eq OrdType where + (==) = eqType `on` unOrdType + +instance Ord OrdType where + compare = nonDetCmpType `on` unOrdType + +---------------------------------------- + +type VisitedSet = Set (OrdType, OrdType) + +initPlugin :: String -> String -> TcPluginM (Class, IORef VisitedSet) +initPlugin modName clsName = do + recMod <- lookupModule (mkModuleName modName) + cls <- tcLookupClass =<< lookupOrig recMod (mkTcOcc clsName) + visited <- tcPluginIO $ newIORef Set.empty + pure (cls, visited) + where + lookupModule :: ModuleName -> TcPluginM Module + lookupModule mod_nm = do + hsc_env <- getTopEnv + let dflags = hsc_dflags hsc_env + fopts = initFinderOpts dflags + fc = hsc_FC hsc_env + units = hsc_units hsc_env + home_unit = hsc_home_unit hsc_env + tcPluginIO (findPluginModule fc fopts units (Just home_unit) mod_nm) >>= \case + Found _ md -> pure md + _ -> panicDoc "Couldn't find module" (ppr mod_nm) + + +solveFakedep + :: (Class, IORef VisitedSet) + -> EvBindsVar + -> [Ct] + -> [Ct] + -> TcPluginM TcPluginSolveResult +solveFakedep (elemCls, visitedRef) _ allGivens allWanteds = do + -- We're given two lists of constraints here: + -- + -- - 'allGivens' are constraints already in our context, + -- + -- - 'allWanteds' are constraints that need to be solved. + -- + -- In the following notes, the words "give/given" and "want/wanted" all refer + -- to this specific technical concept: given constraints are those that we can + -- use, and wanted constraints are those that we need to solve. + + --tcPluginIO $ do + -- putStrLn $ "Givens: " <> show (showSDocUnsafe . ppr <$> allGivens) + -- putStrLn $ "Wanteds: " <> show (showSDocUnsafe . ppr <$> allWanteds) + + -- For each 'e :> es' we /want/ to solve (the "goal"), we need to eventually + -- correspond it to another unique /given/ 'e :> es' that will make the + -- program typecheck (the "solution"). + globals <- unsafeTcPluginTcM tcGetInstEnvs + let solns = mapMaybe (solve globals) effWanteds + + -- Now we need to tell GHC the solutions. The way we do this is to generate a + -- new equality constraint, like 'State e ~ State Int', so that GHC's + -- constraint solver will know that 'e' must be 'Int'. + eqns <- for solns $ \(goal, soln) -> do + let wantedEq = newWantedEq (wantedLoc goal) emptyRewriterSet Nominal + (wantedEff goal) (givenEff soln) + (eqn, _) <- unsafeTcPluginTcM $ runTcSEarlyAbort wantedEq + pure (CNonCanonical eqn, (OrdType $ wantedEff goal, OrdType $ givenEff soln)) + + -- For any solution we've generated, we need to be careful not to generate it + -- again, or we might end up generating infinitely many solutions. So, we + -- record any already generated solution in a set. + visitedSolnPairs <- tcPluginIO $ readIORef visitedRef + let solnEqns = fmap fst . flip filter eqns $ \(_, pair) -> Set.notMember pair visitedSolnPairs + tcPluginIO $ do + modifyIORef visitedRef (Set.union $ Set.fromList $ map snd eqns) + --putStrLn $ "Emitting: " <> showSDocUnsafe (ppr solnEqns) + + pure $ TcPluginSolveResult [] [] solnEqns + where + -- The only type of constraint we're interested in solving are 'e :> es' + -- constraints. Therefore, we extract these constraints out of the + -- 'allGivens' and 'allWanted's. + effGivens = mapMaybe maybeEffGiven allGivens + (otherWantedTys, effWanteds) = partitionEithers $ map splitWanteds allWanteds + + -- We store a list of the types of all given constraints, which will be + -- useful later. + allGivenTys = ctPred <$> allGivens + + -- Determine if there is a unique solution to a goal from a set of + -- candidates. + solve + :: InstEnvs + -> EffWanted + -> Maybe (EffWanted, EffGiven) + solve globals goal = case unifiableCands of + -- If there's already only one unique solution, commit to it; in the worst + -- case where it doesn't actually match, we get a cleaner error message + -- like "Unable to match (State String) to (State Int)" instead of a type + -- ambiguity error. + [(soln, _)] -> Just (goal, soln) + _ -> + -- Otherwise, the second criteria comes in: the candidate must satisfy + -- all other constraints we /want/ to solve. For example, when we want + -- to solve '(State a :> es, Num a)`, the candidate 'State Int :> es' + -- will do the job, because it satisfied 'Num a'; however 'State String + -- :> es' will be excluded. + let satisfiableCands = filter (satisfiable globals) unifiableCands + in -- Finally, if there is a unique candidate remaining, we use it as + -- the solution; otherwise we don't solve anything. + case satisfiableCands of + [(soln, _)] -> Just (goal, soln) + _ -> Nothing + where + -- Apart from ':>' constraints in the context, the effects already + -- hardwired into the effect stack type, like those in 'A : B : C : es' + -- also need to be considered. So here we extract that for them to be + -- considered simultaneously with regular ':>' constraints. + cands = extractExtraGivens (wantedEs goal) (wantedEs goal) <> effGivens + -- The first criteria is that the candidate constraint must /unify/ with + -- the goal. This means that the type variables in the goal can be + -- instantiated in a way so that the goal becomes equal to the + -- candidate. For example, the candidates 'State Int :> es' and 'State + -- String :> es' both unify with the goal 'State s :> es'. + unifiableCands = mapMaybe (unifiableWith goal) cands + + -- Extract the heads of a type like 'A : B : C : es' into 'FakedepGiven's. + extractExtraGivens :: Type -> Type -> [EffGiven] + extractExtraGivens fullEs es = case splitAppTys es of + (_colon, [_kind, e, es']) -> + let (dtHead, _tyArgs) = splitAppTys e + in EffGiven { givenEffHead = dtHead + , givenEff = e + , givenEs = fullEs + } : extractExtraGivens fullEs es' + _ -> [] + + -- Determine whether a given constraint is of form 'e :> es'. + maybeEffGiven :: Ct -> Maybe EffGiven + maybeEffGiven = \case + CDictCan { cc_class = cls + , cc_tyargs = [eff, es] + } -> + if cls == elemCls + then Just EffGiven { givenEffHead = fst $ splitAppTys eff + , givenEff = eff + , givenEs = es + } + else Nothing + _ -> Nothing + + -- Determine whether a wanted constraint is of form 'e :> es'. + splitWanteds :: Ct -> Either PredType EffWanted + splitWanteds = \case + ct@CDictCan { cc_ev = CtWanted { ctev_loc = loc } + , cc_class = cls + , cc_tyargs = [eff, es] + } -> + if cls == elemCls + then Right EffWanted { wantedEffHead = fst $ splitAppTys eff + , wantedEff = eff + , wantedEs = es + , wantedLoc = loc + } + else Left $ ctPred ct + ct -> Left $ ctPred ct + + -- Given a wanted constraint and a given constraint, unify them and give + -- back a substitution that can be applied to the wanted to make it equal to + -- the given. + unifiableWith :: EffWanted -> EffGiven -> Maybe (EffGiven, TCvSubst) + unifiableWith goal cand = + if wantedEs goal `eqType` givenEs cand + && wantedEffHead goal `eqType` givenEffHead cand + then (cand, ) <$> tcUnifyTy (wantedEff goal) (givenEff cand) + else Nothing + + -- Check whether a candidate can satisfy all the wanted constraints. + satisfiable :: InstEnvs -> (EffGiven, TCvSubst) -> Bool + satisfiable globals (_, subst) = flip all wantedsInst $ \wanted -> + if Set.member (OrdType wanted) givensInst + then True -- Can we find this constraint in our local context? + else case tcSplitTyConApp wanted of + (con, args) -> + -- If not, lookup the global environment. + case tyConClass_maybe con of + Nothing -> False + Just cls -> + let (res, _, _) = lookupInstEnv False globals cls args + in not $ null res + where + -- The wanteds after unification. + wantedsInst = substTys subst otherWantedTys + -- The local given context after unification. + givensInst = Set.fromList (OrdType <$> substTys subst allGivenTys) diff --git a/src/Effectful/Plugin/Internal.hs b/src/Effectful/Plugin/Internal.hs deleted file mode 100644 --- a/src/Effectful/Plugin/Internal.hs +++ /dev/null @@ -1,238 +0,0 @@ -{-# LANGUAGE BlockArguments #-} -{-# LANGUAGE CPP #-} -module Effectful.Plugin.Internal (Plugin, Names, makePlugin) where - -import Data.Function (on) -import Data.IORef (IORef, modifyIORef, newIORef, readIORef) -import Data.Maybe (isNothing, mapMaybe) -import Data.Set (Set) -import qualified Data.Set as Set -import Data.Traversable (for) -import GHC.TcPluginM.Extra (lookupModule, lookupName) - -#if __GLASGOW_HASKELL__ >= 900 -import GHC.Core.Class (Class) -import GHC.Core.InstEnv (InstEnvs, lookupInstEnv) -import GHC.Core.Unify (tcUnifyTy) -import GHC.Plugins (Outputable (ppr), Plugin (pluginRecompile, tcPlugin), PredType, - Role (Nominal), TCvSubst, Type, defaultPlugin, eqType, fsLit, mkModuleName, - mkTcOcc, nonDetCmpType, purePlugin, showSDocUnsafe, splitAppTys, substTys, - tyConClass_maybe) -import GHC.Tc.Plugin (tcLookupClass, tcPluginIO) -import GHC.Tc.Solver.Monad (newWantedEq, runTcSDeriveds) -import GHC.Tc.Types (TcM, TcPlugin (TcPlugin, tcPluginInit, tcPluginSolve, tcPluginStop), - TcPluginM, TcPluginResult (TcPluginOk), unsafeTcPluginTcM) -import GHC.Tc.Types.Constraint (Ct (CDictCan, CNonCanonical), CtEvidence (CtWanted), CtLoc, ctPred) -import GHC.Tc.Utils.Env (tcGetInstEnvs) -import GHC.Tc.Utils.TcType (tcSplitTyConApp) - -#else -import Class (Class) -#if __GLASGOW_HASKELL__ >= 810 -import Constraint (Ct (CDictCan, CNonCanonical), CtEvidence (CtWanted), CtLoc, ctPred) -#endif -import GhcPlugins (Outputable (ppr), Plugin (pluginRecompile, tcPlugin), PredType, - Role (Nominal), TCvSubst, Type, defaultPlugin, eqType, fsLit, mkModuleName, - mkTcOcc, nonDetCmpType, purePlugin, showSDocUnsafe, splitAppTys, substTys, - tyConClass_maybe) -import InstEnv (InstEnvs, lookupInstEnv) -import TcEnv (tcGetInstEnvs) -import TcPluginM (tcLookupClass, tcPluginIO) -import TcRnTypes -import TcSMonad (newWantedEq, runTcSDeriveds) -import TcType (tcSplitTyConApp) -import Unify (tcUnifyTy) -#endif - --- | A list of unique, unambiguous Haskell names in the format of @(packageName, moduleName, identifier)@. -type Names = [(String, String, String)] - --- | Make a @polysemy-plugin@-style effect disambiguation plugin that applies to all the "element-of" typeclasses --- passed in. Each of the names passed in should have type @k -> [k] -> 'Data.Kind.Type'@ where @k@ can be either --- polymorphic or monomorphic. --- --- Some examples include: --- --- @ --- (\"cleff\", \"Cleff.Internal.Rec\", \":>\") --- (\"polysemy\", \"Polysemy.Internal.Union\", \"Member\") --- (\"effectful\", \"Effectful.Internal.Effect\", \":>\") --- @ --- --- You can see the source code for notes on the implementation of the plugin. -makePlugin :: Names -> Plugin -makePlugin names = defaultPlugin - { tcPlugin = const (Just $ fakedep names) - , pluginRecompile = purePlugin - } - -fakedep :: Names -> TcPlugin -fakedep names = TcPlugin - { tcPluginInit = initFakedep names - , tcPluginSolve = solveFakedepForAllElemClasses - , tcPluginStop = const $ pure () - } - -liftTc :: TcM a -> TcPluginM a -liftTc = unsafeTcPluginTcM - -liftIo :: IO a -> TcPluginM a -liftIo = tcPluginIO -type VisitedSet = Set (OrdType, OrdType) - -initFakedep :: Names -> TcPluginM ([Class], IORef VisitedSet) -initFakedep names = do - classes <- for names \(packageName, elemModuleName, elemClassName) -> do - recMod <- lookupModule (mkModuleName elemModuleName) $ fsLit packageName - nm <- lookupName recMod $ mkTcOcc elemClassName - tcLookupClass nm - visited <- liftIo $ newIORef Set.empty - pure (classes, visited) - -data FakedepGiven = FakedepGiven - { givenEffHead :: Type - , givenEff :: Type - , givenEs :: Type - } - -instance Show FakedepGiven where - show (FakedepGiven _ e es) = "(Elem " <> showSDocUnsafe (ppr e) <> " " <> showSDocUnsafe (ppr es) <> ")" - -data FakedepWanted = FakedepWanted FakedepGiven CtLoc - -instance Show FakedepWanted where - show (FakedepWanted given _) = show given - -newtype OrdType = OrdType { unOrdType :: Type } - -instance Eq OrdType where - (==) = eqType `on` unOrdType - -instance Ord OrdType where - compare = nonDetCmpType `on` unOrdType - -solveFakedepForAllElemClasses :: ([Class], IORef VisitedSet) -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult -solveFakedepForAllElemClasses (elemClasses, visitedRef) givens _ wanteds = do - solns <- concat <$> for elemClasses \elemCls -> solveFakedep (elemCls, visitedRef) givens wanteds - pure $ TcPluginOk [] solns - -solveFakedep :: (Class, IORef VisitedSet) -> [Ct] -> [Ct] -> TcPluginM [Ct] -solveFakedep _ _ [] = pure [] -solveFakedep (elemCls, visitedRef) allGivens allWanteds = do - -- We're given two lists of constraints here: - -- - 'allGivens' are constraints already in our context, - -- - 'allWanteds' are constraints that need to be solved. - -- In the following notes, the words "give/given" and "want/wanted" all refer to this specific technical concept: - -- given constraints are those that we can use, and wanted constraints are those that we need to solve. - let - -- The only type of constraint we're interested in solving are 'Elem e es' constraints. Therefore, we extract these - -- constraints out of the 'allGivens' and 'allWanted's. - givens = mapMaybe relevantGiven allGivens - wanteds = mapMaybe relevantWanted allWanteds - -- We store a list of the types of all given constraints, which will be useful later. - allGivenTypes = ctPred <$> allGivens - -- We also store a list of wanted constraints that are /not/ 'Elem e es' for later use. - extraWanteds = ctPred <$> filter irrelevant allWanteds - - -- traceM $ "Givens: " <> show (showSDocUnsafe . ppr <$> allGivens) - -- traceM $ "Wanteds: " <> show (showSDocUnsafe . ppr <$> allWanteds) - - -- For each 'Elem e es' we /want/ to solve (the "goal"), we need to eventually correspond it to another unique - -- /given/ 'Elem e es' that will make the program typecheck (the "solution"). - globals <- liftTc tcGetInstEnvs -- Get the global instances environment for later use - let solns = mapMaybe (solve globals allGivenTypes extraWanteds givens) wanteds - - -- Now we need to tell GHC the solutions. The way we do this is to generate a new equality constraint, like - -- 'Elem (State e) es ~ Elem (State Int) es', so that GHC's constraint solver will know that 'e' must be 'Int'. - eqns <- for solns \(FakedepWanted (FakedepGiven _ goalEff _) loc, FakedepGiven _ solnEff _) -> do - (eqn, _) <- liftTc $ runTcSDeriveds $ newWantedEq loc Nominal goalEff solnEff - pure (CNonCanonical eqn, (OrdType goalEff, OrdType solnEff)) - - -- For any solution we've generated, we need to be careful not to generate it again, or we might end up generating - -- infinitely many solutions. So, we record any already generated solution in a set. - visitedSolnPairs <- liftIo $ readIORef visitedRef - let solnEqns = fst <$> flip filter eqns \(_, pair) -> Set.notMember pair visitedSolnPairs - liftIo $ modifyIORef visitedRef (Set.union $ Set.fromList $ snd <$> eqns) - - -- traceM $ "Emitting: " <> showSDocUnsafe (ppr solnEqns) - pure solnEqns -- Finally we tell GHC the solutions. - - where - - -- Determine if there is a unique solution to a goal from a set of candidates. - solve :: InstEnvs -> [PredType] -> [PredType] -> [FakedepGiven] -> FakedepWanted -> Maybe (FakedepWanted, FakedepGiven) - solve globals allGivenTypes extraWanteds givens goal@(FakedepWanted (FakedepGiven _ _ goalEs) _) = - let - -- Apart from 'Elem' constraints in the context, the effects already hardwired into the effect stack type, - -- like those in 'A : B : C : es', also need to be considered. So here we extract that for them to be considered - -- simultaneously with regular 'Elem' constraints. - cands = extractExtraGivens goalEs goalEs <> givens - -- The first criteria is that the candidate constraint must /unify/ with the goal. This means that the type - -- variables in the goal can be instantiated in a way so that the goal becomes equal to the candidate. - -- For example, the candidates 'Elem (State Int) es' and 'Elem (State String) es' both unify with the goal - -- 'Elem (State s) es'. - unifiableCands = mapMaybe (unifiableWith goal) cands - in case unifiableCands of - -- If there's already only one unique solution, commit to it; in the worst case where it doesn't actually match, - -- we get a cleaner error message like "Unable to match (State String) to (State Int)" instead of a type - -- ambiguity error. - [(soln, _)] -> Just (goal, soln) - _ -> - -- Otherwise, the second criteria comes in: the candidate must satisfy all other constraints we /want/ to solve. - -- For example, when we want to solve '(Elem (State a) es, Num a)`, the candidate 'Elem (State Int) es' will do - -- the job, because it satisfied 'Num a'; however 'Elem (State String) es' will be excluded. - let satisfiableCands = filter (satisfiable globals allGivenTypes extraWanteds) unifiableCands - -- Finally, if there is a unique candidate remaining, we use it as the solution; otherwise we don't solve anything. - in case satisfiableCands of - [(soln, _)] -> Just (goal, soln) - _ -> Nothing - - -- Extract the heads of a type like 'A : B : C : es' into 'FakedepGiven's. - extractExtraGivens :: Type -> Type -> [FakedepGiven] - extractExtraGivens fullEs es = case splitAppTys es of - (_colon, [_kind, e, es']) -> - let (dtHead, _tyArgs) = splitAppTys e - in FakedepGiven dtHead e fullEs : extractExtraGivens fullEs es' - _ -> [] - - -- Determine whether a given constraint is of form 'Elem e es'. - relevantGiven :: Ct -> Maybe FakedepGiven - relevantGiven (CDictCan _ cls [_kind, eff, es] _) -- Polymorphic case - | cls == elemCls = Just $ FakedepGiven (fst $ splitAppTys eff) eff es - relevantGiven (CDictCan _ cls [eff, es] _) -- Monomorphic case - | cls == elemCls = Just $ FakedepGiven (fst $ splitAppTys eff) eff es - relevantGiven _ = Nothing - - -- Determine whether a wanted constraint is of form 'Elem e es'. - relevantWanted :: Ct -> Maybe FakedepWanted - relevantWanted (CDictCan (CtWanted _ _ _ loc) cls [_kind, eff, es] _) -- Polymorphic case - | cls == elemCls = Just $ FakedepWanted (FakedepGiven (fst $ splitAppTys eff) eff es) loc - relevantWanted (CDictCan (CtWanted _ _ _ loc) cls [eff, es] _) -- Monomorphic case - | cls == elemCls = Just $ FakedepWanted (FakedepGiven (fst $ splitAppTys eff) eff es) loc - relevantWanted _ = Nothing - - -- Determine whether a constraint is /not/ of form 'Elem e es'. - irrelevant :: Ct -> Bool - irrelevant = isNothing . relevantGiven - - -- Given a wanted constraint and a given constraint, unify them and give back a substitution that can be applied - -- to the wanted to make it equal to the given. - unifiableWith :: FakedepWanted -> FakedepGiven -> Maybe (FakedepGiven, TCvSubst) - unifiableWith (FakedepWanted goal _) cand = - -- First, the 'es' type must be equal, and the datatype head of the effect must be equal too. - if givenEs goal `eqType` givenEs cand && givenEffHead goal `eqType` givenEffHead cand - then (cand, ) <$> tcUnifyTy (givenEff goal) (givenEff cand) -- Then the effect type must unify. - else Nothing - - -- Check whether a candidate can satisfy all tthe wanted constraints. - satisfiable :: InstEnvs -> [PredType] -> [PredType] -> (FakedepGiven, TCvSubst) -> Bool - satisfiable globals givens wanteds (_, subst) = - let - wantedsInst = substTys subst wanteds -- The wanteds after unification. - givensInst = Set.fromList $ OrdType <$> substTys subst givens -- The local given context after unification. - in flip all wantedsInst \want -> - if Set.member (OrdType want) givensInst then True -- Can we find this constraint in our local context? - else let (con, args) = tcSplitTyConApp want - in case tyConClass_maybe con of -- If not, lookup the global environment. - Nothing -> False - Just cls -> let (res, _, _) = lookupInstEnv False globals cls args in not $ null res diff --git a/tests/PluginTests.hs b/tests/PluginTests.hs --- a/tests/PluginTests.hs +++ b/tests/PluginTests.hs @@ -28,19 +28,19 @@ instance MPTC Bool Int where mptc _ = 1000 -uniquelyInt :: [State Int, State String] :>> es => Eff es () +uniquelyInt :: (State Int :> es, State String :> es) => Eff es () uniquelyInt = put 10 -uniquelyA :: (Num a, [State a, State b] :>> es) => Eff es () +uniquelyA :: (Num a, State a :> es, State b :> es) => Eff es () uniquelyA = put 10 -uniquelyString :: [State Int, State String] :>> es => Eff es () +uniquelyString :: (State Int :> es, State String :> es) => Eff es () uniquelyString = put mempty -uniquelyB :: (MPTC Bool b, [State String, State b] :>> es) => Eff es () +uniquelyB :: (MPTC Bool b, State String :> es, State b :> es) => Eff es () uniquelyB = put $ mptc False -uniquelyState' :: [Error (), State ()] :>> es => Eff es () +uniquelyState' :: (Error () :> es, State () :> es) => Eff es () uniquelyState' = pure () idState :: State s :> es => Eff es () @@ -66,7 +66,7 @@ (throwError (error "")) (\_ _ -> pure True) -errState :: Num s => [Error e, State s] :>> es => Eff es Bool +errState :: (Num s, Error e :> es, State s :> es) => Eff es Bool errState = do numState err @@ -100,7 +100,7 @@ TaggedGet -> get TaggedPut s' -> put s' -test :: [TaggedState Char Int, TaggedState Bool Int] :>> es => Eff es () +test :: (TaggedState Char Int :> es, TaggedState Bool Int :> es) => Eff es () test = do send $ TaggedPut @Bool 10 send $ TaggedPut @Char (-10)