{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE CPP #-}
module Effectful.Plugin.Internal (Plugin, Names, makePlugin) 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

-- | 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 = Maybe TcPlugin -> TcPlugin
forall a b. a -> b -> a
const (TcPlugin -> Maybe TcPlugin
forall a. a -> Maybe a
Just (TcPlugin -> Maybe TcPlugin) -> TcPlugin -> Maybe TcPlugin
forall a b. (a -> b) -> a -> b
$ Names -> TcPlugin
fakedep Names
names)
  , pluginRecompile :: [CommandLineOption] -> IO PluginRecompile
pluginRecompile = [CommandLineOption] -> IO PluginRecompile
purePlugin
  }

fakedep :: Names -> TcPlugin
fakedep :: Names -> TcPlugin
fakedep Names
names = TcPlugin :: forall s.
TcPluginM s
-> (s -> TcPluginSolver) -> (s -> TcPluginM ()) -> TcPlugin
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 = TcPluginM () -> ([Class], IORef VisitedSet) -> TcPluginM ()
forall a b. a -> b -> a
const (TcPluginM () -> ([Class], IORef VisitedSet) -> TcPluginM ())
-> TcPluginM () -> ([Class], IORef VisitedSet) -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ () -> TcPluginM ()
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ()
  }

liftTc :: TcM a -> TcPluginM a
liftTc :: TcM a -> TcPluginM a
liftTc = TcM a -> TcPluginM a
forall a. TcM a -> TcPluginM a
unsafeTcPluginTcM

liftIo :: IO a -> TcPluginM a
liftIo :: IO a -> TcPluginM a
liftIo = IO a -> TcPluginM a
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 <- Names
-> ((CommandLineOption, CommandLineOption, CommandLineOption)
    -> TcPluginM Class)
-> TcPluginM [Class]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for Names
names \(CommandLineOption
packageName, CommandLineOption
elemModuleName, CommandLineOption
elemClassName) -> do
    Module
recMod <- ModuleName -> FastString -> TcPluginM Module
lookupModule (CommandLineOption -> ModuleName
mkModuleName CommandLineOption
elemModuleName) (FastString -> TcPluginM Module) -> FastString -> TcPluginM Module
forall a b. (a -> b) -> a -> b
$ CommandLineOption -> FastString
fsLit CommandLineOption
packageName
    Name
nm <- Module -> OccName -> TcPluginM Name
lookupName Module
recMod (OccName -> TcPluginM Name) -> OccName -> TcPluginM Name
forall a b. (a -> b) -> a -> b
$ CommandLineOption -> OccName
mkTcOcc CommandLineOption
elemClassName
    Name -> TcPluginM Class
tcLookupClass Name
nm
  IORef VisitedSet
visited <- IO (IORef VisitedSet) -> TcPluginM (IORef VisitedSet)
forall a. IO a -> TcPluginM a
liftIo (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 (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 -> CommandLineOption
show (FakedepGiven Type
_ Type
e Type
es) = CommandLineOption
"(Elem " 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) CommandLineOption -> ShowS
forall a. Semigroup a => a -> a -> a
<> CommandLineOption
")"

data FakedepWanted = FakedepWanted FakedepGiven CtLoc

instance Show FakedepWanted where
  show :: FakedepWanted -> CommandLineOption
show (FakedepWanted FakedepGiven
given CtLoc
_) = FakedepGiven -> CommandLineOption
forall a. Show a => a -> CommandLineOption
show FakedepGiven
given

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

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 <- [[Ct]] -> [Ct]
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat ([[Ct]] -> [Ct]) -> TcPluginM [[Ct]] -> TcPluginM [Ct]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Class] -> (Class -> TcPluginM [Ct]) -> TcPluginM [[Ct]]
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
  TcPluginResult -> TcPluginM TcPluginResult
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TcPluginResult -> TcPluginM TcPluginResult)
-> TcPluginResult -> TcPluginM TcPluginResult
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]
_ [] = [Ct] -> TcPluginM [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 = (Ct -> Maybe FakedepGiven) -> [Ct] -> [FakedepGiven]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Ct -> Maybe FakedepGiven
relevantGiven [Ct]
allGivens
    wanteds :: [FakedepWanted]
wanteds = (Ct -> Maybe FakedepWanted) -> [Ct] -> [FakedepWanted]
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 (Ct -> Type) -> [Ct] -> [Type]
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 (Ct -> Type) -> [Ct] -> [Type]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Ct -> Bool) -> [Ct] -> [Ct]
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 <- TcM InstEnvs -> TcPluginM InstEnvs
forall a. TcM a -> TcPluginM a
liftTc TcM InstEnvs
tcGetInstEnvs -- Get the global instances environment for later use
  let solns :: [(FakedepWanted, FakedepGiven)]
solns = (FakedepWanted -> Maybe (FakedepWanted, FakedepGiven))
-> [FakedepWanted] -> [(FakedepWanted, FakedepGiven)]
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 <- [(FakedepWanted, FakedepGiven)]
-> ((FakedepWanted, FakedepGiven)
    -> 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 [(FakedepWanted, FakedepGiven)]
solns \(FakedepWanted (FakedepGiven Type
_ Type
goalEff Type
_) CtLoc
loc, FakedepGiven Type
_ Type
solnEff Type
_)  -> do
    (CtEvidence
eqn, Coercion
_) <- TcM (CtEvidence, Coercion) -> TcPluginM (CtEvidence, Coercion)
forall a. TcM a -> TcPluginM a
liftTc (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
runTcSDeriveds (TcS (CtEvidence, Coercion) -> TcM (CtEvidence, Coercion))
-> TcS (CtEvidence, Coercion) -> TcM (CtEvidence, Coercion)
forall a b. (a -> b) -> a -> b
$ CtLoc -> Role -> Type -> Type -> TcS (CtEvidence, Coercion)
newWantedEq CtLoc
loc Role
Nominal Type
goalEff Type
solnEff
    (Ct, (OrdType, OrdType)) -> TcPluginM (Ct, (OrdType, OrdType))
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 <- IO VisitedSet -> TcPluginM VisitedSet
forall a. IO a -> TcPluginM a
liftIo (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
forall a b. (a, b) -> a
fst ((Ct, (OrdType, OrdType)) -> Ct)
-> [(Ct, (OrdType, OrdType))] -> [Ct]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (((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)
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
liftIo (IO () -> TcPluginM ()) -> IO () -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ 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)
forall a b. (a, b) -> b
snd ((Ct, (OrdType, OrdType)) -> (OrdType, OrdType))
-> [(Ct, (OrdType, OrdType))] -> [(OrdType, OrdType)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Ct, (OrdType, OrdType))]
eqns)

  -- traceM $ "Emitting: " <> showSDocUnsafe (ppr solnEqns)
  [Ct] -> TcPluginM [Ct]
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 [FakedepGiven] -> [FakedepGiven] -> [FakedepGiven]
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 = (FakedepGiven -> Maybe (FakedepGiven, TCvSubst))
-> [FakedepGiven] -> [(FakedepGiven, TCvSubst)]
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
_)] -> (FakedepWanted, FakedepGiven)
-> Maybe (FakedepWanted, FakedepGiven)
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 = ((FakedepGiven, TCvSubst) -> Bool)
-> [(FakedepGiven, TCvSubst)] -> [(FakedepGiven, TCvSubst)]
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
_)] -> (FakedepWanted, FakedepGiven)
-> Maybe (FakedepWanted, FakedepGiven)
forall a. a -> Maybe a
Just (FakedepWanted
goal, FakedepGiven
soln)
            [(FakedepGiven, TCvSubst)]
_           -> Maybe (FakedepWanted, FakedepGiven)
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 FakedepGiven -> [FakedepGiven] -> [FakedepGiven]
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 Class -> Class -> Bool
forall a. Eq a => a -> a -> Bool
== Class
elemCls = FakedepGiven -> Maybe FakedepGiven
forall a. a -> Maybe a
Just (FakedepGiven -> Maybe FakedepGiven)
-> FakedepGiven -> Maybe FakedepGiven
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type -> FakedepGiven
FakedepGiven ((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) Type
eff Type
es
    relevantGiven (CDictCan CtEvidence
_ Class
cls [Type
eff, Type
es] Bool
_) -- Monomorphic case
      | Class
cls Class -> Class -> Bool
forall a. Eq a => a -> a -> Bool
== Class
elemCls = FakedepGiven -> Maybe FakedepGiven
forall a. a -> Maybe a
Just (FakedepGiven -> Maybe FakedepGiven)
-> FakedepGiven -> Maybe FakedepGiven
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type -> FakedepGiven
FakedepGiven ((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) Type
eff Type
es
    relevantGiven Ct
_ = Maybe FakedepGiven
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 Class -> Class -> Bool
forall a. Eq a => a -> a -> Bool
== Class
elemCls = FakedepWanted -> Maybe FakedepWanted
forall a. a -> Maybe a
Just (FakedepWanted -> Maybe FakedepWanted)
-> FakedepWanted -> Maybe FakedepWanted
forall a b. (a -> b) -> a -> b
$ FakedepGiven -> CtLoc -> FakedepWanted
FakedepWanted (Type -> Type -> Type -> FakedepGiven
FakedepGiven ((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) 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 Class -> Class -> Bool
forall a. Eq a => a -> a -> Bool
== Class
elemCls = FakedepWanted -> Maybe FakedepWanted
forall a. a -> Maybe a
Just (FakedepWanted -> Maybe FakedepWanted)
-> FakedepWanted -> Maybe FakedepWanted
forall a b. (a -> b) -> a -> b
$ FakedepGiven -> CtLoc -> FakedepWanted
FakedepWanted (Type -> Type -> Type -> FakedepGiven
FakedepGiven ((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) Type
eff Type
es) CtLoc
loc
    relevantWanted Ct
_ = Maybe FakedepWanted
forall a. Maybe a
Nothing

    -- Determine whether a constraint is /not/ of form 'Elem e es'.
    irrelevant :: Ct -> Bool
    irrelevant :: Ct -> Bool
irrelevant = Maybe FakedepGiven -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe FakedepGiven -> Bool)
-> (Ct -> Maybe FakedepGiven) -> Ct -> Bool
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, ) (TCvSubst -> (FakedepGiven, TCvSubst))
-> Maybe TCvSubst -> Maybe (FakedepGiven, TCvSubst)
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 Maybe (FakedepGiven, TCvSubst)
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]
TCvSubst -> [Type] -> [Type]
substTys TCvSubst
subst [Type]
wanteds -- The wanteds after unification.
        givensInst :: Set OrdType
givensInst = [OrdType] -> Set OrdType
forall a. Ord a => [a] -> Set a
Set.fromList ([OrdType] -> Set OrdType) -> [OrdType] -> Set OrdType
forall a b. (a -> b) -> a -> b
$ Type -> OrdType
OrdType (Type -> OrdType) -> [Type] -> [OrdType]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> HasCallStack => TCvSubst -> [Type] -> [Type]
TCvSubst -> [Type] -> [Type]
substTys TCvSubst
subst [Type]
givens -- The local given context after unification.
      in ((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
want ->
        if OrdType -> Set OrdType -> Bool
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 (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [InstMatch] -> Bool
forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null [InstMatch]
res