diff --git a/ChangeLog.md b/ChangeLog.md --- a/ChangeLog.md +++ b/ChangeLog.md @@ -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` diff --git a/polysemy-plugin.cabal b/polysemy-plugin.cabal --- a/polysemy-plugin.cabal +++ b/polysemy-plugin.cabal @@ -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 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 diff --git a/src/Polysemy/Plugin/Fundep.hs b/src/Polysemy/Plugin/Fundep.hs --- a/src/Polysemy/Plugin/Fundep.hs +++ b/src/Polysemy/Plugin/Fundep.hs @@ -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 diff --git a/src/Polysemy/Plugin/Fundep/Stuff.hs b/src/Polysemy/Plugin/Fundep/Stuff.hs new file mode 100644 --- /dev/null +++ b/src/Polysemy/Plugin/Fundep/Stuff.hs @@ -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 + diff --git a/src/Polysemy/Plugin/Fundep/Unification.hs b/src/Polysemy/Plugin/Fundep/Unification.hs new file mode 100644 --- /dev/null +++ b/src/Polysemy/Plugin/Fundep/Unification.hs @@ -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) + diff --git a/src/Polysemy/Plugin/Fundep/Utils.hs b/src/Polysemy/Plugin/Fundep/Utils.hs new file mode 100644 --- /dev/null +++ b/src/Polysemy/Plugin/Fundep/Utils.hs @@ -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 + diff --git a/test/ExampleSpec.hs b/test/ExampleSpec.hs --- a/test/ExampleSpec.hs +++ b/test/ExampleSpec.hs @@ -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 diff --git a/test/LegitimateTypeErrorSpec.hs b/test/LegitimateTypeErrorSpec.hs --- a/test/LegitimateTypeErrorSpec.hs +++ b/test/LegitimateTypeErrorSpec.hs @@ -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 diff --git a/test/MultipleVarsSpec.hs b/test/MultipleVarsSpec.hs new file mode 100644 --- /dev/null +++ b/test/MultipleVarsSpec.hs @@ -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, ())) diff --git a/test/PluginSpec.hs b/test/PluginSpec.hs --- a/test/PluginSpec.hs +++ b/test/PluginSpec.hs @@ -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` () diff --git a/test/TypeErrors.hs b/test/TypeErrors.hs --- a/test/TypeErrors.hs +++ b/test/TypeErrors.hs @@ -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 = ()