From f259f8ae7848f0ce3ec115310da31c234abe17c5 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 5 Jul 2019 14:14:45 -0400 Subject: [PATCH] Cleanup and document fundep plugin (#155) I made the code style agree with the rest of the codebase, and I wrote down everything I know about how this works. --- polysemy-plugin/polysemy-plugin.cabal | 5 +- polysemy-plugin/src/Polysemy/Plugin/Fundep.hs | 353 +++++++----------- .../src/Polysemy/Plugin/Fundep/Stuff.hs | 83 ++++ .../src/Polysemy/Plugin/Fundep/Unification.hs | 136 +++++++ .../src/Polysemy/Plugin/Fundep/Utils.hs | 33 ++ 5 files changed, 389 insertions(+), 221 deletions(-) create mode 100644 polysemy-plugin/src/Polysemy/Plugin/Fundep/Stuff.hs create mode 100644 polysemy-plugin/src/Polysemy/Plugin/Fundep/Unification.hs create mode 100644 polysemy-plugin/src/Polysemy/Plugin/Fundep/Utils.hs diff --git a/polysemy-plugin/polysemy-plugin.cabal b/polysemy-plugin/polysemy-plugin.cabal index dd59a86..da020b5 100644 --- a/polysemy-plugin/polysemy-plugin.cabal +++ b/polysemy-plugin/polysemy-plugin.cabal @@ -4,7 +4,7 @@ cabal-version: 1.12 -- -- see: https://github.com/sol/hpack -- --- hash: 63b03550f0fe1e13941505a11116fac8e6eef8a871dff51b30d2bca2263b2a75 +-- hash: b8d6dd19e90295689617adfecbd3bb83127b112840f4f304d956a4d5b33bf821 name: polysemy-plugin version: 0.2.2.0 @@ -31,6 +31,9 @@ library 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 diff --git a/polysemy-plugin/src/Polysemy/Plugin/Fundep.hs b/polysemy-plugin/src/Polysemy/Plugin/Fundep.hs index d99ebb2..fdf9e26 100644 --- a/polysemy-plugin/src/Polysemy/Plugin/Fundep.hs +++ b/polysemy-plugin/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,106 @@ -- ------------------------------------------------------------------------------ -- --- 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 - } - - -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") - } - fundepPlugin :: TcPlugin fundepPlugin = TcPlugin - { tcPluginInit = - (,) <$> tcPluginIO (newIORef S.empty) - <*> lookupEverything polysemyStuffLocations - , tcPluginSolve = solveFundep - , tcPluginStop = const (return ()) } + { tcPluginInit = + (,) <$> tcPluginIO (newIORef S.empty) + <*> polysemyStuff + , tcPluginSolve = solveFundep + , tcPluginStop = const $ pure () + } -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 +------------------------------------------------------------------------------ +-- | 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@ + } -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 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 + } + + +------------------------------------------------------------------------------ +-- | If there's only a single @Member@ in the same @r@ whose effect name +-- matches, return its effect (including tyvars.) +findMatchingEffectIfSingular + :: FindConstraint + -> [FindConstraint] + -> Maybe Type +findMatchingEffectIfSingular (FindConstraint _ eff_name _ r) ts = + singleListToJust $ do + FindConstraint _ eff_name' eff' r' <- ts + guard $ eqType eff_name eff_name' + guard $ eqType r r' + pure eff' + + +------------------------------------------------------------------------------ +-- | 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 - 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 - ] - - ------------------------------------------------------------------------------ --- | 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 = + :: 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) $ do (ev, _) <- unsafeTcPluginTcM . runTcSDeriveds - $ newWantedEq loc Nominal wanted given - pure ( (OrdType wanted, OrdType given) + $ newWantedEq (fcLoc fc) Nominal wanted given + pure ( Unification (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 + where + wanted = fcEffect fc ------------------------------------------------------------------------------ @@ -246,68 +134,93 @@ mustUnify (InterpreterUse b) = b 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. + Just eff' -> mkWanted fc FunctionDef 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/polysemy-plugin/src/Polysemy/Plugin/Fundep/Stuff.hs b/polysemy-plugin/src/Polysemy/Plugin/Fundep/Stuff.hs new file mode 100644 index 0000000..02c84b8 --- /dev/null +++ b/polysemy-plugin/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/polysemy-plugin/src/Polysemy/Plugin/Fundep/Unification.hs b/polysemy-plugin/src/Polysemy/Plugin/Fundep/Unification.hs new file mode 100644 index 0000000..5012ae1 --- /dev/null +++ b/polysemy-plugin/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/polysemy-plugin/src/Polysemy/Plugin/Fundep/Utils.hs b/polysemy-plugin/src/Polysemy/Plugin/Fundep/Utils.hs new file mode 100644 index 0000000..145b8c1 --- /dev/null +++ b/polysemy-plugin/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 +