{-# 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
":>")]

-- | A list of unique, unambiguous Haskell names in the format of @(packageName, moduleName, identifier)@.
type Names = [(String, String, String)]

-- | Make a @polysemy-plugin@-style effect disambiguation plugin that applies to all the "element-of" typeclasses
-- passed in. Each of the names passed in should have type @k -> [k] -> 'Data.Kind.Type'@ where @k@ can be either
-- polymorphic or monomorphic.
--
-- Some examples include:
--
-- @
-- (\"cleff\", \"Cleff.Internal.Rec\", \":>\")
-- (\"polysemy\", \"Polysemy.Internal.Union\", \"Member\")
-- (\"effectful\", \"Effectful.Internal.Effect\", \":>\")
-- @
--
-- You can see the source code for notes on the implementation of the plugin.
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
  -- 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.
  let
    -- The only type of constraint we're interested in solving are 'Elem e es' constraints. Therefore, we extract these
    -- constraints out of the 'allGivens' and 'allWanted's.
    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
    -- We store a list of the types of all given constraints, which will be useful later.
    allGivenTypes :: [Type]
allGivenTypes = Ct -> Type
ctPred forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Ct]
allGivens
    -- We also store a list of wanted constraints that are /not/ 'Elem e es' for later use.
    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

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

  -- For each 'Elem e es' we /want/ to solve (the "goal"), we need to eventually correspond it to another unique
  -- /given/ 'Elem e es' that will make the program typecheck (the "solution").
  InstEnvs
globals <- forall a. TcM a -> TcPluginM a
liftTc TcM InstEnvs
tcGetInstEnvs -- Get the global instances environment for later use
  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

  -- Now we need to tell GHC the solutions. The way we do this is to generate a new equality constraint, like
  -- 'Elem (State e) es ~ Elem (State Int) es', so that GHC's constraint solver will know that 'e' must be 'Int'.
  [(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))

  -- 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 <- 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)

  -- traceM $ "Emitting: " <> showSDocUnsafe (ppr solnEqns)
  forall (f :: Type -> Type) a. Applicative f => a -> f a
pure [Ct]
solnEqns -- Finally we tell GHC the solutions.

  where

    -- Determine if there is a unique solution to a goal from a set of candidates.
    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
        -- Apart from 'Elem' 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 'Elem' constraints.
        cands :: [FakedepGiven]
cands = Type -> Type -> [FakedepGiven]
extractExtraGivens Type
goalEs Type
goalEs forall a. Semigroup a => a -> a -> a
<> [FakedepGiven]
givens
        -- 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 'Elem (State Int) es' and 'Elem (State String) es' both unify with the goal
        -- 'Elem (State s) es'.
        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
        -- 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.
        [(FakedepGiven
soln, TCvSubst
_)] -> forall a. a -> Maybe a
Just (FakedepWanted
goal, FakedepGiven
soln)
        [(FakedepGiven, 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 '(Elem (State a) es, Num a)`, the candidate 'Elem (State Int) es' will do
          -- the job, because it satisfied 'Num a'; however 'Elem (State String) es' will be excluded.
          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
          -- Finally, if there is a unique candidate remaining, we use it as the solution; otherwise we don't solve anything.
          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

    -- Extract the heads of a type like 'A : B : C : es' into 'FakedepGiven's.
    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])
_ -> []

    -- Determine whether a given constraint is of form 'Elem e es'.
    relevantGiven :: Ct -> Maybe FakedepGiven
    relevantGiven :: Ct -> Maybe FakedepGiven
relevantGiven (CDictCan CtEvidence
_ Class
cls [Type
_kind, Type
eff, Type
es] Bool
_) -- Polymorphic case
      | 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
_) -- Monomorphic case
      | 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

    -- Determine whether a wanted constraint is of form 'Elem e es'.
    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
_) -- Polymorphic case
      | 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
_) -- Monomorphic case
      | 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

    -- Determine whether a constraint is /not/ of form 'Elem e es'.
    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

    -- 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 :: FakedepWanted -> FakedepGiven -> Maybe (FakedepGiven, TCvSubst)
    unifiableWith :: FakedepWanted -> FakedepGiven -> Maybe (FakedepGiven, TCvSubst)
unifiableWith (FakedepWanted FakedepGiven
goal CtLoc
_) FakedepGiven
cand =
      -- First, the 'es' type must be equal, and the datatype head of the effect must be equal too.
      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) -- Then the effect type must unify.
        else forall a. Maybe a
Nothing

    -- Check whether a candidate can satisfy all tthe wanted constraints.
    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 -- The wanteds after unification.
        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 -- The local given context after unification.
      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 -- Can we find this constraint in our local context?
        else let (TyCon
con, [Type]
args) = Type -> (TyCon, [Type])
tcSplitTyConApp Type
want
        in case TyCon -> Maybe Class
tyConClass_maybe TyCon
con of -- If not, lookup the global environment.
          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