{-# LANGUAGE CPP                        #-}
{-# LANGUAGE DerivingStrategies         #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE RecordWildCards            #-}
{-# LANGUAGE ViewPatterns               #-}

------------------------------------------------------------------------------
-- The MIT License (MIT)
--
-- Copyright (c) 2017 Luka Horvat, 2019 Sandy Maguire
--
-- Permission is hereby granted, free of charge, to any person obtaining a copy
-- of this software and associated documentation files (the "Software"), to
-- deal in the Software without restriction, including without limitation the
-- rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
-- sell copies of the Software, and to permit persons to whom the Software is
-- furnished to do so, subject to the following conditions:
--
-- The above copyright notice and this permission notice shall be included in
-- all copies or substantial portions of the Software.
--
-- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
-- IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
-- FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
-- AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
-- LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
-- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
-- IN THE SOFTWARE.
--
------------------------------------------------------------------------------
--
-- This module was originally based on 'Control.Effects.Plugin' from the
-- 'simple-effects' package, by Luka Horvat.
--
-- https://gitlab.com/LukaHorvat/simple-effects/commit/966ce80b8b5777a4bd8f87ffd443f5fa80cc8845#f51c1641c95dfaa4827f641013f8017e8cd02aab

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
  }


------------------------------------------------------------------------------
-- | Like 'PredType', but has an 'Ord' instance.
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


------------------------------------------------------------------------------
-- | Corresponds to a 'Polysemy.Internal.Union.Find' constraint. For example,
-- given @Member (State s) r@, we would get:
data FindConstraint = FindConstraint
  { FindConstraint -> CtLoc
fcLoc        :: CtLoc
  , FindConstraint -> PredType
fcEffectName :: Type  -- ^ @State@
  , FindConstraint -> PredType
fcEffect     :: Type  -- ^ @State s@
  , FindConstraint -> PredType
fcRow        :: Type  -- ^ @r@
  }

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
    ]


------------------------------------------------------------------------------
-- | Given a list of constraints, filter out the 'FindConstraint's.
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
    }


------------------------------------------------------------------------------
-- | Get evidence in scope that aren't the 'FindConstraint's.
getExtraEvidence :: PolysemyStuff 'Things -> [Ct] -> [PredType]
getExtraEvidence :: PolysemyStuff 'Things -> [Ct] -> [PredType]
getExtraEvidence 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


------------------------------------------------------------------------------
-- | If there's a unique given @Member@ that would cause the program to
-- typecheck, use it.
findMatchingEffectIfSingular
    :: [PredType]        -- ^ Extra wanteds
    -> Set PredType'     -- ^ Extra givens
    -> FindConstraint    -- ^ Goal
    -> [FindConstraint]  -- ^ Member constraints
    -> 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
      -- Which members unify with our current goal?
      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
        -- If there is a unique member which unifies, return it.
        [(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)]
_ ->
          -- Otherwise, check if the extra wanteds give us enough information
          -- to make a unique choice.
          --
          -- For example, if we're trying to solve @Member (State a) r@, with
          -- candidates @Members (State Int, State String) r@ and can prove
          -- that @Num a@, then we can uniquely choose @State Int@.
          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 givens subst c@ returns 'True' iff we can prove that
-- the constraint @c@ holds under the substitution @subst@ in the context of
-- @givens@.
checkExtraEvidence ::
  Set PredType' ->
  SUBST ->
  PredType ->
  TcM Bool
checkExtraEvidence :: Set PredType' -> TCvSubst -> PredType -> TcM Bool
checkExtraEvidence 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


------------------------------------------------------------------------------
-- | Given an effect, compute its effect name.
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


------------------------------------------------------------------------------
-- | Generate a wanted unification for the effect described by the
-- 'FindConstraint' and the given effect.
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


------------------------------------------------------------------------------
-- | It's very important that we don't try to unify entire effects when we're
-- in interpreter mode. It's OK to unify @T x ~ T y@, but never @e ~ T y@. This
-- function takes then "given" of an interpreter, and produces a singleton
-- skolem set iff the outermost effect to be unified is a tyvar.
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


------------------------------------------------------------------------------
-- | Generate a wanted unification for the effect described by the
-- 'FindConstraint' and the given effect --- if they can be unified in this
-- context.
mkWanted
    :: FindConstraint
    -> SolveContext
    -> Type  -- ^ The given effect.
    -> 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


------------------------------------------------------------------------------
-- | Determine if there is exactly one wanted find for the @r@ in question.
exactlyOneWantedForR
    :: [FindConstraint]  -- ^ Wanted finds
    -> Type              -- ^ Effect row
    -> 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
               -- TODO(sandy): Nothing fails if this is just @second (const
               -- True)@. Why not? Incomplete test suite, or doing too much
               -- work?
               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


------------------------------------------------------------------------------
-- | Returns 'True' if we can prove the given 'PredType' has a (fully
-- instantiated) instance. Uses 'StateT' to cache the results of any instances
-- it needs to prove in service of the original goal.
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
              -- Get the instantiated type of the dictionary
              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
              -- pull off its resulting arguments
              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
                  -- Record that we can solve this instance, in case it's used
                  -- elsewhere
                  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
      -- We found a real given, therefore we are in the context of a function
      -- with an explicit @Member e r@ constraint. We also know it can
      -- be unified (although it may generate unsatisfiable constraints).
      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'

      -- Otherwise, check to see if @r ~ (e ': r')@. If so, pretend we're
      -- trying to solve a given @Member e r@. But this can only happen in the
      -- context of an interpreter!
      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

  -- We only want to emit a unification wanted once, otherwise a type error can
  -- force the type checker to loop forever.
  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