effectful-plugin 1.1.0.4 → 2.1.0.0
raw patch · 5 files changed
Files
- CHANGELOG.md +14/−0
- effectful-plugin.cabal +25/−13
- src-legacy/Effectful/Plugin.hs +0/−259
- src/Effectful/Plugin.hs +397/−253
- tests/PluginTests.hs +57/−6
CHANGELOG.md view
@@ -1,3 +1,17 @@+# effectful-plugin-2.1.0.0 (2026-04-02)+* Drop support for GHC < 9.6.+* Consider built-in instances when filtering candidates.++# effectful-plugin-2.0.0.1 (2025-08-30)+* Small optimization of checking suitable effects for unification.+* Add `timing` flag for tracking execution time of the plugin.+* Expect wanted constraints that are already solved.++# effectful-plugin-2.0.0.0 (2025-06-09)+* Drop support for GHC < 9.4.+* Fix various bugs and shortcomings.+* Add `verbose` flag for tracing execution of the plugin.+ # effectful-plugin-1.1.0.4 (2024-10-08) * Fix inference in presence of implicit parameters.
effectful-plugin.cabal view
@@ -1,7 +1,7 @@ cabal-version: 3.0 build-type: Simple name: effectful-plugin-version: 1.1.0.4+version: 2.1.0.0 license: BSD-3-Clause license-file: LICENSE category: Control@@ -17,17 +17,24 @@ extra-source-files: CHANGELOG.md README.md -tested-with: GHC == { 8.10.7, 9.0.2, 9.2.8, 9.4.8, 9.6.5, 9.8.2, 9.10.1 }+tested-with: GHC == { 9.6.7, 9.8.4, 9.10.3, 9.12.4, 9.14.1 } bug-reports: https://github.com/haskell-effectful/effectful/issues source-repository head type: git location: https://github.com/haskell-effectful/effectful.git +flag timing+ description: Show timing information+ default: False++flag verbose+ description: Trace plugin execution+ default: False+ common language ghc-options: -Wall -Wcompat- -Wno-unticked-promoted-constructors -Wmissing-deriving-strategies -Werror=prepositive-qualified-module @@ -39,6 +46,7 @@ DeriveFunctor DeriveGeneric DerivingStrategies+ DuplicateRecordFields FlexibleContexts FlexibleInstances GADTs@@ -46,7 +54,9 @@ ImportQualifiedPost LambdaCase MultiParamTypeClasses+ NoFieldSelectors NoStarIsType+ OverloadedRecordDot PolyKinds RankNTypes RecordWildCards@@ -57,27 +67,29 @@ TypeApplications TypeFamilies TypeOperators+ UndecidableInstances library import: language - build-depends: base >= 4.14 && < 5- , effectful-core >= 1.0.0.0 && < 3.0.0.0- , containers >= 0.5- , ghc >= 8.10 && < 9.11+ if flag(timing)+ cpp-options: -DTIMING - if impl(ghc < 9.4)- build-depends: ghc-tcplugins-extra >= 0.3 && < 0.5+ if flag(verbose)+ cpp-options: -DVERBOSE - if impl(ghc < 9.4)- hs-source-dirs: src-legacy- else- hs-source-dirs: src+ build-depends: base >= 4.18 && < 5+ , containers >= 0.5+ , ghc >= 9.6 && < 9.15 + hs-source-dirs: src+ exposed-modules: Effectful.Plugin test-suite plugin-tests import: language++ ghc-options: -fplugin=Effectful.Plugin build-depends: base , effectful-core
− src-legacy/Effectful/Plugin.hs
@@ -1,259 +0,0 @@-{-# 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 Data.Set qualified 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.Predicate (isIPClass)-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 Predicate (isIPClass)-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 (\w -> irrelevant w && not (isIP w)) 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-- -- Check if a constraint in an implicit parameter.- isIP :: Ct -> Bool- isIP = \case- CDictCan _ cls _ _ -> isIPClass cls- _ -> False-- -- Determine whether a constraint is /not/ of form 'Elem e es'.- irrelevant :: Ct -> Bool- irrelevant = isNothing . relevantWanted-- -- 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
src/Effectful/Plugin.hs view
@@ -1,314 +1,458 @@ {-# LANGUAGE CPP #-} module Effectful.Plugin (plugin) where +import Data.Bifunctor+import Data.Coerce import Data.Either-import Data.Function+import Data.Foldable import Data.IORef import Data.Maybe-import Data.Set (Set)-import Data.Set qualified as Set-import Data.Traversable--import GHC.Core.Class (Class)-import GHC.Core.InstEnv (InstEnvs, lookupInstEnv)-import GHC.Core.Predicate (isIPClass)-import GHC.Core.TyCo.Rep (PredType, Type)+import Data.Set qualified as S+import GHC.Core.Class+import GHC.Core.Predicate+import GHC.Core.TyCo.Rep 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.Core.TyCon+import GHC.Core.Type+import GHC.Core.Unify+import GHC.Driver.Env+import GHC.Driver.Plugins+import GHC.Tc.Instance.Class+import GHC.Tc.Plugin import GHC.Tc.Types- ( TcPlugin (..)- , TcPluginM- , TcPluginSolveResult (..)- , unsafeTcPluginTcM- ) import GHC.Tc.Types.Constraint- ( Ct (..)- , CtEvidence (..)-#if __GLASGOW_HASKELL__ < 912- , CtLoc-#endif+import GHC.Tc.Types.Evidence+import GHC.Tc.Utils.TcType+import GHC.Types.Name+import GHC.Types.Unique.FM+import GHC.Types.Unique.Set+import GHC.Types.Var.Set+import GHC.Unit.Finder+import GHC.Unit.Module+import GHC.Utils.Outputable qualified as O+ #if __GLASGOW_HASKELL__ >= 908- , DictCt (..)+import GHC.Driver.DynFlags (DynFlags)+#else+import GHC.Driver.Session (DynFlags) #endif- , ctPred- , emptyRewriterSet- )++#if __GLASGOW_HASKELL__ <= 912+import GHC.Driver.Config.Finder (initFinderOpts)+#endif+ #if __GLASGOW_HASKELL__ >= 912 import GHC.Tc.Types.CtLoc (CtLoc) #endif-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) -#if __GLASGOW_HASKELL__ >= 906-type TCvSubst = Subst+#ifdef TIMING+import GHC.Clock #endif -plugin :: Plugin-plugin = defaultPlugin- { tcPlugin = \_ -> Just TcPlugin- { tcPluginInit = initPlugin- , tcPluginRewrite = \_ -> emptyUFM- , tcPluginSolve = solveFakedep- , tcPluginStop = \_ -> pure ()- }- , pluginRecompile = purePlugin- }------------------------------------------- data EffGiven = EffGiven- { givenEffHead :: Type- , givenEff :: Type- , givenEs :: Type+ { effCon :: Type+ , eff :: Type+ , es :: Type } -instance Show EffGiven where- show (EffGiven _ e es) =- "[G] " ++ showSDocUnsafe (ppr e) <> " :> " <> showSDocUnsafe (ppr es)+instance O.Outputable EffGiven where+ ppr given =+ O.text "[G]" O.<+> O.ppr given.eff O.<+> O.text ":>" O.<+> O.ppr given.es data EffWanted = EffWanted- { wantedEffHead :: Type- , wantedEff :: Type- , wantedEs :: Type- , wantedLoc :: CtLoc+ { effCon :: Type+ , eff :: Type+ , es :: Type+ , loc :: CtLoc } -instance Show EffWanted where- show (EffWanted _ e es _) =- "[W] " <> showSDocUnsafe (ppr e) <> " :> " <> showSDocUnsafe (ppr es)+newtype OtherGiven = OtherGiven+ { ty :: Type+ } -newtype OrdType = OrdType {unOrdType :: Type}+instance O.Outputable OtherGiven where+ ppr given =+ O.text "[G]" O.<+> O.ppr given.ty -instance Eq OrdType where- (==) = eqType `on` unOrdType+instance O.Outputable EffWanted where+ ppr wanted =+ O.text "[W]" O.<+> O.ppr wanted.eff O.<+> O.text ":>" O.<+> O.ppr wanted.es -instance Ord OrdType where- compare = nonDetCmpType `on` unOrdType+data OtherWanted = OtherWanted+ { ty :: Type+ , vars :: TyCoVarSet+ } +instance O.Outputable OtherWanted where+ ppr wanted =+ O.text "[W]" O.<+> O.ppr wanted.ty++data Candidates = None | Single EffGiven | Multiple+ ---------------------------------------- -type VisitedSet = Set (OrdType, OrdType)+data PluginData = PluginData+ { elemClass :: Class+ , totalTime :: !(IORef Double)+ } -initPlugin :: TcPluginM (Class, IORef VisitedSet)+plugin :: Plugin+plugin = defaultPlugin+ { tcPlugin = \_ -> Just TcPlugin+ { tcPluginInit = initPlugin+ , tcPluginRewrite = \_ -> emptyUFM+ , tcPluginSolve = disambiguateEffects+ , tcPluginStop = pluginStopHook+ }+ , pluginRecompile = purePlugin+ }++initPlugin :: TcPluginM PluginData initPlugin = do- recMod <- lookupModule $ mkModuleName "Effectful.Internal.Effect"- cls <- tcLookupClass =<< lookupOrig recMod (mkTcOcc ":>")- visited <- tcPluginIO $ newIORef Set.empty- pure (cls, visited)+ clsMod <- lookupModule $ mkModuleName "Effectful.Internal.Effect"+ elemClass <- tcLookupClass =<< lookupOrig clsMod (mkTcOcc ":>")+ totalTime <- tcPluginIO $ newIORef 0+ pure PluginData{..} 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+ lookupModule modName = do+ hscEnv <- getTopEnv+ findPluginModuleCompat hscEnv modName >>= \case Found _ md -> pure md _ -> errorWithoutStackTrace "Please add effectful-core to the list of dependencies." -solveFakedep- :: (Class, IORef VisitedSet)+disambiguateEffects+ :: PluginData -> 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+disambiguateEffects pd _ allGivens allWanteds = timed pd $ do+ printList "Givens" allGivens+ printList "EffGivens" effGivens+ printList "OtherGivens" otherGivens+ printList "Wanteds" allWanteds+ printList "EffWanteds" effWanteds+ printList "OtherWanteds" otherWanteds+ dflags <- hsc_dflags <$> getTopEnv+ solutions <- tcPluginIO $ newIORef []+ forM_ effWanteds $ \wanted -> do+ printSingle "Wanted" wanted+ case findCandidates wanted effGivens of+ Left given -> printSingle "Already solved by" given+ Right [] -> printLn "No candidates"+ Right [(given, _)] -> do+ printSingle "Single candidate found" given+ emitEqConstraint solutions wanted given+ Right candidates -> do+ printList "Multiple candidates found" $ map fst candidates+ filterCandidates dflags None candidates >>= \case+ None -> printLn "No candidates left"+ Single given -> do+ printSingle "Single candidate left" given+ emitEqConstraint solutions wanted given+ Multiple -> printLn "Multiple candidates left"+ printLn ""+ TcPluginSolveResult [] [] <$> tcPluginIO (readIORef solutions) 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- -- Get rid of implicit parameters, they're weird.+ (otherGivens, effGivens)+ = second (extendEffGivens effWanteds)+ . partitionEithers+ . map (groupGivens pd.elemClass) . filter (not . isIP)- $ allWanteds+ $ allGivens - -- We store a list of the types of all given constraints, which will be- -- useful later.- allGivenTys = ctPred <$> allGivens+ (otherWanteds, effWanteds)+ = partitionEithers+ . map (groupWanteds pd.elemClass)+ . filter (not . isIP)+ $ allWanteds - -- 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+ filterCandidates+ :: DynFlags+ -> Candidates+ -> [(EffGiven, Subst)]+ -> TcPluginM Candidates+ filterCandidates dflags acc = \case+ [] -> pure acc+ (given, subst) : rest -> do+ printSingle "Candidate" given+ let relevantWanteds = (`mapMaybe` otherWanteds) $ \wanted ->+ if substHasAnyTyVar subst wanted.vars+ then Just $ substTy subst wanted.ty+ else Nothing+ printList "Relevant wanteds" relevantWanteds+ allWantedsSolvable relevantWanteds >>= \case+ True -> do+ printLn "Candidate fits"+ case acc of+ None -> filterCandidates dflags (Single given) rest+ Single _ -> pure Multiple+ Multiple -> error "unreachable"+ False -> do+ printLn "Candidate doesn't fit, skipping"+ filterCandidates dflags acc rest 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+ allWantedsSolvable :: [Type] -> TcPluginM Bool+ allWantedsSolvable = \case+ [] -> pure True+ wanted : rest -> do+ printSingle "Checking" wanted+ if wanted `unifiesWithAny` otherGivens+ then do+ printLn "Solvable from local context"+ allWantedsSolvable rest+ else case tcSplitTyConApp wanted of+ (con, args) -> case tyConClass_maybe con of+ Nothing -> do+ printLn "Not a class constraint"+ pure False+ Just cls -> findMatchingInstances dflags cls args >>= \case+ OneInst { cir_what = inst } -> do+ printSingle "Single matching instance" inst+ allWantedsSolvable rest+ NoInstance -> do+ printLn "No matching instances"+ pure False+ NotSure -> do+ printLn "Multiple matching instances"+ pure False - -- 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'- _ -> []+----------------------------------------+-- Standalone helpers - -- Determine whether a given constraint is of form 'e :> es'.- maybeEffGiven :: Ct -> Maybe EffGiven- maybeEffGiven = \case+findMatchingInstances :: DynFlags -> Class -> [Type] -> TcPluginM ClsInstResult+findMatchingInstances dflags cls args =+#if __GLASGOW_HASKELL__ <= 912+ unsafeTcPluginTcM $ matchGlobalInst dflags False cls args+#else+ unsafeTcPluginTcM $ matchGlobalInst dflags False cls args Nothing+#endif++findPluginModuleCompat :: HscEnv -> ModuleName -> TcPluginM FindResult+findPluginModuleCompat hsc_env mod_name = do+#if __GLASGOW_HASKELL__ <= 912+ 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_name)+#else+ tcPluginIO (findPluginModule hsc_env mod_name)+#endif++-- | Record a wanted equality constraint to aid typechecking.+emitEqConstraint :: IORef [Ct] -> EffWanted -> EffGiven -> TcPluginM ()+emitEqConstraint solutions wanted given = do+ let predTy =+#if __GLASGOW_HASKELL__ <= 912+ mkPrimEqPred wanted.eff given.eff+#else+ mkNomEqPred wanted.eff given.eff+#endif+ printSingle "Emitting constraint" predTy+ ev <- newWanted wanted.loc predTy+ tcPluginIO $ modifyIORef' solutions (mkNonCanonical ev :)++-- | Separate givens based on whether they're of the form @e :> es@ or not.+groupGivens :: Class -> Ct -> Either OtherGiven EffGiven+groupGivens elemCls = \case #if __GLASGOW_HASKELL__ < 908- CDictCan { cc_class = cls- , cc_tyargs = [eff, es]- } ->+ CDictCan+ { cc_class = cls+ , cc_tyargs = [eff, es]+ }+ | cls == elemCls -> #else- CDictCan DictCt { di_cls = cls- , di_tys = [eff, es]- } ->+ CDictCan DictCt+ { di_cls = cls+ , di_tys = [eff, es]+ }+ | cls == elemCls -> #endif- if cls == elemCls- then Just EffGiven { givenEffHead = fst $ splitAppTys eff- , givenEff = eff- , givenEs = es- }- else Nothing- _ -> Nothing+ Right EffGiven+ { effCon = fst $ splitAppTys eff+ , eff = eff+ , es = es+ }+ ct -> Left OtherGiven+ { ty = ctPred ct+ } - -- Check if a constraint in an implicit parameter.- isIP :: Ct -> Bool- isIP = \case+-- | Separate wanteds based on whether they're of the form @e :> es@ or not.+groupWanteds :: Class -> Ct -> Either OtherWanted EffWanted+groupWanteds elemCls = \case #if __GLASGOW_HASKELL__ < 908- CDictCan { cc_class = cls } -> isIPClass cls+ CDictCan+ { cc_ev = CtWanted { ctev_loc = loc }+ , cc_class = cls+ , cc_tyargs = [eff, es]+ }+ | cls == elemCls ->+#elif __GLASGOW_HASKELL__ <= 912+ CDictCan DictCt+ { di_ev = CtWanted { ctev_loc = loc }+ , di_cls = cls+ , di_tys = [eff, es]+ }+ | cls == elemCls -> #else- CDictCan DictCt { di_cls = cls } -> isIPClass cls+ CDictCan DictCt+ { di_ev = CtWanted WantedCt { ctev_loc = loc }+ , di_cls = cls+ , di_tys = [eff, es]+ }+ | cls == elemCls -> #endif- _ -> False+ Right EffWanted+ { effCon = fst $ splitAppTys eff+ , eff = eff+ , es = es+ , loc = loc+ }+ ct ->+ Left OtherWanted+ { ty = ctPred ct+ , vars = tyCoVarsOfType $ ctPred ct+ } - -- Determine whether a wanted constraint is of form 'e :> es'.- splitWanteds :: Ct -> Either PredType EffWanted- splitWanteds = \case+-- | We don't get appropriate given constraints when dealing with concrete (or+-- partially concrete) effect lists like (A : B : C : es), so they need to be+-- manually added (GHC will resolve them later).+extendEffGivens :: [EffWanted] -> [EffGiven] -> [EffGiven]+extendEffGivens wanteds givens = loop givens . nubType $ map (.es) wanteds+ where+ loop :: [EffGiven] -> [Type] -> [EffGiven]+ loop acc = \case+ [] -> acc+ fullEs : rest ->+ let extractGivens :: Type -> [EffGiven]+ extractGivens es = case splitAppTys es of+ (_colon, [_kind, eff, esTail]) -> EffGiven+ { effCon = fst $ splitAppTys eff+ , eff = eff+ , es = fullEs+ } : extractGivens esTail+ _ -> []+ in loop (extractGivens fullEs ++ acc) rest++-- | Check if a constraint in an implicit parameter. We discard all of them+-- since they will not affect resolution of @:>@ constraints.+isIP :: Ct -> Bool+isIP = \case #if __GLASGOW_HASKELL__ < 908- ct@CDictCan { cc_ev = CtWanted { ctev_loc = loc }- , cc_class = cls- , cc_tyargs = [eff, es]- } ->+ CDictCan { cc_class = cls } -> isIPClass cls #else- ct@(CDictCan DictCt { di_ev = CtWanted { ctev_loc = loc }- , di_cls = cls- , di_tys = [eff, es]- }) ->+ CDictCan DictCt { di_cls = cls } -> isIPClass cls #endif- if cls == elemCls- then Right EffWanted { wantedEffHead = fst $ splitAppTys eff- , wantedEff = eff- , wantedEs = es- , wantedLoc = loc- }- else Left $ ctPred ct- ct -> Left $ ctPred ct+ _ -> False - -- 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+-- | Attempt to unify types, but skip skolem (rigid) type variables. This is+-- crucial for proper filtering of candidates.+tcUnifyTyNoSkolems :: Type -> Type -> Maybe Subst+tcUnifyTyNoSkolems ty1 ty2 = tcUnifyTys bindFun [ty1] [ty2]+ where+ bindFun var _ty = if isSkolemTyVar var then dontBindMe else BindMe - -- 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)+ dontBindMe =+#if __GLASGOW_HASKELL__ <= 912+ Apart+#else+ DontBindMe+#endif++unifiesWithAny :: Type -> [OtherGiven] -> Bool+unifiesWithAny ty = any (isJust . tcUnifyTyNoSkolems ty . (.ty))++substHasAnyTyVar :: Subst -> TyCoVarSet -> Bool+substHasAnyTyVar subst = uniqSetAny (`elemUFM` getTvSubstEnv subst)++-- | Find givens unifiable with a wanted and give them back along with+-- appropriate substitutions.+--+-- Returns Left if the wanted is already solved by one of the givens.+findCandidates :: EffWanted -> [EffGiven] -> Either EffGiven [(EffGiven, Subst)]+findCandidates wanted = loop []+ where+ loop acc = \case+ [] -> Right acc+ given : rest ->+ if wanted.effCon `eqType` given.effCon && wanted.es `eqType` given.es+ then case tcUnifyTyNoSkolems wanted.eff given.eff of+ Just subst+ | isEmptySubst subst -> Left given+ | otherwise -> loop ((given, subst) : acc) rest+ Nothing -> loop acc rest+ else loop acc rest++nubType :: [Type] -> [Type]+nubType = coerce . S.toList . S.fromList @OrdType . coerce++newtype OrdType = OrdType Type++instance Eq OrdType where+ (==) = coerce eqType++instance Ord OrdType where+ compare = coerce nonDetCmpType++----------------------------------------+-- Debugging++#ifdef TIMING++timed :: PluginData -> TcPluginM a -> TcPluginM a+timed pd action = do+ t1 <- tcPluginIO getMonotonicTime+ a <- action+ tcPluginIO $ do+ t2 <- getMonotonicTime+ modifyIORef' pd.totalTime (+ (t2 - t1))+ pure a++pluginStopHook :: PluginData -> TcPluginM ()+pluginStopHook pd = tcPluginIO $ do+ time <- readIORef pd.totalTime+ putStrLn $ "Execution time of effectful-plugin (seconds): " ++ show time++#else++timed :: PluginData -> TcPluginM a -> TcPluginM a+timed _ action = action++pluginStopHook :: PluginData -> TcPluginM ()+pluginStopHook _ = pure ()++#endif++#ifdef VERBOSE++showOut :: O.Outputable o => o -> String+showOut = O.showSDocOneLine O.defaultSDocContext . O.ppr++printSingle :: O.Outputable x => String -> x -> TcPluginM ()+printSingle header x = printLn $ header ++ ": " ++ showOut x++printList :: O.Outputable x => String -> [x] -> TcPluginM ()+printList header = \case+ [] -> printLn $ header ++ ": []"+ xs -> do+ printLn $ header ++ ":"+ forM_ xs $ \x -> printLn $ "- " ++ showOut x++printLn :: String -> TcPluginM ()+printLn = tcPluginIO . putStrLn++#else++printSingle :: String -> x -> TcPluginM ()+printSingle _ _ = pure ()++printList :: String -> [x] -> TcPluginM ()+printList _ _ = pure ()++printLn :: String -> TcPluginM ()+printLn _ = pure ()++#endif
tests/PluginTests.hs view
@@ -1,19 +1,22 @@--- Tests copied from polysemy-plugin:+-- Most tests copied from polysemy-plugin: -- -- https://github.com/polysemy-research/polysemy/tree/master/polysemy-plugin/test -- -- (c) 2019 Sandy Maguire, licensed under BSD-3-Clause {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE OverloadedStrings #-}-{-# OPTIONS_GHC -Wno-unused-foralls -fplugin=Effectful.Plugin #-}+{-# OPTIONS_GHC -Wno-unused-foralls #-} module Main where import Data.String+import Data.Typeable import Unsafe.Coerce import Effectful import Effectful.Dispatch.Dynamic import Effectful.Error.Static+import Effectful.Labeled+import Effectful.Labeled.Reader import Effectful.State.Static.Local main :: IO ()@@ -22,17 +25,65 @@ ---------------------------------------- -- Tests +data X1 = X1 { x1 :: Int }+data X2 = X2 { x2 :: X1 }++x1x2 :: (State X1 :> es, State X2 :> es) => Eff es ()+x1x2 = do+ _ <- gets (.x1)+ _ <- gets (.x2.x1)+ pure ()++typeable :: (State X1 :> es, State x :> es) => Eff es ()+typeable = do+ _ <- gets typeOf+ pure ()++data Function i o :: Effect where+ Call :: i -> Function i o m o+type instance DispatchOf (Function i o) = Dynamic++call :: (HasCallStack, Function i o :> es) => i -> Eff es o+call a = send $ Call a++callTest+ :: ( Function Int a :> es+ , Function a Int :> es+ , Labeled "x" (Reader Int) :> es+ , Labeled "y" (Reader b) :> es+ , IsString s+ , Function s a :> es+ )+ => Eff es ()+callTest = do+ a1 <- call 1+ a2 <- call ""+ _ <- call a1+ _ <- call a2+ (_::Int) <- ask+ _ <- ask @"y"+ pure ()++class X a where+ xxx :: a+ class MPTC a b where mptc :: a -> b instance MPTC Bool Int where mptc _ = 1000 -uniquelyInt :: (State Int :> es, State String :> es) => Eff es ()-uniquelyInt = put 10+ordPut :: (State s :> es, Ord s) => s -> Eff es ()+ordPut = put -uniquelyA :: (Num a, State a :> es, State b :> es) => Eff es ()-uniquelyA = put 10+uniquelyX :: (X a, State a :> es) => Eff es ()+uniquelyX = put xxx++uniquelyA :: (Num a, State a :> es, State b :> es, IsString b) => Eff es ()+uniquelyA = put 10 >> put ""++uniquelyInt :: (State Int :> es, State String :> es) => Eff es ()+uniquelyInt = ordPut 10 >> put "" uniquelyString :: (State Int :> es, State String :> es) => Eff es () uniquelyString = put mempty