{-# 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 :: Plugin
plugin = Names -> Plugin
makePlugin [(String
"effectful", String
"Effectful.Internal.Effect", String
":>")]
type Names = [(String, String, String)]
makePlugin :: Names -> Plugin
makePlugin :: Names -> Plugin
makePlugin Names
names = Plugin
defaultPlugin
{ tcPlugin :: TcPlugin
tcPlugin = forall a b. a -> b -> a
const (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Names -> TcPlugin
fakedep Names
names)
, pluginRecompile :: [String] -> IO PluginRecompile
pluginRecompile = [String] -> IO PluginRecompile
purePlugin
}
fakedep :: Names -> TcPlugin
fakedep :: Names -> TcPlugin
fakedep Names
names = TcPlugin
{ tcPluginInit :: TcPluginM ([Class], IORef VisitedSet)
tcPluginInit = Names -> TcPluginM ([Class], IORef VisitedSet)
initFakedep Names
names
, tcPluginSolve :: ([Class], IORef VisitedSet) -> TcPluginSolver
tcPluginSolve = ([Class], IORef VisitedSet) -> TcPluginSolver
solveFakedepForAllElemClasses
, tcPluginStop :: ([Class], IORef VisitedSet) -> TcPluginM ()
tcPluginStop = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ()
}
liftTc :: TcM a -> TcPluginM a
liftTc :: forall a. TcM a -> TcPluginM a
liftTc = forall a. TcM a -> TcPluginM a
unsafeTcPluginTcM
liftIo :: IO a -> TcPluginM a
liftIo :: forall a. IO a -> TcPluginM a
liftIo = forall a. IO a -> TcPluginM a
tcPluginIO
type VisitedSet = Set (OrdType, OrdType)
initFakedep :: Names -> TcPluginM ([Class], IORef VisitedSet)
initFakedep :: Names -> TcPluginM ([Class], IORef VisitedSet)
initFakedep Names
names = do
[Class]
classes <- forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for Names
names \(String
packageName, String
elemModuleName, String
elemClassName) -> do
Module
recMod <- ModuleName -> FastString -> TcPluginM Module
lookupModule (String -> ModuleName
mkModuleName String
elemModuleName) forall a b. (a -> b) -> a -> b
$ String -> FastString
fsLit String
packageName
Name
nm <- Module -> OccName -> TcPluginM Name
lookupName Module
recMod forall a b. (a -> b) -> a -> b
$ String -> OccName
mkTcOcc String
elemClassName
Name -> TcPluginM Class
tcLookupClass Name
nm
IORef VisitedSet
visited <- forall a. IO a -> TcPluginM a
liftIo forall a b. (a -> b) -> a -> b
$ forall a. a -> IO (IORef a)
newIORef forall a. Set a
Set.empty
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ([Class]
classes, IORef VisitedSet
visited)
data FakedepGiven = FakedepGiven
{ FakedepGiven -> Type
givenEffHead :: Type
, FakedepGiven -> Type
givenEff :: Type
, FakedepGiven -> Type
givenEs :: Type
}
instance Show FakedepGiven where
show :: FakedepGiven -> String
show (FakedepGiven Type
_ Type
e Type
es) = String
"(Elem " forall a. Semigroup a => a -> a -> a
<> SDoc -> String
showSDocUnsafe (forall a. Outputable a => a -> SDoc
ppr Type
e) forall a. Semigroup a => a -> a -> a
<> String
" " forall a. Semigroup a => a -> a -> a
<> SDoc -> String
showSDocUnsafe (forall a. Outputable a => a -> SDoc
ppr Type
es) forall a. Semigroup a => a -> a -> a
<> String
")"
data FakedepWanted = FakedepWanted FakedepGiven CtLoc
instance Show FakedepWanted where
show :: FakedepWanted -> String
show (FakedepWanted FakedepGiven
given CtLoc
_) = forall a. Show a => a -> String
show FakedepGiven
given
newtype OrdType = OrdType { OrdType -> Type
unOrdType :: Type }
instance Eq OrdType where
== :: OrdType -> OrdType -> Bool
(==) = Type -> Type -> Bool
eqType forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` OrdType -> Type
unOrdType
instance Ord OrdType where
compare :: OrdType -> OrdType -> Ordering
compare = Type -> Type -> Ordering
nonDetCmpType forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` OrdType -> Type
unOrdType
solveFakedepForAllElemClasses :: ([Class], IORef VisitedSet) -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult
solveFakedepForAllElemClasses :: ([Class], IORef VisitedSet) -> TcPluginSolver
solveFakedepForAllElemClasses ([Class]
elemClasses, IORef VisitedSet
visitedRef) [Ct]
givens [Ct]
_ [Ct]
wanteds = do
[Ct]
solns <- forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Class]
elemClasses \Class
elemCls -> (Class, IORef VisitedSet) -> [Ct] -> [Ct] -> TcPluginM [Ct]
solveFakedep (Class
elemCls, IORef VisitedSet
visitedRef) [Ct]
givens [Ct]
wanteds
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ [(EvTerm, Ct)] -> [Ct] -> TcPluginResult
TcPluginOk [] [Ct]
solns
solveFakedep :: (Class, IORef VisitedSet) -> [Ct] -> [Ct] -> TcPluginM [Ct]
solveFakedep :: (Class, IORef VisitedSet) -> [Ct] -> [Ct] -> TcPluginM [Ct]
solveFakedep (Class, IORef VisitedSet)
_ [Ct]
_ [] = forall (f :: Type -> Type) a. Applicative f => a -> f a
pure []
solveFakedep (Class
elemCls, IORef VisitedSet
visitedRef) [Ct]
allGivens [Ct]
allWanteds = do
let
givens :: [FakedepGiven]
givens = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Ct -> Maybe FakedepGiven
relevantGiven [Ct]
allGivens
wanteds :: [FakedepWanted]
wanteds = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Ct -> Maybe FakedepWanted
relevantWanted [Ct]
allWanteds
allGivenTypes :: [Type]
allGivenTypes = Ct -> Type
ctPred forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Ct]
allGivens
extraWanteds :: [Type]
extraWanteds = Ct -> Type
ctPred forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. (a -> Bool) -> [a] -> [a]
filter Ct -> Bool
irrelevant [Ct]
allWanteds
InstEnvs
globals <- forall a. TcM a -> TcPluginM a
liftTc TcM InstEnvs
tcGetInstEnvs
let solns :: [(FakedepWanted, FakedepGiven)]
solns = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (InstEnvs
-> [Type]
-> [Type]
-> [FakedepGiven]
-> FakedepWanted
-> Maybe (FakedepWanted, FakedepGiven)
solve InstEnvs
globals [Type]
allGivenTypes [Type]
extraWanteds [FakedepGiven]
givens) [FakedepWanted]
wanteds
[(Ct, (OrdType, OrdType))]
eqns <- forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [(FakedepWanted, FakedepGiven)]
solns \(FakedepWanted (FakedepGiven Type
_ Type
goalEff Type
_) CtLoc
loc, FakedepGiven Type
_ Type
solnEff Type
_) -> do
(CtEvidence
eqn, Coercion
_) <- forall a. TcM a -> TcPluginM a
liftTc forall a b. (a -> b) -> a -> b
$ forall a. TcS a -> TcM a
runTcSDeriveds forall a b. (a -> b) -> a -> b
$ CtLoc -> Role -> Type -> Type -> TcS (CtEvidence, Coercion)
newWantedEq CtLoc
loc Role
Nominal Type
goalEff Type
solnEff
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (CtEvidence -> Ct
CNonCanonical CtEvidence
eqn, (Type -> OrdType
OrdType Type
goalEff, Type -> OrdType
OrdType Type
solnEff))
VisitedSet
visitedSolnPairs <- forall a. IO a -> TcPluginM a
liftIo forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef IORef VisitedSet
visitedRef
let solnEqns :: [Ct]
solnEqns = forall a b. (a, b) -> a
fst forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. (a -> Bool) -> [a] -> [a]
filter [(Ct, (OrdType, OrdType))]
eqns \(Ct
_, (OrdType, OrdType)
pair) -> forall a. Ord a => a -> Set a -> Bool
Set.notMember (OrdType, OrdType)
pair VisitedSet
visitedSolnPairs
forall a. IO a -> TcPluginM a
liftIo forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef VisitedSet
visitedRef (forall a. Ord a => Set a -> Set a -> Set a
Set.union forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> b
snd forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Ct, (OrdType, OrdType))]
eqns)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure [Ct]
solnEqns
where
solve :: InstEnvs -> [PredType] -> [PredType] -> [FakedepGiven] -> FakedepWanted -> Maybe (FakedepWanted, FakedepGiven)
solve :: InstEnvs
-> [Type]
-> [Type]
-> [FakedepGiven]
-> FakedepWanted
-> Maybe (FakedepWanted, FakedepGiven)
solve InstEnvs
globals [Type]
allGivenTypes [Type]
extraWanteds [FakedepGiven]
givens goal :: FakedepWanted
goal@(FakedepWanted (FakedepGiven Type
_ Type
_ Type
goalEs) CtLoc
_) =
let
cands :: [FakedepGiven]
cands = Type -> Type -> [FakedepGiven]
extractExtraGivens Type
goalEs Type
goalEs forall a. Semigroup a => a -> a -> a
<> [FakedepGiven]
givens
unifiableCands :: [(FakedepGiven, TCvSubst)]
unifiableCands = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (FakedepWanted -> FakedepGiven -> Maybe (FakedepGiven, TCvSubst)
unifiableWith FakedepWanted
goal) [FakedepGiven]
cands
in case [(FakedepGiven, TCvSubst)]
unifiableCands of
[(FakedepGiven
soln, TCvSubst
_)] -> forall a. a -> Maybe a
Just (FakedepWanted
goal, FakedepGiven
soln)
[(FakedepGiven, TCvSubst)]
_ ->
let satisfiableCands :: [(FakedepGiven, TCvSubst)]
satisfiableCands = forall a. (a -> Bool) -> [a] -> [a]
filter (InstEnvs -> [Type] -> [Type] -> (FakedepGiven, TCvSubst) -> Bool
satisfiable InstEnvs
globals [Type]
allGivenTypes [Type]
extraWanteds) [(FakedepGiven, TCvSubst)]
unifiableCands
in case [(FakedepGiven, TCvSubst)]
satisfiableCands of
[(FakedepGiven
soln, TCvSubst
_)] -> forall a. a -> Maybe a
Just (FakedepWanted
goal, FakedepGiven
soln)
[(FakedepGiven, TCvSubst)]
_ -> forall a. Maybe a
Nothing
extractExtraGivens :: Type -> Type -> [FakedepGiven]
extractExtraGivens :: Type -> Type -> [FakedepGiven]
extractExtraGivens Type
fullEs Type
es = case Type -> (Type, [Type])
splitAppTys Type
es of
(Type
_colon, [Type
_kind, Type
e, Type
es']) ->
let (Type
dtHead, [Type]
_tyArgs) = Type -> (Type, [Type])
splitAppTys Type
e
in Type -> Type -> Type -> FakedepGiven
FakedepGiven Type
dtHead Type
e Type
fullEs forall a. a -> [a] -> [a]
: Type -> Type -> [FakedepGiven]
extractExtraGivens Type
fullEs Type
es'
(Type, [Type])
_ -> []
relevantGiven :: Ct -> Maybe FakedepGiven
relevantGiven :: Ct -> Maybe FakedepGiven
relevantGiven (CDictCan CtEvidence
_ Class
cls [Type
_kind, Type
eff, Type
es] Bool
_)
| Class
cls forall a. Eq a => a -> a -> Bool
== Class
elemCls = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type -> FakedepGiven
FakedepGiven (forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ Type -> (Type, [Type])
splitAppTys Type
eff) Type
eff Type
es
relevantGiven (CDictCan CtEvidence
_ Class
cls [Type
eff, Type
es] Bool
_)
| Class
cls forall a. Eq a => a -> a -> Bool
== Class
elemCls = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type -> FakedepGiven
FakedepGiven (forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ Type -> (Type, [Type])
splitAppTys Type
eff) Type
eff Type
es
relevantGiven Ct
_ = forall a. Maybe a
Nothing
relevantWanted :: Ct -> Maybe FakedepWanted
relevantWanted :: Ct -> Maybe FakedepWanted
relevantWanted (CDictCan (CtWanted Type
_ TcEvDest
_ ShadowInfo
_ CtLoc
loc) Class
cls [Type
_kind, Type
eff, Type
es] Bool
_)
| Class
cls forall a. Eq a => a -> a -> Bool
== Class
elemCls = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ FakedepGiven -> CtLoc -> FakedepWanted
FakedepWanted (Type -> Type -> Type -> FakedepGiven
FakedepGiven (forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ Type -> (Type, [Type])
splitAppTys Type
eff) Type
eff Type
es) CtLoc
loc
relevantWanted (CDictCan (CtWanted Type
_ TcEvDest
_ ShadowInfo
_ CtLoc
loc) Class
cls [Type
eff, Type
es] Bool
_)
| Class
cls forall a. Eq a => a -> a -> Bool
== Class
elemCls = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ FakedepGiven -> CtLoc -> FakedepWanted
FakedepWanted (Type -> Type -> Type -> FakedepGiven
FakedepGiven (forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ Type -> (Type, [Type])
splitAppTys Type
eff) Type
eff Type
es) CtLoc
loc
relevantWanted Ct
_ = forall a. Maybe a
Nothing
irrelevant :: Ct -> Bool
irrelevant :: Ct -> Bool
irrelevant = forall a. Maybe a -> Bool
isNothing forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> Maybe FakedepGiven
relevantGiven
unifiableWith :: FakedepWanted -> FakedepGiven -> Maybe (FakedepGiven, TCvSubst)
unifiableWith :: FakedepWanted -> FakedepGiven -> Maybe (FakedepGiven, TCvSubst)
unifiableWith (FakedepWanted FakedepGiven
goal CtLoc
_) FakedepGiven
cand =
if FakedepGiven -> Type
givenEs FakedepGiven
goal Type -> Type -> Bool
`eqType` FakedepGiven -> Type
givenEs FakedepGiven
cand Bool -> Bool -> Bool
&& FakedepGiven -> Type
givenEffHead FakedepGiven
goal Type -> Type -> Bool
`eqType` FakedepGiven -> Type
givenEffHead FakedepGiven
cand
then (FakedepGiven
cand, ) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Type -> Maybe TCvSubst
tcUnifyTy (FakedepGiven -> Type
givenEff FakedepGiven
goal) (FakedepGiven -> Type
givenEff FakedepGiven
cand)
else forall a. Maybe a
Nothing
satisfiable :: InstEnvs -> [PredType] -> [PredType] -> (FakedepGiven, TCvSubst) -> Bool
satisfiable :: InstEnvs -> [Type] -> [Type] -> (FakedepGiven, TCvSubst) -> Bool
satisfiable InstEnvs
globals [Type]
givens [Type]
wanteds (FakedepGiven
_, TCvSubst
subst) =
let
wantedsInst :: [Type]
wantedsInst = HasCallStack => TCvSubst -> [Type] -> [Type]
substTys TCvSubst
subst [Type]
wanteds
givensInst :: Set OrdType
givensInst = forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ Type -> OrdType
OrdType forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> HasCallStack => TCvSubst -> [Type] -> [Type]
substTys TCvSubst
subst [Type]
givens
in forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Bool
all [Type]
wantedsInst \Type
want ->
if forall a. Ord a => a -> Set a -> Bool
Set.member (Type -> OrdType
OrdType Type
want) Set OrdType
givensInst then Bool
True
else let (TyCon
con, [Type]
args) = Type -> (TyCon, [Type])
tcSplitTyConApp Type
want
in case TyCon -> Maybe Class
tyConClass_maybe TyCon
con of
Maybe Class
Nothing -> Bool
False
Just Class
cls -> let ([InstMatch]
res, [ClsInst]
_, [InstMatch]
_) = Bool
-> InstEnvs
-> Class
-> [Type]
-> ([InstMatch], [ClsInst], [InstMatch])
lookupInstEnv Bool
False InstEnvs
globals Class
cls [Type]
args in Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null [InstMatch]
res