{-# LANGUAGE CPP #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ViewPatterns #-}
module Polysemy.Plugin.Fundep (fundepPlugin) where
import Control.Monad
import Control.Monad.Trans.Class (lift)
import Control.Monad.Trans.State
import Data.Bifunctor
import Data.Coerce
import Data.Function (on)
import Data.IORef
import qualified Data.Map as M
import Data.Maybe
import Data.Set (Set)
import qualified Data.Set as S
import Data.Traversable (for)
import Polysemy.Plugin.Fundep.Stuff
import Polysemy.Plugin.Fundep.Unification
import Polysemy.Plugin.Fundep.Utils
#if __GLASGOW_HASKELL__ >= 906
#define SUBST Subst
#define GET_TYVAR getTyVar_maybe
import GHC.Core.TyCo.Subst (SUBST)
import GHC.Core.TyCo.Compare (eqType, nonDetCmpType)
#else
#define SUBST TCvSubst
#define GET_TYVAR tcGetTyVar_maybe
#endif
#if __GLASGOW_HASKELL__ >= 900
import GHC.Builtin.Types.Prim (alphaTys)
import GHC.Plugins (idType, tyConClass_maybe, ppr, Outputable, sep, text, (<+>), parens, emptyUFM)
import GHC.Tc.Types.Evidence
import GHC.Tc.Plugin (TcPluginM, tcPluginIO)
import GHC.Tc.Types
import GHC.Tc.Types.Constraint
import GHC.Tc.Utils.Env (tcGetInstEnvs)
import GHC.Tc.Utils.TcType (tcSplitPhiTy, tcSplitTyConApp, GET_TYVAR, tcSplitAppTy_maybe)
import GHC.Tc.Solver.Monad hiding (tcLookupClass)
import GHC.Core.Class (classTyCon)
import GHC.Core.InstEnv (lookupInstEnv, is_dfun)
import GHC.Core.Type
import GHC.Utils.Monad (allM, anyM)
#else
#if __GLASGOW_HASKELL__ >= 810
import Constraint
#endif
import Class (classTyCon)
import GhcPlugins (idType, tyConClass_maybe, ppr, Outputable, sep, text, (<+>), parens)
import Inst (tcGetInstEnvs)
import InstEnv (lookupInstEnv, is_dfun)
import MonadUtils (allM, anyM)
import TcEvidence
import TcPluginM (tcPluginIO)
import TcRnTypes
import TcType (tcSplitPhiTy, tcSplitTyConApp, GET_TYVAR, tcSplitAppTy_maybe)
import TcSMonad hiding (tcLookupClass)
import Type
import TysPrim (alphaTys)
#endif
fundepPlugin :: TcPlugin
fundepPlugin :: TcPlugin
fundepPlugin = TcPlugin
{ tcPluginInit :: TcPluginM (IORef (Set Unification), PolysemyStuff 'Things)
tcPluginInit =
(,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. IO a -> TcPluginM a
tcPluginIO (forall a. a -> IO (IORef a)
newIORef forall a. Set a
S.empty)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TcPluginM (PolysemyStuff 'Things)
polysemyStuff
, tcPluginSolve :: (IORef (Set Unification), PolysemyStuff 'Things) -> TcPluginSolver
tcPluginSolve = (IORef (Set Unification), PolysemyStuff 'Things) -> TcPluginSolver
solveFundep
, tcPluginStop :: (IORef (Set Unification), PolysemyStuff 'Things) -> TcPluginM ()
tcPluginStop = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
#if __GLASGOW_HASKELL__ >= 904
, tcPluginRewrite = \ _ -> emptyUFM
#endif
}
newtype PredType' = PredType' { PredType' -> PredType
getPredType :: PredType }
deriving newtype PredType' -> SDoc
forall a. (a -> SDoc) -> Outputable a
ppr :: PredType' -> SDoc
$cppr :: PredType' -> SDoc
Outputable
instance Eq PredType' where
== :: PredType' -> PredType' -> Bool
(==) = ((forall a. Eq a => a -> a -> Bool
== Ordering
EQ) forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => a -> a -> Ordering
compare
instance Ord PredType' where
compare :: PredType' -> PredType' -> Ordering
compare = PredType -> PredType -> Ordering
nonDetCmpType forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` PredType' -> PredType
getPredType
data FindConstraint = FindConstraint
{ FindConstraint -> CtLoc
fcLoc :: CtLoc
, FindConstraint -> PredType
fcEffectName :: Type
, FindConstraint -> PredType
fcEffect :: Type
, FindConstraint -> PredType
fcRow :: Type
}
instance Outputable FindConstraint where
ppr :: FindConstraint -> SDoc
ppr FindConstraint{CtLoc
PredType
fcRow :: PredType
fcEffect :: PredType
fcEffectName :: PredType
fcLoc :: CtLoc
fcRow :: FindConstraint -> PredType
fcEffect :: FindConstraint -> PredType
fcEffectName :: FindConstraint -> PredType
fcLoc :: FindConstraint -> CtLoc
..} = SDoc -> SDoc
parens forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
sep
[ String -> SDoc
text String
"effect name = " SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr PredType
fcEffectName
, String -> SDoc
text String
"effect = " SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr PredType
fcEffect
, String -> SDoc
text String
"row = " SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr PredType
fcRow
]
getFindConstraints :: PolysemyStuff 'Things -> [Ct] -> [FindConstraint]
getFindConstraints :: PolysemyStuff 'Things -> [Ct] -> [FindConstraint]
getFindConstraints (forall (l :: LookupState). PolysemyStuff l -> ThingOf l Class
findClass -> ThingOf 'Things Class
cls) [Ct]
cts = do
cd :: Ct
cd@CDictCan{cc_class :: Ct -> Class
cc_class = Class
cls', cc_tyargs :: Ct -> [PredType]
cc_tyargs = [PredType
eff, PredType
r]} <- [Ct]
cts
forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ ThingOf 'Things Class
cls forall a. Eq a => a -> a -> Bool
== Class
cls'
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ FindConstraint
{ fcLoc :: CtLoc
fcLoc = Ct -> CtLoc
ctLoc Ct
cd
, fcEffectName :: PredType
fcEffectName = PredType -> PredType
getEffName PredType
eff
, fcEffect :: PredType
fcEffect = PredType
eff
, fcRow :: PredType
fcRow = PredType
r
}
getExtraEvidence :: PolysemyStuff 'Things -> [Ct] -> [PredType]
PolysemyStuff 'Things
things [Ct]
cts = do
CDictCan{cc_class :: Ct -> Class
cc_class = Class
cls, cc_tyargs :: Ct -> [PredType]
cc_tyargs = [PredType]
as} <- [Ct]
cts
forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ Class
cls forall a. Eq a => a -> a -> Bool
/= forall (l :: LookupState). PolysemyStuff l -> ThingOf l Class
findClass PolysemyStuff 'Things
things
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ PredType -> [PredType] -> PredType
mkAppTys (TyCon -> PredType
mkTyConTy forall a b. (a -> b) -> a -> b
$ Class -> TyCon
classTyCon Class
cls) [PredType]
as
findMatchingEffectIfSingular
:: [PredType]
-> Set PredType'
-> FindConstraint
-> [FindConstraint]
-> TcM (Maybe Type)
findMatchingEffectIfSingular :: [PredType]
-> Set PredType'
-> FindConstraint
-> [FindConstraint]
-> TcM (Maybe PredType)
findMatchingEffectIfSingular
[PredType]
extra_wanted
Set PredType'
extra_given
(FindConstraint CtLoc
_ PredType
eff_name PredType
wanted PredType
r)
[FindConstraint]
ts =
let skolems :: Set TyVar
skolems = forall a. Ord a => [a] -> Set a
S.fromList forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (PredType -> [TyVar]
tyCoVarsOfTypeWellScoped forall b c a. (b -> c) -> (a -> b) -> a -> c
. FindConstraint -> PredType
fcEffect) [FindConstraint]
ts
results :: [(PredType, TCvSubst)]
results = do
FindConstraint CtLoc
_ PredType
eff_name' PredType
eff' PredType
r' <- [FindConstraint]
ts
forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ PredType -> PredType -> Bool
eqType PredType
eff_name PredType
eff_name'
forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ PredType -> PredType -> Bool
eqType PredType
r PredType
r'
TCvSubst
subst <- forall a. Maybe a -> [a]
maybeToList forall a b. (a -> b) -> a -> b
$ SolveContext -> PredType -> PredType -> Maybe TCvSubst
unify (Set TyVar -> SolveContext
FunctionDef Set TyVar
skolems) PredType
wanted PredType
eff'
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PredType
eff', TCvSubst
subst)
in case [(PredType, TCvSubst)]
results of
[] -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
[(PredType
a, TCvSubst
_)] -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just PredType
a
[(PredType, TCvSubst)]
_ ->
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. [a] -> Maybe a
singleListToJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Monad m => m (m a) -> m a
join) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [(PredType, TCvSubst)]
results forall a b. (a -> b) -> a -> b
$ \(PredType
eff, TCvSubst
subst) ->
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Maybe a -> [a]
maybeToList forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) a. Monad m => (a -> m Bool) -> [a] -> m Bool
anyM (Set PredType' -> TCvSubst -> PredType -> TcM Bool
checkExtraEvidence Set PredType'
extra_given TCvSubst
subst) [PredType]
extra_wanted forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Bool
True -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just PredType
eff
Bool
False -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
checkExtraEvidence ::
Set PredType' ->
SUBST ->
PredType ->
TcM Bool
Set PredType'
givens TCvSubst
subst = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT Set PredType'
givens forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredType -> StateT (Set PredType') TcM Bool
getInstance forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasCallStack => TCvSubst -> PredType -> PredType
substTy TCvSubst
subst
getEffName :: Type -> Type
getEffName :: PredType -> PredType
getEffName PredType
t = forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ PredType -> (PredType, [PredType])
splitAppTys PredType
t
mkWantedForce
:: FindConstraint
-> Type
-> TcPluginM (Unification, Ct)
mkWantedForce :: FindConstraint -> PredType -> TcPluginM (Unification, Ct)
mkWantedForce FindConstraint
fc PredType
given = do
#if __GLASGOW_HASKELL__ >= 904
((ev, _), _) <- unsafeTcPluginTcM
. runTcS
$ newWantedEq (fcLoc fc) emptyRewriterSet Nominal wanted given
#else
(CtEvidence
ev, Coercion
_) <- forall a. TcM a -> TcPluginM a
unsafeTcPluginTcM
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. TcS a -> TcM a
runTcSDeriveds
forall a b. (a -> b) -> a -> b
$ CtLoc -> Role -> PredType -> PredType -> TcS (CtEvidence, Coercion)
newWantedEq (FindConstraint -> CtLoc
fcLoc FindConstraint
fc) Role
Nominal PredType
wanted PredType
given
#endif
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( OrdType -> OrdType -> Unification
Unification (PredType -> OrdType
OrdType PredType
wanted) (PredType -> OrdType
OrdType PredType
given)
, CtEvidence -> Ct
CNonCanonical CtEvidence
ev
)
where
wanted :: PredType
wanted = FindConstraint -> PredType
fcEffect FindConstraint
fc
skolemsForInterpreter :: Type -> Set TyVar
skolemsForInterpreter :: PredType -> Set TyVar
skolemsForInterpreter PredType
ty =
case PredType -> Maybe (PredType, PredType)
tcSplitAppTy_maybe PredType
ty of
Just (GET_TYVAR -> Just skolem, _) -> S.singleton skolem
Maybe (PredType, PredType)
_ -> forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Monoid a => a
mempty forall a. a -> Set a
S.singleton forall a b. (a -> b) -> a -> b
$ GET_TYVAR ty
mkWanted
:: FindConstraint
-> SolveContext
-> Type
-> TcPluginM (Maybe (Unification, Ct))
mkWanted :: FindConstraint
-> SolveContext -> PredType -> TcPluginM (Maybe (Unification, Ct))
mkWanted FindConstraint
fc SolveContext
solve_ctx PredType
given = do
forall (m :: * -> *) (z :: * -> *) a.
(Monad m, Alternative z) =>
Bool -> m a -> m (z a)
whenA (Bool -> Bool
not (SolveContext -> Bool
mustUnify SolveContext
solve_ctx) Bool -> Bool -> Bool
|| forall a. Maybe a -> Bool
isJust (SolveContext -> PredType -> PredType -> Maybe TCvSubst
unify SolveContext
solve_ctx PredType
wanted PredType
given)) forall a b. (a -> b) -> a -> b
$
FindConstraint -> PredType -> TcPluginM (Unification, Ct)
mkWantedForce FindConstraint
fc PredType
given
where
wanted :: PredType
wanted = FindConstraint -> PredType
fcEffect FindConstraint
fc
exactlyOneWantedForR
:: [FindConstraint]
-> Type
-> Bool
exactlyOneWantedForR :: [FindConstraint] -> PredType -> Bool
exactlyOneWantedForR [FindConstraint]
wanteds
= forall a. a -> Maybe a -> a
fromMaybe Bool
False
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Map OrdType Bool
singular_r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredType -> OrdType
OrdType
where
singular_r :: Map OrdType Bool
singular_r = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (forall a. Eq a => a -> a -> Bool
/= Int
1))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Eq a => [a] -> [(a, Int)]
countLength
forall a b. (a -> b) -> a -> b
$ PredType -> OrdType
OrdType forall b c a. (b -> c) -> (a -> b) -> a -> c
. FindConstraint -> PredType
fcRow forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FindConstraint]
wanteds
getInstance :: PredType -> StateT (Set PredType') TcM Bool
getInstance :: PredType -> StateT (Set PredType') TcM Bool
getInstance PredType
predty = do
Set PredType'
givens <- forall (m :: * -> *) s. Monad m => StateT s m s
get
case forall a. Ord a => a -> Set a -> Bool
S.member (PredType -> PredType'
PredType' PredType
predty) Set PredType'
givens of
Bool
True -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
Bool
False ->
let (TyCon
con, [PredType]
apps) = PredType -> (TyCon, [PredType])
tcSplitTyConApp PredType
predty
in case TyCon -> Maybe Class
tyConClass_maybe TyCon
con of
Maybe Class
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
Just Class
cls -> do
InstEnvs
env <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TcM InstEnvs
tcGetInstEnvs
let ([InstMatch]
mres, [ClsInst]
_, [InstMatch]
_) = Bool
-> InstEnvs
-> Class
-> [PredType]
-> ([InstMatch], [ClsInst], [InstMatch])
lookupInstEnv Bool
False InstEnvs
env Class
cls [PredType]
apps
case [InstMatch]
mres of
((ClsInst
inst, [Maybe PredType]
mapps) : [InstMatch]
_) -> do
let df :: PredType
df = HasDebugCallStack => PredType -> [PredType] -> PredType
piResultTys (TyVar -> PredType
idType forall a b. (a -> b) -> a -> b
$ ClsInst -> TyVar
is_dfun ClsInst
inst)
forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall a. a -> Maybe a -> a
fromMaybe [PredType]
alphaTys [Maybe PredType]
mapps
let ([PredType]
theta, PredType
_) = PredType -> ([PredType], PredType)
tcSplitPhiTy PredType
df
forall (m :: * -> *) a. Monad m => (a -> m Bool) -> [a] -> m Bool
allM PredType -> StateT (Set PredType') TcM Bool
getInstance [PredType]
theta forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Bool
True -> do
forall (m :: * -> *) s. Monad m => (s -> s) -> StateT s m ()
modify forall a b. (a -> b) -> a -> b
$ forall a. Ord a => a -> Set a -> Set a
S.insert forall a b. (a -> b) -> a -> b
$ coerce :: forall a b. Coercible a b => a -> b
coerce PredType
predty
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
Bool
False -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
[InstMatch]
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
solveFundep
:: ( IORef (S.Set Unification)
, PolysemyStuff 'Things
)
#if __GLASGOW_HASKELL__ >= 904
-> EvBindsVar
-> [Ct]
-> [Ct]
-> TcPluginM TcPluginSolveResult
#else
-> [Ct]
-> [Ct]
-> [Ct]
-> TcPluginM TcPluginResult
#endif
solveFundep :: (IORef (Set Unification), PolysemyStuff 'Things) -> TcPluginSolver
solveFundep (IORef (Set Unification), PolysemyStuff 'Things)
_ [Ct]
_ [Ct]
_ [] = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ [(EvTerm, Ct)] -> [Ct] -> TcPluginResult
TcPluginOk [] []
#if __GLASGOW_HASKELL__ >= 904
solveFundep (ref, stuff) _ given wanted = do
#else
solveFundep (IORef (Set Unification)
ref, PolysemyStuff 'Things
stuff) [Ct]
given [Ct]
_ [Ct]
wanted = do
#endif
let wanted_finds :: [FindConstraint]
wanted_finds = PolysemyStuff 'Things -> [Ct] -> [FindConstraint]
getFindConstraints PolysemyStuff 'Things
stuff [Ct]
wanted
given_finds :: [FindConstraint]
given_finds = PolysemyStuff 'Things -> [Ct] -> [FindConstraint]
getFindConstraints PolysemyStuff 'Things
stuff [Ct]
given
extra_wanted :: [PredType]
extra_wanted = PolysemyStuff 'Things -> [Ct] -> [PredType]
getExtraEvidence PolysemyStuff 'Things
stuff [Ct]
wanted
extra_given :: Set PredType'
extra_given = forall a. Ord a => [a] -> Set a
S.fromList forall a b. (a -> b) -> a -> b
$ coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ PolysemyStuff 'Things -> [Ct] -> [PredType]
getExtraEvidence PolysemyStuff 'Things
stuff [Ct]
given
[Maybe (Unification, Ct)]
eqs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [FindConstraint]
wanted_finds forall a b. (a -> b) -> a -> b
$ \FindConstraint
fc -> do
let r :: PredType
r = FindConstraint -> PredType
fcRow FindConstraint
fc
Maybe PredType
res <- forall a. TcM a -> TcPluginM a
unsafeTcPluginTcM
forall a b. (a -> b) -> a -> b
$ [PredType]
-> Set PredType'
-> FindConstraint
-> [FindConstraint]
-> TcM (Maybe PredType)
findMatchingEffectIfSingular [PredType]
extra_wanted Set PredType'
extra_given FindConstraint
fc [FindConstraint]
given_finds
case Maybe PredType
res of
Just PredType
eff' -> forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FindConstraint -> PredType -> TcPluginM (Unification, Ct)
mkWantedForce FindConstraint
fc PredType
eff'
Maybe PredType
Nothing ->
case PredType -> (PredType, [PredType])
splitAppTys PredType
r of
(PredType
_, [PredType
_, PredType
eff', PredType
_]) ->
FindConstraint
-> SolveContext -> PredType -> TcPluginM (Maybe (Unification, Ct))
mkWanted FindConstraint
fc
(Bool -> Set TyVar -> SolveContext
InterpreterUse
([FindConstraint] -> PredType -> Bool
exactlyOneWantedForR [FindConstraint]
wanted_finds PredType
r)
(PredType -> Set TyVar
skolemsForInterpreter PredType
eff'))
PredType
eff'
(PredType, [PredType])
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
Set Unification
already_emitted <- forall a. IO a -> TcPluginM a
tcPluginIO forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef IORef (Set Unification)
ref
let ([Unification]
unifications, [Ct]
new_wanteds) = Set Unification -> [(Unification, Ct)] -> ([Unification], [Ct])
unzipNewWanteds Set Unification
already_emitted forall a b. (a -> b) -> a -> b
$ forall a. [Maybe a] -> [a]
catMaybes [Maybe (Unification, Ct)]
eqs
forall a. IO a -> TcPluginM a
tcPluginIO forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef (Set Unification)
ref forall a b. (a -> b) -> a -> b
$ forall a. Ord a => Set a -> Set a -> Set a
S.union forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> Set a
S.fromList [Unification]
unifications
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ [(EvTerm, Ct)] -> [Ct] -> TcPluginResult
TcPluginOk [] [Ct]
new_wanteds