diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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. diff --git a/effectful-plugin.cabal b/effectful-plugin.cabal --- a/effectful-plugin.cabal +++ b/effectful-plugin.cabal @@ -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 diff --git a/src-legacy/Effectful/Plugin.hs b/src-legacy/Effectful/Plugin.hs deleted file mode 100644 --- a/src-legacy/Effectful/Plugin.hs +++ /dev/null @@ -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 diff --git a/src/Effectful/Plugin.hs b/src/Effectful/Plugin.hs --- a/src/Effectful/Plugin.hs +++ b/src/Effectful/Plugin.hs @@ -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 diff --git a/tests/PluginTests.hs b/tests/PluginTests.hs --- a/tests/PluginTests.hs +++ b/tests/PluginTests.hs @@ -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