effectful-plugin 1.0.0.0 → 1.1.0.0

raw patch · 7 files changed

+544/−263 lines, 7 filesdep ~ghcPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: ghc

API changes (from Hackage documentation)

Files

• CHANGELOG.md +3/−0
• README.md +2/−2
• effectful-plugin.cabal +15/−14
• src-legacy/Effectful/Plugin.hs +241/−0
• src/Effectful/Plugin.hs +276/−2
• src/Effectful/Plugin/Internal.hs +0/−238
• tests/PluginTests.hs +7/−7

@@ -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.

@@ -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)

@@ -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

@@ -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

@@ -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)

@@ -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

@@ -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)