{-# LANGUAGE CPP #-}
module Effectful.Plugin (plugin) where

import Data.Either
import Data.Function
import Data.IORef
import Data.Maybe
import Data.Set (Set)
import Data.Set qualified as Set
import Data.Traversable

import GHC.Core.Class (Class)
import GHC.Core.InstEnv (InstEnvs, lookupInstEnv)
import GHC.Core.TyCo.Rep (PredType, Type)
import GHC.Core.TyCo.Subst
import GHC.Core.TyCon (tyConClass_maybe)
import GHC.Core.Type (splitAppTys)
import GHC.Core.Unify (tcUnifyTy)
import GHC.Driver.Config.Finder (initFinderOpts)
import GHC.Driver.Env (hsc_home_unit, hsc_units)
import GHC.Driver.Env.Types (HscEnv (..))
import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin)
import GHC.Tc.Plugin (getTopEnv, lookupOrig, tcLookupClass, tcPluginIO)
import GHC.Tc.Solver.Monad (newWantedEq, runTcSEarlyAbort)
import GHC.Tc.Types
  ( TcPlugin (..)
  , TcPluginM
  , TcPluginSolveResult (..)
  , unsafeTcPluginTcM
  )
import GHC.Tc.Types.Constraint
  ( Ct (..)
  , CtEvidence (..)
  , CtLoc
#if __GLASGOW_HASKELL__ >= 908
  , DictCt (..)
#endif
  , ctPred
  , emptyRewriterSet
  )
import GHC.Tc.Types.Evidence (EvBindsVar, Role (..))
import GHC.Tc.Utils.Env (tcGetInstEnvs)
import GHC.Tc.Utils.TcType (tcSplitTyConApp, eqType, nonDetCmpType)
import GHC.Types.Name (mkTcOcc)
import GHC.Types.Unique.FM (emptyUFM)
import GHC.Unit.Finder (FindResult (..), findPluginModule)
import GHC.Unit.Module (Module, ModuleName, mkModuleName)
import GHC.Utils.Outputable (Outputable (..), showSDocUnsafe)

#if __GLASGOW_HASKELL__ >= 906
type TCvSubst = Subst
#endif

plugin :: Plugin
plugin :: Plugin
plugin = Plugin
defaultPlugin
  { tcPlugin = \[CommandLineOption]
_ -> TcPlugin -> Maybe TcPlugin
forall a. a -> Maybe a
Just TcPlugin
    { tcPluginInit :: TcPluginM (Class, IORef VisitedSet)
tcPluginInit = TcPluginM (Class, IORef VisitedSet)
initPlugin
    , tcPluginRewrite :: (Class, IORef VisitedSet) -> UniqFM TyCon TcPluginRewriter
tcPluginRewrite = \(Class, IORef VisitedSet)
_ -> UniqFM TyCon TcPluginRewriter
forall key elt. UniqFM key elt
emptyUFM
    , tcPluginSolve :: (Class, IORef VisitedSet) -> TcPluginSolver
tcPluginSolve = (Class, IORef VisitedSet) -> TcPluginSolver
solveFakedep
    , tcPluginStop :: (Class, IORef VisitedSet) -> TcPluginM ()
tcPluginStop = \(Class, IORef VisitedSet)
_ -> () -> TcPluginM ()
forall a. a -> TcPluginM a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ()
    }
  , pluginRecompile = purePlugin
  }

----------------------------------------

data EffGiven = EffGiven
  { EffGiven -> Type
givenEffHead :: Type
  , EffGiven -> Type
givenEff :: Type
  , EffGiven -> Type
givenEs :: Type
  }

instance Show EffGiven where
  show :: EffGiven -> CommandLineOption
show (EffGiven Type
_ Type
e Type
es) =
    CommandLineOption
"[G] " CommandLineOption -> ShowS
forall a. [a] -> [a] -> [a]
++ SDoc -> CommandLineOption
showSDocUnsafe (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
e) CommandLineOption -> ShowS
forall a. Semigroup a => a -> a -> a
<> CommandLineOption
" :> " CommandLineOption -> ShowS
forall a. Semigroup a => a -> a -> a
<> SDoc -> CommandLineOption
showSDocUnsafe (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
es)

data EffWanted = EffWanted
  { EffWanted -> Type
wantedEffHead :: Type
  , EffWanted -> Type
wantedEff :: Type
  , EffWanted -> Type
wantedEs :: Type
  , EffWanted -> CtLoc
wantedLoc :: CtLoc
  }

instance Show EffWanted where
  show :: EffWanted -> CommandLineOption
show (EffWanted Type
_ Type
e Type
es CtLoc
_) =
    CommandLineOption
"[W] " CommandLineOption -> ShowS
forall a. Semigroup a => a -> a -> a
<> SDoc -> CommandLineOption
showSDocUnsafe (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
e) CommandLineOption -> ShowS
forall a. Semigroup a => a -> a -> a
<> CommandLineOption
" :> " CommandLineOption -> ShowS
forall a. Semigroup a => a -> a -> a
<> SDoc -> CommandLineOption
showSDocUnsafe (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
es)

newtype OrdType = OrdType {OrdType -> Type
unOrdType :: Type}

instance Eq OrdType where
  == :: OrdType -> OrdType -> Bool
(==) = Type -> Type -> Bool
eqType (Type -> Type -> Bool)
-> (OrdType -> Type) -> OrdType -> OrdType -> Bool
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 (Type -> Type -> Ordering)
-> (OrdType -> Type) -> OrdType -> OrdType -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` OrdType -> Type
unOrdType

----------------------------------------

type VisitedSet = Set (OrdType, OrdType)

initPlugin :: TcPluginM (Class, IORef VisitedSet)
initPlugin :: TcPluginM (Class, IORef VisitedSet)
initPlugin = do
  Module
recMod <- ModuleName -> TcPluginM Module
lookupModule (ModuleName -> TcPluginM Module) -> ModuleName -> TcPluginM Module
forall a b. (a -> b) -> a -> b
$ CommandLineOption -> ModuleName
mkModuleName CommandLineOption
"Effectful.Internal.Effect"
  Class
cls <- Name -> TcPluginM Class
tcLookupClass (Name -> TcPluginM Class) -> TcPluginM Name -> TcPluginM Class
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< Module -> OccName -> TcPluginM Name
lookupOrig Module
recMod (CommandLineOption -> OccName
mkTcOcc CommandLineOption
":>")
  IORef VisitedSet
visited <- IO (IORef VisitedSet) -> TcPluginM (IORef VisitedSet)
forall a. IO a -> TcPluginM a
tcPluginIO (IO (IORef VisitedSet) -> TcPluginM (IORef VisitedSet))
-> IO (IORef VisitedSet) -> TcPluginM (IORef VisitedSet)
forall a b. (a -> b) -> a -> b
$ VisitedSet -> IO (IORef VisitedSet)
forall a. a -> IO (IORef a)
newIORef VisitedSet
forall a. Set a
Set.empty
  (Class, IORef VisitedSet) -> TcPluginM (Class, IORef VisitedSet)
forall a. a -> TcPluginM a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Class
cls, IORef VisitedSet
visited)
  where
    lookupModule :: ModuleName -> TcPluginM Module
    lookupModule :: ModuleName -> TcPluginM Module
lookupModule ModuleName
mod_nm = do
      HscEnv
hsc_env <- TcPluginM HscEnv
getTopEnv
      let dflags :: DynFlags
dflags = HscEnv -> DynFlags
hsc_dflags HscEnv
hsc_env
          fopts :: FinderOpts
fopts = DynFlags -> FinderOpts
initFinderOpts DynFlags
dflags
          fc :: FinderCache
fc = HscEnv -> FinderCache
hsc_FC HscEnv
hsc_env
          units :: UnitState
units = (() :: Constraint) => HscEnv -> UnitState
HscEnv -> UnitState
hsc_units HscEnv
hsc_env
          home_unit :: HomeUnit
home_unit = HscEnv -> HomeUnit
hsc_home_unit HscEnv
hsc_env
      IO FindResult -> TcPluginM FindResult
forall a. IO a -> TcPluginM a
tcPluginIO (FinderCache
-> FinderOpts
-> UnitState
-> Maybe HomeUnit
-> ModuleName
-> IO FindResult
findPluginModule FinderCache
fc FinderOpts
fopts UnitState
units (HomeUnit -> Maybe HomeUnit
forall a. a -> Maybe a
Just HomeUnit
home_unit) ModuleName
mod_nm) TcPluginM FindResult
-> (FindResult -> TcPluginM Module) -> TcPluginM Module
forall a b. TcPluginM a -> (a -> TcPluginM b) -> TcPluginM b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Found ModLocation
_ Module
md -> Module -> TcPluginM Module
forall a. a -> TcPluginM a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Module
md
        FindResult
_ -> CommandLineOption -> TcPluginM Module
forall a. CommandLineOption -> a
errorWithoutStackTrace CommandLineOption
"Please add effectful-core to the list of dependencies."

solveFakedep
  :: (Class, IORef VisitedSet)
  -> EvBindsVar
  -> [Ct]
  -> [Ct]
  -> TcPluginM TcPluginSolveResult
solveFakedep :: (Class, IORef VisitedSet) -> TcPluginSolver
solveFakedep (Class
elemCls, IORef VisitedSet
visitedRef) EvBindsVar
_ [Ct]
allGivens [Ct]
allWanteds = do
  -- We're given two lists of constraints here:
  --
  -- - 'allGivens' are constraints already in our context,
  --
  -- - 'allWanteds' are constraints that need to be solved.
  --
  -- In the following notes, the words "give/given" and "want/wanted" all refer
  -- to this specific technical concept: given constraints are those that we can
  -- use, and wanted constraints are those that we need to solve.

  --tcPluginIO $ do
  --  putStrLn $ "Givens: " <> show (showSDocUnsafe . ppr <$> allGivens)
  --  putStrLn $ "Wanteds: " <> show (showSDocUnsafe . ppr <$> allWanteds)

  -- For each 'e :> es' we /want/ to solve (the "goal"), we need to eventually
  -- correspond it to another unique /given/ 'e :> es' that will make the
  -- program typecheck (the "solution").
  InstEnvs
globals <- TcM InstEnvs -> TcPluginM InstEnvs
forall a. TcM a -> TcPluginM a
unsafeTcPluginTcM TcM InstEnvs
tcGetInstEnvs
  let solns :: [(EffWanted, EffGiven)]
solns = (EffWanted -> Maybe (EffWanted, EffGiven))
-> [EffWanted] -> [(EffWanted, EffGiven)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (InstEnvs -> EffWanted -> Maybe (EffWanted, EffGiven)
solve InstEnvs
globals) [EffWanted]
effWanteds

  -- Now we need to tell GHC the solutions. The way we do this is to generate a
  -- new equality constraint, like 'State e ~ State Int', so that GHC's
  -- constraint solver will know that 'e' must be 'Int'.
  [(Ct, (OrdType, OrdType))]
eqns <- [(EffWanted, EffGiven)]
-> ((EffWanted, EffGiven) -> TcPluginM (Ct, (OrdType, OrdType)))
-> TcPluginM [(Ct, (OrdType, OrdType))]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [(EffWanted, EffGiven)]
solns (((EffWanted, EffGiven) -> TcPluginM (Ct, (OrdType, OrdType)))
 -> TcPluginM [(Ct, (OrdType, OrdType))])
-> ((EffWanted, EffGiven) -> TcPluginM (Ct, (OrdType, OrdType)))
-> TcPluginM [(Ct, (OrdType, OrdType))]
forall a b. (a -> b) -> a -> b
$ \(EffWanted
goal, EffGiven
soln) -> do
    let wantedEq :: TcS (CtEvidence, Coercion)
wantedEq = CtLoc
-> RewriterSet
-> Role
-> Type
-> Type
-> TcS (CtEvidence, Coercion)
newWantedEq (EffWanted -> CtLoc
wantedLoc EffWanted
goal) RewriterSet
emptyRewriterSet Role
Nominal
                               (EffWanted -> Type
wantedEff EffWanted
goal) (EffGiven -> Type
givenEff EffGiven
soln)
    (CtEvidence
eqn, Coercion
_) <- TcM (CtEvidence, Coercion) -> TcPluginM (CtEvidence, Coercion)
forall a. TcM a -> TcPluginM a
unsafeTcPluginTcM (TcM (CtEvidence, Coercion) -> TcPluginM (CtEvidence, Coercion))
-> TcM (CtEvidence, Coercion) -> TcPluginM (CtEvidence, Coercion)
forall a b. (a -> b) -> a -> b
$ TcS (CtEvidence, Coercion) -> TcM (CtEvidence, Coercion)
forall a. TcS a -> TcM a
runTcSEarlyAbort TcS (CtEvidence, Coercion)
wantedEq
    (Ct, (OrdType, OrdType)) -> TcPluginM (Ct, (OrdType, OrdType))
forall a. a -> TcPluginM a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (CtEvidence -> Ct
CNonCanonical CtEvidence
eqn, (Type -> OrdType
OrdType (Type -> OrdType) -> Type -> OrdType
forall a b. (a -> b) -> a -> b
$ EffWanted -> Type
wantedEff EffWanted
goal, Type -> OrdType
OrdType (Type -> OrdType) -> Type -> OrdType
forall a b. (a -> b) -> a -> b
$ EffGiven -> Type
givenEff EffGiven
soln))

  -- For any solution we've generated, we need to be careful not to generate it
  -- again, or we might end up generating infinitely many solutions. So, we
  -- record any already generated solution in a set.
  VisitedSet
visitedSolnPairs <- IO VisitedSet -> TcPluginM VisitedSet
forall a. IO a -> TcPluginM a
tcPluginIO (IO VisitedSet -> TcPluginM VisitedSet)
-> IO VisitedSet -> TcPluginM VisitedSet
forall a b. (a -> b) -> a -> b
$ IORef VisitedSet -> IO VisitedSet
forall a. IORef a -> IO a
readIORef IORef VisitedSet
visitedRef
  let solnEqns :: [Ct]
solnEqns = ((Ct, (OrdType, OrdType)) -> Ct)
-> [(Ct, (OrdType, OrdType))] -> [Ct]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Ct, (OrdType, OrdType)) -> Ct
forall a b. (a, b) -> a
fst ([(Ct, (OrdType, OrdType))] -> [Ct])
-> (((Ct, (OrdType, OrdType)) -> Bool)
    -> [(Ct, (OrdType, OrdType))])
-> ((Ct, (OrdType, OrdType)) -> Bool)
-> [Ct]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((Ct, (OrdType, OrdType)) -> Bool)
 -> [(Ct, (OrdType, OrdType))] -> [(Ct, (OrdType, OrdType))])
-> [(Ct, (OrdType, OrdType))]
-> ((Ct, (OrdType, OrdType)) -> Bool)
-> [(Ct, (OrdType, OrdType))]
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Ct, (OrdType, OrdType)) -> Bool)
-> [(Ct, (OrdType, OrdType))] -> [(Ct, (OrdType, OrdType))]
forall a. (a -> Bool) -> [a] -> [a]
filter [(Ct, (OrdType, OrdType))]
eqns (((Ct, (OrdType, OrdType)) -> Bool) -> [Ct])
-> ((Ct, (OrdType, OrdType)) -> Bool) -> [Ct]
forall a b. (a -> b) -> a -> b
$ \(Ct
_, (OrdType, OrdType)
pair) -> (OrdType, OrdType) -> VisitedSet -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.notMember (OrdType, OrdType)
pair VisitedSet
visitedSolnPairs
  IO () -> TcPluginM ()
forall a. IO a -> TcPluginM a
tcPluginIO (IO () -> TcPluginM ()) -> IO () -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ do
    IORef VisitedSet -> (VisitedSet -> VisitedSet) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef VisitedSet
visitedRef (VisitedSet -> VisitedSet -> VisitedSet
forall a. Ord a => Set a -> Set a -> Set a
Set.union (VisitedSet -> VisitedSet -> VisitedSet)
-> VisitedSet -> VisitedSet -> VisitedSet
forall a b. (a -> b) -> a -> b
$ [(OrdType, OrdType)] -> VisitedSet
forall a. Ord a => [a] -> Set a
Set.fromList ([(OrdType, OrdType)] -> VisitedSet)
-> [(OrdType, OrdType)] -> VisitedSet
forall a b. (a -> b) -> a -> b
$ ((Ct, (OrdType, OrdType)) -> (OrdType, OrdType))
-> [(Ct, (OrdType, OrdType))] -> [(OrdType, OrdType)]
forall a b. (a -> b) -> [a] -> [b]
map (Ct, (OrdType, OrdType)) -> (OrdType, OrdType)
forall a b. (a, b) -> b
snd [(Ct, (OrdType, OrdType))]
eqns)
    --putStrLn $ "Emitting: " <> showSDocUnsafe (ppr solnEqns)

  TcPluginSolveResult -> TcPluginM TcPluginSolveResult
forall a. a -> TcPluginM a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TcPluginSolveResult -> TcPluginM TcPluginSolveResult)
-> TcPluginSolveResult -> TcPluginM TcPluginSolveResult
forall a b. (a -> b) -> a -> b
$ [Ct] -> [(EvTerm, Ct)] -> [Ct] -> TcPluginSolveResult
TcPluginSolveResult [] [] [Ct]
solnEqns
  where
    -- The only type of constraint we're interested in solving are 'e :> es'
    -- constraints. Therefore, we extract these constraints out of the
    -- 'allGivens' and 'allWanted's.
    effGivens :: [EffGiven]
effGivens = (Ct -> Maybe EffGiven) -> [Ct] -> [EffGiven]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Ct -> Maybe EffGiven
maybeEffGiven [Ct]
allGivens
    ([Type]
otherWantedTys, [EffWanted]
effWanteds) = [Either Type EffWanted] -> ([Type], [EffWanted])
forall a b. [Either a b] -> ([a], [b])
partitionEithers ([Either Type EffWanted] -> ([Type], [EffWanted]))
-> [Either Type EffWanted] -> ([Type], [EffWanted])
forall a b. (a -> b) -> a -> b
$ (Ct -> Either Type EffWanted) -> [Ct] -> [Either Type EffWanted]
forall a b. (a -> b) -> [a] -> [b]
map Ct -> Either Type EffWanted
splitWanteds [Ct]
allWanteds

    -- We store a list of the types of all given constraints, which will be
    -- useful later.
    allGivenTys :: [Type]
allGivenTys = Ct -> Type
ctPred (Ct -> Type) -> [Ct] -> [Type]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Ct]
allGivens

    -- Determine if there is a unique solution to a goal from a set of
    -- candidates.
    solve
      :: InstEnvs
      -> EffWanted
      -> Maybe (EffWanted, EffGiven)
    solve :: InstEnvs -> EffWanted -> Maybe (EffWanted, EffGiven)
solve InstEnvs
globals EffWanted
goal = case [(EffGiven, TCvSubst)]
unifiableCands of
      -- If there's already only one unique solution, commit to it; in the worst
      -- case where it doesn't actually match, we get a cleaner error message
      -- like "Unable to match (State String) to (State Int)" instead of a type
      -- ambiguity error.
      [(EffGiven
soln, TCvSubst
_)] -> (EffWanted, EffGiven) -> Maybe (EffWanted, EffGiven)
forall a. a -> Maybe a
Just (EffWanted
goal, EffGiven
soln)
      [(EffGiven, TCvSubst)]
_ ->
        -- Otherwise, the second criteria comes in: the candidate must satisfy
        -- all other constraints we /want/ to solve. For example, when we want
        -- to solve '(State a :> es, Num a)`, the candidate 'State Int :> es'
        -- will do the job, because it satisfied 'Num a'; however 'State String
        -- :> es' will be excluded.
        let satisfiableCands :: [(EffGiven, TCvSubst)]
satisfiableCands = ((EffGiven, TCvSubst) -> Bool)
-> [(EffGiven, TCvSubst)] -> [(EffGiven, TCvSubst)]
forall a. (a -> Bool) -> [a] -> [a]
filter (InstEnvs -> (EffGiven, TCvSubst) -> Bool
satisfiable InstEnvs
globals) [(EffGiven, TCvSubst)]
unifiableCands
        in -- Finally, if there is a unique candidate remaining, we use it as
           -- the solution; otherwise we don't solve anything.
           case [(EffGiven, TCvSubst)]
satisfiableCands of
             [(EffGiven
soln, TCvSubst
_)] -> (EffWanted, EffGiven) -> Maybe (EffWanted, EffGiven)
forall a. a -> Maybe a
Just (EffWanted
goal, EffGiven
soln)
             [(EffGiven, TCvSubst)]
_ -> Maybe (EffWanted, EffGiven)
forall a. Maybe a
Nothing
      where
        -- Apart from ':>' constraints in the context, the effects already
        -- hardwired into the effect stack type, like those in 'A : B : C : es'
        -- also need to be considered. So here we extract that for them to be
        -- considered simultaneously with regular ':>' constraints.
        cands :: [EffGiven]
cands = Type -> Type -> [EffGiven]
extractExtraGivens (EffWanted -> Type
wantedEs EffWanted
goal) (EffWanted -> Type
wantedEs EffWanted
goal) [EffGiven] -> [EffGiven] -> [EffGiven]
forall a. Semigroup a => a -> a -> a
<> [EffGiven]
effGivens
        -- The first criteria is that the candidate constraint must /unify/ with
        -- the goal. This means that the type variables in the goal can be
        -- instantiated in a way so that the goal becomes equal to the
        -- candidate. For example, the candidates 'State Int :> es' and 'State
        -- String :> es' both unify with the goal 'State s :> es'.
        unifiableCands :: [(EffGiven, TCvSubst)]
unifiableCands = (EffGiven -> Maybe (EffGiven, TCvSubst))
-> [EffGiven] -> [(EffGiven, TCvSubst)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (EffWanted -> EffGiven -> Maybe (EffGiven, TCvSubst)
unifiableWith EffWanted
goal) [EffGiven]
cands

    -- Extract the heads of a type like 'A : B : C : es' into 'FakedepGiven's.
    extractExtraGivens :: Type -> Type -> [EffGiven]
    extractExtraGivens :: Type -> Type -> [EffGiven]
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 EffGiven { givenEffHead :: Type
givenEffHead = Type
dtHead
                    , givenEff :: Type
givenEff = Type
e
                    , givenEs :: Type
givenEs = Type
fullEs
                    } EffGiven -> [EffGiven] -> [EffGiven]
forall a. a -> [a] -> [a]
: Type -> Type -> [EffGiven]
extractExtraGivens Type
fullEs Type
es'
      (Type, [Type])
_ -> []

    -- Determine whether a given constraint is of form 'e :> es'.
    maybeEffGiven :: Ct -> Maybe EffGiven
    maybeEffGiven :: Ct -> Maybe EffGiven
maybeEffGiven = \case
#if __GLASGOW_HASKELL__ < 908
      CDictCan { cc_class :: Ct -> Class
cc_class = Class
cls
               , cc_tyargs :: Ct -> [Type]
cc_tyargs = [Type
eff, Type
es]
               } ->
#else
      CDictCan DictCt { di_cls = cls
                      , di_tys = [eff, es]
                      } ->
#endif
        if Class
cls Class -> Class -> Bool
forall a. Eq a => a -> a -> Bool
== Class
elemCls
        then EffGiven -> Maybe EffGiven
forall a. a -> Maybe a
Just EffGiven { givenEffHead :: Type
givenEffHead = (Type, [Type]) -> Type
forall a b. (a, b) -> a
fst ((Type, [Type]) -> Type) -> (Type, [Type]) -> Type
forall a b. (a -> b) -> a -> b
$ Type -> (Type, [Type])
splitAppTys Type
eff
                           , givenEff :: Type
givenEff = Type
eff
                           , givenEs :: Type
givenEs = Type
es
                           }
        else Maybe EffGiven
forall a. Maybe a
Nothing
      Ct
_ -> Maybe EffGiven
forall a. Maybe a
Nothing

    -- Determine whether a wanted constraint is of form 'e :> es'.
    splitWanteds :: Ct -> Either PredType EffWanted
    splitWanteds :: Ct -> Either Type EffWanted
splitWanteds = \case
#if __GLASGOW_HASKELL__ < 908
      ct :: Ct
ct@CDictCan { cc_ev :: Ct -> CtEvidence
cc_ev = CtWanted { ctev_loc :: CtEvidence -> CtLoc
ctev_loc = CtLoc
loc }
               , cc_class :: Ct -> Class
cc_class = Class
cls
               , cc_tyargs :: Ct -> [Type]
cc_tyargs = [Type
eff, Type
es]
               } ->
#else
      ct@(CDictCan DictCt { di_ev = CtWanted { ctev_loc = loc }
                          , di_cls = cls
                          , di_tys = [eff, es]
                          }) ->
#endif
        if Class
cls Class -> Class -> Bool
forall a. Eq a => a -> a -> Bool
== Class
elemCls
        then EffWanted -> Either Type EffWanted
forall a b. b -> Either a b
Right EffWanted { wantedEffHead :: Type
wantedEffHead = (Type, [Type]) -> Type
forall a b. (a, b) -> a
fst ((Type, [Type]) -> Type) -> (Type, [Type]) -> Type
forall a b. (a -> b) -> a -> b
$ Type -> (Type, [Type])
splitAppTys Type
eff
                             , wantedEff :: Type
wantedEff = Type
eff
                             , wantedEs :: Type
wantedEs = Type
es
                             , wantedLoc :: CtLoc
wantedLoc = CtLoc
loc
                             }
        else Type -> Either Type EffWanted
forall a b. a -> Either a b
Left (Type -> Either Type EffWanted) -> Type -> Either Type EffWanted
forall a b. (a -> b) -> a -> b
$ Ct -> Type
ctPred Ct
ct
      Ct
ct -> Type -> Either Type EffWanted
forall a b. a -> Either a b
Left (Type -> Either Type EffWanted) -> Type -> Either Type EffWanted
forall a b. (a -> b) -> a -> b
$ Ct -> Type
ctPred Ct
ct

    -- Given a wanted constraint and a given constraint, unify them and give
    -- back a substitution that can be applied to the wanted to make it equal to
    -- the given.
    unifiableWith :: EffWanted -> EffGiven -> Maybe (EffGiven, TCvSubst)
    unifiableWith :: EffWanted -> EffGiven -> Maybe (EffGiven, TCvSubst)
unifiableWith EffWanted
goal EffGiven
cand =
      if    EffWanted -> Type
wantedEs      EffWanted
goal Type -> Type -> Bool
`eqType` EffGiven -> Type
givenEs      EffGiven
cand
         Bool -> Bool -> Bool
&& EffWanted -> Type
wantedEffHead EffWanted
goal Type -> Type -> Bool
`eqType` EffGiven -> Type
givenEffHead EffGiven
cand
      then (EffGiven
cand, ) (TCvSubst -> (EffGiven, TCvSubst))
-> Maybe TCvSubst -> Maybe (EffGiven, TCvSubst)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Type -> Maybe TCvSubst
tcUnifyTy (EffWanted -> Type
wantedEff EffWanted
goal) (EffGiven -> Type
givenEff EffGiven
cand)
      else Maybe (EffGiven, TCvSubst)
forall a. Maybe a
Nothing

    -- Check whether a candidate can satisfy all the wanted constraints.
    satisfiable :: InstEnvs -> (EffGiven, TCvSubst) -> Bool
    satisfiable :: InstEnvs -> (EffGiven, TCvSubst) -> Bool
satisfiable InstEnvs
globals (EffGiven
_, TCvSubst
subst) = ((Type -> Bool) -> [Type] -> Bool)
-> [Type] -> (Type -> Bool) -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Type -> Bool) -> [Type] -> Bool
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Bool
all [Type]
wantedsInst ((Type -> Bool) -> Bool) -> (Type -> Bool) -> Bool
forall a b. (a -> b) -> a -> b
$ \Type
wanted ->
      if OrdType -> Set OrdType -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (Type -> OrdType
OrdType Type
wanted) Set OrdType
givensInst
        then Bool
True -- Can we find this constraint in our local context?
        else case Type -> (TyCon, [Type])
tcSplitTyConApp Type
wanted of
          (TyCon
con, [Type]
args) ->
            -- If not, lookup the global environment.
            case TyCon -> Maybe Class
tyConClass_maybe TyCon
con of
              Maybe Class
Nothing -> Bool
False
              Just Class
cls ->
                let ([InstMatch]
res, PotentialUnifiers
_, [InstMatch]
_) = Bool
-> InstEnvs
-> Class
-> [Type]
-> ([InstMatch], PotentialUnifiers, [InstMatch])
lookupInstEnv Bool
False InstEnvs
globals Class
cls [Type]
args
                in Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [InstMatch] -> Bool
forall a. [a] -> Bool
forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null [InstMatch]
res
      where
        -- The wanteds after unification.
        wantedsInst :: [Type]
wantedsInst = (() :: Constraint) => TCvSubst -> [Type] -> [Type]
TCvSubst -> [Type] -> [Type]
substTys TCvSubst
subst [Type]
otherWantedTys
        -- The local given context after unification.
        givensInst :: Set OrdType
givensInst = [OrdType] -> Set OrdType
forall a. Ord a => [a] -> Set a
Set.fromList (Type -> OrdType
OrdType (Type -> OrdType) -> [Type] -> [OrdType]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (() :: Constraint) => TCvSubst -> [Type] -> [Type]
TCvSubst -> [Type] -> [Type]
substTys TCvSubst
subst [Type]
allGivenTys)