packages feed

polysemy-plugin 0.2.2.0 → 0.2.3.0

raw patch · 11 files changed

+497/−237 lines, 11 filesdep ~polysemy

Dependency ranges changed: polysemy

Files

ChangeLog.md view
@@ -1,5 +1,14 @@ # Changelog for polysemy-plugin ++## 0.2.3.0 (2019-09-04)+- The plugin will now choose between given effects based on the ability to unify them.+    This makes it possible for disambiguation to kick in even when using multiple+    instances of the same effect with different type variables,+    as long as type annotations/applications are used to+    target a specific instance.+- Updated the test suite to test against `polysemy-1.2.0.0`.+ ## 0.2.2.0 (2019-07-04)  - The plugin will now prevent some false-positives in `polysemy`'s error@@ -50,5 +59,5 @@  ## Unreleased changes -- Added `runErrorAsAnother`+- Added `mapError`
polysemy-plugin.cabal view
@@ -4,10 +4,10 @@ -- -- see: https://github.com/sol/hpack ----- hash: 63b03550f0fe1e13941505a11116fac8e6eef8a871dff51b30d2bca2263b2a75+-- hash: 01634ce3c7ac101e60c1a02f8ccad7ec499c02a04b66e5d9dd5993f314318097  name:           polysemy-plugin-version:        0.2.2.0+version:        0.2.3.0 synopsis:       Disambiguate obvious uses of effects. description:    Please see the README on GitHub at <https://github.com/isovector/polysemy/tree/master/polysemy-plugin#readme> category:       Polysemy@@ -31,6 +31,9 @@   exposed-modules:       Polysemy.Plugin       Polysemy.Plugin.Fundep+      Polysemy.Plugin.Fundep.Stuff+      Polysemy.Plugin.Fundep.Unification+      Polysemy.Plugin.Fundep.Utils       Polysemy.Plugin.Phases   other-modules:       Paths_polysemy_plugin@@ -55,6 +58,7 @@       DoctestSpec       ExampleSpec       LegitimateTypeErrorSpec+      MultipleVarsSpec       PluginSpec       TypeErrors       VDQSpec@@ -73,7 +77,7 @@     , ghc-tcplugins-extra >=0.3 && <0.4     , hspec >=2.6.0 && <3     , inspection-testing >=0.4.2 && <0.5-    , polysemy >=0.6.0.0+    , polysemy >=1.2.0.0     , polysemy-plugin     , should-not-typecheck >=2.1.0 && <3     , syb >=0.7 && <0.8
src/Polysemy/Plugin/Fundep.hs view
@@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ -- The MIT License (MIT) ----- Copyright (c) 2017 Luka Horvat+-- Copyright (c) 2017 Luka Horvat, 2019 Sandy Maguire -- -- Permission is hereby granted, free of charge, to any person obtaining a copy -- of this software and associated documentation files (the "Software"), to@@ -26,218 +26,119 @@ -- ------------------------------------------------------------------------------ ----- This module is heavily based on 'Control.Effects.Plugin' from the--- 'simple-effects' package, originally by Luka Horvat.+-- This module was originally based on 'Control.Effects.Plugin' from the+-- 'simple-effects' package, by Luka Horvat. -- -- https://gitlab.com/LukaHorvat/simple-effects/commit/966ce80b8b5777a4bd8f87ffd443f5fa80cc8845#f51c1641c95dfaa4827f641013f8017e8cd02aab  module Polysemy.Plugin.Fundep (fundepPlugin) where -import           Class-import           CoAxiom-import           Control.Applicative import           Control.Monad import           Data.Bifunctor-import           Data.Bool import           Data.Coerce-import           Data.Function (on) import           Data.IORef-import qualified Data.Kind as K-import           Data.List+import qualified Data.Map as M import           Data.Maybe import qualified Data.Set as S-import           FastString (fsLit)-import           GHC (TyCon, Name)-import           GHC.TcPluginM.Extra (lookupModule, lookupName)-import           Module (mkModuleName)-import           OccName (mkTcOcc)+import           Polysemy.Plugin.Fundep.Stuff+import           Polysemy.Plugin.Fundep.Unification+import           Polysemy.Plugin.Fundep.Utils import           TcEvidence-import           TcPluginM (TcPluginM, tcLookupClass, tcLookupTyCon, tcPluginIO)+import           TcPluginM (TcPluginM, tcPluginIO) import           TcRnTypes import           TcSMonad hiding (tcLookupClass)-import           TyCoRep (Type (..)) import           Type  -data LookupState-  = Locations-  | Things --type family ThingOf (l :: LookupState) (a :: K.Type) :: K.Type where-  ThingOf 'Locations _ = (String, String)-  ThingOf 'Things a = a---data PolysemyStuff (l :: LookupState) = PolysemyStuff-  { findClass    :: ThingOf l Class-  , semTyCon     :: ThingOf l TyCon-  , ifStuckTyCon :: ThingOf l TyCon-  , indexOfTyCon :: ThingOf l TyCon+fundepPlugin :: TcPlugin+fundepPlugin = TcPlugin+  { tcPluginInit =+      (,) <$> tcPluginIO (newIORef S.empty)+          <*> polysemyStuff+  , tcPluginSolve = solveFundep+  , tcPluginStop = const $ pure ()   }  -class CanLookup a where-  lookupStrategy :: Name -> TcPluginM a--instance CanLookup Class where-  lookupStrategy = tcLookupClass--instance CanLookup TyCon where-  lookupStrategy = tcLookupTyCon---doLookup :: CanLookup a => ThingOf 'Locations a -> TcPluginM (ThingOf 'Things a)-doLookup (mdname, name) = do-  md  <- lookupModule (mkModuleName mdname) $ fsLit "polysemy"-  nm <- lookupName md $ mkTcOcc name-  lookupStrategy nm---lookupEverything :: PolysemyStuff 'Locations -> TcPluginM (PolysemyStuff 'Things)-lookupEverything (PolysemyStuff a b c d) =-  PolysemyStuff <$> doLookup a-                <*> doLookup b-                <*> doLookup c-                <*> doLookup d---polysemyStuffLocations :: PolysemyStuff 'Locations-polysemyStuffLocations = PolysemyStuff-  { findClass    = ("Polysemy.Internal.Union",                  "Find")-  , semTyCon     = ("Polysemy.Internal",                        "Sem")-  , ifStuckTyCon = ("Polysemy.Internal.CustomErrors.Redefined", "IfStuck")-  , indexOfTyCon = ("Polysemy.Internal.Union",                  "IndexOf")+------------------------------------------------------------------------------+-- | Corresponds to a 'Polysemy.Internal.Union.Find' constraint. For example,+-- given @Member (State s) r@, we would get:+data FindConstraint = FindConstraint+  { fcLoc        :: CtLoc+  , fcEffectName :: Type  -- ^ @State@+  , fcEffect     :: Type  -- ^ @State s@+  , fcRow        :: Type  -- ^ @r@   }  -fundepPlugin :: TcPlugin-fundepPlugin = TcPlugin-    { tcPluginInit =-        (,) <$> tcPluginIO (newIORef S.empty)-            <*> lookupEverything polysemyStuffLocations-    , tcPluginSolve = solveFundep-    , tcPluginStop = const (return ()) }+------------------------------------------------------------------------------+-- | Given a list of constraints, filter out the 'FindConstraint's.+getFindConstraints :: PolysemyStuff 'Things -> [Ct] -> [FindConstraint]+getFindConstraints (findClass -> cls) cts = do+  cd@CDictCan{cc_class = cls', cc_tyargs = [_, r, eff]} <- cts+  guard $ cls == cls'+  pure $ FindConstraint+    { fcLoc = ctLoc cd+    , fcEffectName = getEffName eff+    , fcEffect = eff+    , fcRow = r+    } -allMonadEffectConstraints :: PolysemyStuff 'Things -> [Ct] -> [(CtLoc, (Type, Type, Type))]-allMonadEffectConstraints (findClass -> cls) cts =-    [ (ctLoc cd, (effName, eff, r))-    | cd@CDictCan{cc_class = cls', cc_tyargs = [_, r, eff]} <- cts-    , cls == cls'-    , let effName = getEffName eff-    ] -singleListToJust :: [a] -> Maybe a-singleListToJust [a] = Just a-singleListToJust _ = Nothing+------------------------------------------------------------------------------+-- | If there's only a single @Member@ in the same @r@ whose effect name+-- matches and could possibly unify, return its effect (including tyvars.)+findMatchingEffectIfSingular+    :: FindConstraint+    -> [FindConstraint]+    -> Maybe Type+findMatchingEffectIfSingular (FindConstraint _ eff_name wanted r) ts =+  singleListToJust $ do+    FindConstraint _ eff_name' eff' r' <- ts+    guard $ eqType eff_name eff_name'+    guard $ eqType r r'+    guard $ canUnifyRecursive FunctionDef wanted eff'+    pure eff' -findMatchingEffectIfSingular :: (Type, Type, Type) -> [(Type, Type, Type)] -> Maybe Type-findMatchingEffectIfSingular (effName, _, mon) ts = singleListToJust-    [ eff'-        | (effName', eff', mon') <- ts-        , eqType effName effName'-        , eqType mon mon' ] +------------------------------------------------------------------------------+-- | Given an effect, compute its effect name. getEffName :: Type -> Type getEffName t = fst $ splitAppTys t  -canUnifyRecursive :: SolveContext -> Type -> Type -> Bool-canUnifyRecursive solve_ctx = go True+------------------------------------------------------------------------------+-- | Generate a wanted unification for the effect described by the+-- 'FindConstraint' and the given effect.+mkWantedForce+  :: FindConstraint+  -> Type+  -> TcPluginM (Unification, Ct)+mkWantedForce fc given = do+  (ev, _) <- unsafeTcPluginTcM+           . runTcSDeriveds+           $ newWantedEq (fcLoc fc) Nominal wanted given+  pure ( Unification (OrdType wanted) (OrdType given)+       , CNonCanonical ev+       )   where-    -- It's only OK to solve a polymorphic "given" if we're in the context of-    -- an interpreter, because it's not really a given!-    poly_given_ok :: Bool-    poly_given_ok =-      case solve_ctx of-        InterpreterUse _ -> True-        FunctionDef      -> False--    -- On the first go around, we don't want to unify effects with tyvars, but-    -- we _do_ want to unify their arguments, thus 'is_first'.-    go :: Bool -> Type -> Type -> Bool-    go is_first wanted given =-      let (w, ws) = splitAppTys wanted-          (g, gs) = splitAppTys given-       in (&& bool (canUnify poly_given_ok) eqType is_first w g)-        . flip all (zip ws gs)-        $ \(wt, gt) -> canUnify poly_given_ok wt gt || go False wt gt---canUnify :: Bool -> Type -> Type -> Bool-canUnify poly_given_ok wt gt =-  or [ isTyVarTy wt-     , isTyVarTy gt && poly_given_ok-     , eqType wt gt-     ]-+    wanted = fcEffect fc  --------------------------------------------------------------------------------- | Like 'Control.Monad.when', but in the context of an 'Alternative'.-whenA-    :: (Monad m, Alternative z)-    => Bool-    -> m a-    -> m (z a)-whenA False _ = pure empty-whenA True ma = fmap pure ma--+-- | Generate a wanted unification for the effect described by the+-- 'FindConstraint' and the given effect --- if they can be unified in this+-- context. mkWanted-    :: SolveContext-    -> CtLoc-    -> Type-    -> Type-    -> TcPluginM (Maybe ( (OrdType, OrdType)  -- the types we want to unify-                        , Ct                  -- the constraint-                        ))-mkWanted solve_ctx loc wanted given =-  whenA (not (mustUnify solve_ctx) || canUnifyRecursive solve_ctx wanted given) $ do-    (ev, _) <- unsafeTcPluginTcM-             . runTcSDeriveds-             $ newWantedEq loc Nominal wanted given-    pure ( (OrdType wanted, OrdType given)-         , CNonCanonical ev-         )--thd :: (a, b, c) -> c-thd (_, _, c) = c--countLength :: (a -> a -> Bool) -> [a] -> [(a, Int)]-countLength eq as =-  let grouped = groupBy eq as-   in zipWith (curry $ bimap head length) grouped grouped------------------------------------------------------------------------------------ | 'Type's don't have 'Eq' or 'Ord' instances by default, even though there--- are functions in GHC that implement these operations. This newtype gives us--- those instances.-newtype OrdType = OrdType-  { getOrdType :: Type-  }--instance Eq OrdType where-  (==) = eqType `on` getOrdType--instance Ord OrdType where-  compare = nonDetCmpType `on` getOrdType------------------------------------------------------------------------------------ | The context in which we're attempting to solve a constraint.-data SolveContext-  = -- | In the context of a function definition.-    FunctionDef-    -- | In the context of running an interpreter. The 'Bool' corresponds to-    -- whether we are only trying to solve a single 'Member' constraint right-    -- now. If so, we *must* produce a unification wanted.-  | InterpreterUse Bool-  deriving (Eq, Ord, Show)--mustUnify :: SolveContext -> Bool-mustUnify FunctionDef = True-mustUnify (InterpreterUse b) = b+    :: FindConstraint+    -> SolveContext+    -> Type  -- ^ The given effect.+    -> TcPluginM (Maybe (Unification, Ct))+mkWanted fc solve_ctx given =+  whenA (not (mustUnify solve_ctx) || canUnifyRecursive solve_ctx wanted given) $+    mkWantedForce fc given+  where+    wanted = fcEffect fc   ------------------------------------------------------------------------------@@ -246,68 +147,94 @@ getBogusRs :: PolysemyStuff 'Things -> [Ct] -> [Type] getBogusRs stuff wanteds = do   CIrredCan ct _ <- wanteds-  case splitAppTys $ ctev_pred ct of-    (_, [_, _, a, b]) ->-      maybeToList (getRIfSem stuff a) ++ maybeToList (getRIfSem stuff b)-    (_, _) -> []+  (_, [_, _, a, b]) <- pure . splitAppTys $ ctev_pred ct+  maybeToList (extractRowFromSem stuff a)+    ++ maybeToList (extractRowFromSem stuff b)   ------------------------------------------------------------------------------ -- | Take the @r@ out of @Sem r a@.-getRIfSem :: PolysemyStuff 'Things -> Type -> Maybe Type-getRIfSem (semTyCon -> sem) ty =-  case splitTyConApp_maybe ty of-    Just (tycon, [r, _]) | tycon == sem -> pure r-    _                                   -> Nothing+extractRowFromSem :: PolysemyStuff 'Things -> Type -> Maybe Type+extractRowFromSem (semTyCon -> sem) ty = do+  (tycon, [r, _]) <- splitTyConApp_maybe ty+  guard $ tycon == sem+  pure r   ------------------------------------------------------------------------------ -- | Given a list of bogus @r@s, and the wanted constraints, produce bogus -- evidence terms that will prevent @IfStuck (IndexOf r _) _ _@ error messsages.-solveBogusError :: PolysemyStuff 'Things -> [Type] -> [Ct] -> [(EvTerm, Ct)]-solveBogusError stuff bogus wanteds = do+solveBogusError :: PolysemyStuff 'Things -> [Ct] -> [(EvTerm, Ct)]+solveBogusError stuff wanteds = do+  let splitTyConApp_list = maybeToList  . splitTyConApp_maybe++  let bogus = getBogusRs stuff wanteds   ct@(CIrredCan ce _) <- wanteds-  case splitTyConApp_maybe $ ctev_pred ce of-    Just (stuck, [_, _, expr, _, _]) | stuck == ifStuckTyCon stuff -> do-      case splitTyConApp_maybe expr of-        Just (idx, [_, r, _]) | idx == indexOfTyCon stuff -> do-          case elem @[] (OrdType r) $ coerce bogus of-            True -> pure (error "bogus proof for stuck type family", ct)-            False -> []-        _ -> []-    _ -> []+  (stuck, [_, _, expr, _, _]) <- splitTyConApp_list $ ctev_pred ce+  guard $ stuck == ifStuckTyCon stuff+  (idx, [_, r, _]) <- splitTyConApp_list expr+  guard $ idx == indexOfTyCon stuff+  guard $ elem @[] (OrdType r) $ coerce bogus+  pure (error "bogus proof for stuck type family", ct)  +------------------------------------------------------------------------------+-- | Determine if there is exactly one wanted find for the @r@ in question.+exactlyOneWantedForR+    :: [FindConstraint]  -- ^ Wanted finds+    -> Type              -- ^ Effect row+    -> Bool+exactlyOneWantedForR wanteds+    = fromMaybe False+    . flip M.lookup singular_r+    . OrdType+  where+    singular_r = M.fromList+               -- TODO(sandy): Nothing fails if this is just @second (const+               -- True)@. Why not? Incomplete test suite, or doing too much+               -- work?+               . fmap (second (/= 1))+               . countLength+               $ fmap (OrdType . fcRow) wanteds++ solveFundep-    :: (IORef (S.Set (OrdType, OrdType)), PolysemyStuff 'Things)+    :: ( IORef (S.Set Unification)+       , PolysemyStuff 'Things+       )     -> [Ct]     -> [Ct]     -> [Ct]     -> TcPluginM TcPluginResult solveFundep _ _ _ [] = pure $ TcPluginOk [] []-solveFundep (ref, stuff) giv _ want = do-    let bogus = getBogusRs stuff want-        solved_bogus = solveBogusError stuff bogus want+solveFundep (ref, stuff) given _ wanted = do+  let wanted_finds = getFindConstraints stuff wanted+      given_finds  = getFindConstraints stuff given -    let wantedEffs = allMonadEffectConstraints stuff want-        givenEffs = snd <$> allMonadEffectConstraints stuff giv-        num_wanteds_by_r = countLength eqType $ fmap (thd . snd) wantedEffs-        must_unify r =-          let Just num_wanted = find (eqType r . fst) num_wanteds_by_r-           in snd num_wanted /= 1+  eqs <- forM wanted_finds $ \fc -> do+    let r  = fcRow fc+    case findMatchingEffectIfSingular fc given_finds of+      -- We found a real given, therefore we are in the context of a function+      -- with an explicit @Member e r@ constraint. We also know it can+      -- be unified (although it may generate unsatisfiable constraints).+      Just eff' -> Just <$> mkWantedForce fc eff' -    eqs <- forM wantedEffs $ \(loc, e@(_, eff, r)) -> do-      case findMatchingEffectIfSingular e givenEffs of-        Nothing -> do-          case splitAppTys r of-            (_, [_, eff', _]) -> mkWanted (InterpreterUse $ must_unify r) loc eff eff'-            _                 -> pure Nothing-        Just eff' -> mkWanted FunctionDef loc eff eff'+      -- Otherwise, check to see if @r ~ (e ': r')@. If so, pretend we're+      -- trying to solve a given @Member e r@. But this can only happen in the+      -- context of an interpreter!+      Nothing ->+        case splitAppTys r of+          (_, [_, eff', _]) ->+            mkWanted fc+                     (InterpreterUse $ exactlyOneWantedForR wanted_finds r)+                     eff'+          _ -> pure Nothing -    already_emitted <- tcPluginIO $ readIORef ref-    let new_wanteds = filter (not . flip S.member already_emitted . fst)-                    $ catMaybes eqs+  -- We only want to emit a unification wanted once, otherwise a type error can+  -- force the type checker to loop forever.+  already_emitted <- tcPluginIO $ readIORef ref+  let (unifications, new_wanteds) = unzipNewWanteds already_emitted $ catMaybes eqs+  tcPluginIO $ modifyIORef ref $ S.union $ S.fromList unifications -    tcPluginIO $ modifyIORef ref $ S.union $ S.fromList $ fmap fst new_wanteds-    pure . TcPluginOk solved_bogus $ fmap snd new_wanteds+  pure $ TcPluginOk (solveBogusError stuff wanted) new_wanteds
+ src/Polysemy/Plugin/Fundep/Stuff.hs view
@@ -0,0 +1,83 @@+module Polysemy.Plugin.Fundep.Stuff+  ( PolysemyStuff (..)+  , LookupState (..)+  , polysemyStuff+  ) where++import Data.Kind (Type)+import FastString (fsLit)+import GHC (Name, Class, TyCon, mkModuleName)+import GHC.TcPluginM.Extra (lookupModule, lookupName)+import OccName (mkTcOcc)+import TcPluginM (TcPluginM, tcLookupClass, tcLookupTyCon)++++------------------------------------------------------------------------------+-- | All of the things from "polysemy" that we need access to in the plugin.+-- When @l ~ 'Locations@, each of these is just a pair of strings. When @l+-- ~ 'Things@, it's actually references to the stuff.+data PolysemyStuff (l :: LookupState) = PolysemyStuff+  { findClass    :: ThingOf l Class+  , semTyCon     :: ThingOf l TyCon+  , ifStuckTyCon :: ThingOf l TyCon+  , indexOfTyCon :: ThingOf l TyCon+  }+++------------------------------------------------------------------------------+-- | All of the things we need to lookup.+polysemyStuffLocations :: PolysemyStuff 'Locations+polysemyStuffLocations = PolysemyStuff+  { findClass    = ("Polysemy.Internal.Union",                  "Find")+  , semTyCon     = ("Polysemy.Internal",                        "Sem")+  , ifStuckTyCon = ("Polysemy.Internal.CustomErrors.Redefined", "IfStuck")+  , indexOfTyCon = ("Polysemy.Internal.Union",                  "IndexOf")+  }+++------------------------------------------------------------------------------+-- | Lookup all of the 'PolysemyStuff'.+polysemyStuff :: TcPluginM (PolysemyStuff 'Things)+polysemyStuff =+  let PolysemyStuff a b c d = polysemyStuffLocations+   in PolysemyStuff <$> doLookup a+                    <*> doLookup b+                    <*> doLookup c+                    <*> doLookup d+++------------------------------------------------------------------------------+-- | Data kind for 'ThingOf'.+data LookupState+  = Locations+  | Things+++------------------------------------------------------------------------------+-- | HKD indexed by the 'LookupState'; used by 'PolysemyStuff'.+type family ThingOf (l :: LookupState) (a :: Type) :: Type where+  ThingOf 'Locations _ = (String, String)+  ThingOf 'Things    a = a+++------------------------------------------------------------------------------+-- | Things that can be found in a 'TcPluginM' environment.+class CanLookup a where+  lookupStrategy :: Name -> TcPluginM a++instance CanLookup Class where+  lookupStrategy = tcLookupClass++instance CanLookup TyCon where+  lookupStrategy = tcLookupTyCon+++------------------------------------------------------------------------------+-- | Transform a @'ThingOf' 'Locations@ into a @'ThingOf' 'Things@.+doLookup :: CanLookup a => ThingOf 'Locations a -> TcPluginM (ThingOf 'Things a)+doLookup (mdname, name) = do+  md <- lookupModule (mkModuleName mdname) $ fsLit "polysemy"+  nm <- lookupName md $ mkTcOcc name+  lookupStrategy nm+
+ src/Polysemy/Plugin/Fundep/Unification.hs view
@@ -0,0 +1,136 @@+module Polysemy.Plugin.Fundep.Unification where++import           Data.Bool+import           Data.Function (on)+import qualified Data.Set as S+import           TcRnTypes+import           Type+++------------------------------------------------------------------------------+-- | The context in which we're attempting to solve a constraint.+data SolveContext+  = -- | In the context of a function definition.+    FunctionDef+    -- | In the context of running an interpreter. The 'Bool' corresponds to+    -- whether we are only trying to solve a single 'Member' constraint right+    -- now. If so, we *must* produce a unification wanted.+  | InterpreterUse Bool+  deriving (Eq, Ord, Show)+++------------------------------------------------------------------------------+-- | Depending on the context in which we're solving a constraint, we may or+-- may not want to force a unification of effects. For example, when defining+-- user code whose type is @Member (State Int) r => ...@, if we see @get :: Sem+-- r s@, we should unify @s ~ Int@.+mustUnify :: SolveContext -> Bool+mustUnify FunctionDef = True+mustUnify (InterpreterUse b) = b+++------------------------------------------------------------------------------+-- | Determine whether or not two effects are unifiable. This is nuanced.+--+-- There are several cases:+--+-- 1. [W] ∀ e1. e1   [G] ∀ e2. e2+--    Always fails, because we never want to unify two effects if effect names+--    are polymorphic.+--+-- 2. [W] State s    [G] State Int+--    Always succeeds. It's safe to take our given as a fundep annotation.+--+-- 3. [W] State Int  [G] State s+--        (when the [G] is a given that comes from a type signature)+--+--    This should fail, because it means we wrote the type signature @Member+--    (State s) r => ...@, but are trying to use @s@ as an @Int@. Clearly+--    bogus!+--+-- 4. [W] State Int  [G] State s+--        (when the [G] was generated by running an interpreter)+--+--    Sometimes OK, but only if the [G] is the only thing we're trying to solve+--    right now. Consider the case:+--+--      runState 5 $ pure @(Sem (State Int ': r)) ()+--+--    Here we have  [G] forall a. Num a => State a  and  [W] State Int. Clearly+--    the typechecking should flow "backwards" here, out of the row and into+--    the type of 'runState'.+--+--    What happens if there are multiple [G]s in scope for the same @r@? Then+--    we'd emit multiple unification constraints for the same effect but with+--    different polymorphic variables, which would unify a bunch of effects+--    that shouldn't be!+canUnifyRecursive+    :: SolveContext+    -> Type  -- ^ wanted+    -> Type  -- ^ given+    -> Bool+canUnifyRecursive solve_ctx = go True+  where+    -- It's only OK to solve a polymorphic "given" if we're in the context of+    -- an interpreter, because it's not really a given!+    poly_given_ok :: Bool+    poly_given_ok =+      case solve_ctx of+        InterpreterUse _ -> True+        FunctionDef      -> False++    -- On the first go around, we don't want to unify effects with tyvars, but+    -- we _do_ want to unify their arguments, thus 'is_first'.+    go :: Bool -> Type -> Type -> Bool+    go is_first wanted given =+      let (w, ws) = splitAppTys wanted+          (g, gs) = splitAppTys given+       in (&& bool (canUnify poly_given_ok) eqType is_first w g)+        . flip all (zip ws gs)+        $ \(wt, gt) -> canUnify poly_given_ok wt gt || go False wt gt+++------------------------------------------------------------------------------+-- | A non-recursive version of 'canUnifyRecursive'.+canUnify :: Bool -> Type -> Type -> Bool+canUnify poly_given_ok wt gt =+  or [ isTyVarTy wt+     , isTyVarTy gt && poly_given_ok+     , eqType wt gt+     ]+++------------------------------------------------------------------------------+-- | A wrapper for two types that we want to say have been unified.+data Unification = Unification+  { _unifyLHS :: OrdType+  , _unifyRHS :: OrdType+  }+  deriving (Eq, Ord)+++------------------------------------------------------------------------------+-- | 'Type's don't have 'Eq' or 'Ord' instances by default, even though there+-- are functions in GHC that implement these operations. This newtype gives us+-- those instances.+newtype OrdType = OrdType+  { getOrdType :: Type+  }++instance Eq OrdType where+  (==) = eqType `on` getOrdType++instance Ord OrdType where+  compare = nonDetCmpType `on` getOrdType+++------------------------------------------------------------------------------+-- | Filter out the unifications we've already emitted, and then give back the+-- things we should put into the @S.Set Unification@, and the new constraints+-- we should emit.+unzipNewWanteds+    :: S.Set Unification+    -> [(Unification, Ct)]+    -> ([Unification], [Ct])+unzipNewWanteds old = unzip . filter (not . flip S.member old . fst)+
+ src/Polysemy/Plugin/Fundep/Utils.hs view
@@ -0,0 +1,33 @@+module Polysemy.Plugin.Fundep.Utils  where++import Control.Applicative+import Data.Bifunctor+import Data.List++++------------------------------------------------------------------------------+-- | Returns the head of the list iff there is exactly one element.+singleListToJust :: [a] -> Maybe a+singleListToJust [a] = Just a+singleListToJust _ = Nothing+++------------------------------------------------------------------------------+-- | Like 'Control.Monad.when', but in the context of an 'Alternative'.+whenA+    :: (Monad m, Alternative z)+    => Bool+    -> m a+    -> m (z a)+whenA False _ = pure empty+whenA True ma = fmap pure ma+++------------------------------------------------------------------------------+-- | Count the number of times 'a' is present in the list.+countLength ::  Eq a => [a] -> [(a, Int)]+countLength as =+  let grouped = group as+   in zipWith (curry $ bimap head length) grouped grouped+
test/ExampleSpec.hs view
@@ -16,10 +16,10 @@  makeSem ''Teletype -runTeletypeIO :: Member (Lift IO) r => Sem (Teletype ': r) a -> Sem r a-runTeletypeIO = interpret $ \case-  ReadTTY      -> sendM getLine-  WriteTTY msg -> sendM $ putStrLn msg+teletypeToIO :: Member (Embed IO) r => Sem (Teletype ': r) a -> Sem r a+teletypeToIO = interpret $ \case+  ReadTTY      -> embed getLine+  WriteTTY msg -> embed $ putStrLn msg  data CustomException = ThisException | ThatException deriving Show @@ -33,7 +33,13 @@             _             -> writeTTY i >> writeTTY "no exceptions"  foo :: IO (Either CustomException ())-foo = (runM .@ runResourceInIO .@@ runErrorInIO @CustomException) $ runTeletypeIO program+foo =+    runFinal+  . embedToFinal @IO+  . resourceToIOFinal+  . errorToIOFinal @CustomException+  . teletypeToIO+  $ program  spec :: Spec spec = describe "example" $ do
test/LegitimateTypeErrorSpec.hs view
@@ -6,8 +6,8 @@ import Test.Hspec import Test.ShouldNotTypecheck -wrongLift :: Member (Lift IO) r => Sem r ()-wrongLift = sendM putStrLn+wrongEmbed :: Member (Embed IO) r => Sem r ()+wrongEmbed = embed putStrLn  wrongReturn :: Sem (e ': r) () -> Sem r () wrongReturn = reinterpret undefined@@ -17,8 +17,8 @@ spec :: Spec spec = do   describe "Legitimate type errors" $ do-    it "should be caused by `sendM`ing an unsaturated function" $-        shouldNotTypecheck wrongLift+    it "should be caused by `embed`ing an unsaturated function" $+        shouldNotTypecheck wrongEmbed      it "should be caused by giving a bad type to reinterpret" $         shouldNotTypecheck wrongReturn
+ test/MultipleVarsSpec.hs view
@@ -0,0 +1,62 @@+{-# LANGUAGE TemplateHaskell #-}+{-# OPTIONS_GHC -fplugin=Polysemy.Plugin #-}++module MultipleVarsSpec where++import Polysemy+import Polysemy.State++import Test.Hspec++data TaggedState k s m a where+  TaggedGet :: forall k s m. TaggedState k s m s+  TaggedPut :: forall k s m. s -> TaggedState k s m ()++makeSem ''TaggedState++runTaggedState :: forall k s r a+                . s+               -> Sem (TaggedState k s ': r) a+               -> Sem r (s, a)+runTaggedState s =+    (runState s .)+  $ reinterpret+  $ \case+    TaggedGet -> get+    TaggedPut s -> put s++test :: Members '[+          TaggedState Char Int+        , TaggedState Bool Int+        ] r+     => Sem r ()+test = do+  taggedPut @Bool 10+  taggedPut @Char (-10)++spec :: Spec+spec = describe "Using multiple, but ununifiable instances\+               \ of the same effect" $ do+  it "should get disambiguated and compile, \+     \and actions should target the right effects." $ do+    let+      res1 =+          run+        . runTaggedState @Char 0+        . runTaggedState @Bool 7+        $ test+      res2 =+          run+        . runTaggedState @Bool 0+        . runTaggedState @Char 7+        $ test+      res3 =+          run+        . runTaggedState @Bool 0+        . runTaggedState @Char 7+        $ do+          taggedPut @Bool 10+          taggedPut @Char (-10)+    res1 `shouldBe` (-10, (10, ()))+    res2 `shouldBe` (10, (-10, ()))+    res3 `shouldBe` (10, (-10, ()))
test/PluginSpec.hs view
@@ -46,8 +46,8 @@   err  -lifted :: Monad m => Member (Lift m) r => Sem r ()-lifted = sendM $ pure ()+lifted :: Monad m => Member (Embed m) r => Sem r ()+lifted = embed $ pure ()   newtype MyString = MyString String@@ -131,12 +131,12 @@    describe "Output effect" $ do     it "should unify recursively with tyvars" $ do-      flipShouldBe 11 . sum . fst . run . runFoldMapOutput id $ do+      flipShouldBe 11 . sum . fst . run . runOutputMonoid id $ do         output [1]         output $ replicate 2 5  -  describe "Lift effect" $ do+  describe "Embed effect" $ do     it "should interpret against IO" $ do       res <- runM lifted       res `shouldBe` ()
test/TypeErrors.hs view
@@ -22,7 +22,7 @@ -- ... Couldn't match expected type ...Sem r Bool... with actual type ...Bool... -- ... -- ... Couldn't match expected type ...Maybe a0...--- ... with actual type ...Sem r0 a1...+-- ... with actual type ...Sem r0 s0... -- ... missingFmap = ()