{-# 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__ >= 900
import           GHC.Builtin.Types.Prim (alphaTys)
import           GHC.Plugins (idType, tyConClass_maybe, ppr, Outputable, sep, text, (<+>), parens)
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, tcGetTyVar_maybe, 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, tcGetTyVar_maybe, tcSplitAppTy_maybe)
import           TcSMonad hiding (tcLookupClass)
import           Type
import           TysPrim (alphaTys)
#endif



fundepPlugin :: TcPlugin
fundepPlugin :: TcPlugin
fundepPlugin = TcPlugin :: forall s.
TcPluginM s
-> (s -> TcPluginSolver) -> (s -> TcPluginM ()) -> TcPlugin
TcPlugin
  { tcPluginInit :: TcPluginM (IORef (Set Unification), PolysemyStuff 'Things)
tcPluginInit =
      (,) (IORef (Set Unification)
 -> PolysemyStuff 'Things
 -> (IORef (Set Unification), PolysemyStuff 'Things))
-> TcPluginM (IORef (Set Unification))
-> TcPluginM
     (PolysemyStuff 'Things
      -> (IORef (Set Unification), PolysemyStuff 'Things))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO (IORef (Set Unification)) -> TcPluginM (IORef (Set Unification))
forall a. IO a -> TcPluginM a
tcPluginIO (Set Unification -> IO (IORef (Set Unification))
forall a. a -> IO (IORef a)
newIORef Set Unification
forall a. Set a
S.empty)
          TcPluginM
  (PolysemyStuff 'Things
   -> (IORef (Set Unification), PolysemyStuff 'Things))
-> TcPluginM (PolysemyStuff 'Things)
-> TcPluginM (IORef (Set Unification), PolysemyStuff 'Things)
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 = TcPluginM ()
-> (IORef (Set Unification), PolysemyStuff 'Things) -> TcPluginM ()
forall a b. a -> b -> a
const (TcPluginM ()
 -> (IORef (Set Unification), PolysemyStuff 'Things)
 -> TcPluginM ())
-> TcPluginM ()
-> (IORef (Set Unification), PolysemyStuff 'Things)
-> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ () -> TcPluginM ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  }


------------------------------------------------------------------------------
-- | Like 'PredType', but has an 'Ord' instance.
newtype PredType' = PredType' { PredType' -> PredType
getPredType :: PredType }
  deriving newtype Rational -> PredType' -> SDoc
PredType' -> SDoc
(PredType' -> SDoc)
-> (Rational -> PredType' -> SDoc) -> Outputable PredType'
forall a. (a -> SDoc) -> (Rational -> a -> SDoc) -> Outputable a
pprPrec :: Rational -> PredType' -> SDoc
$cpprPrec :: Rational -> PredType' -> SDoc
ppr :: PredType' -> SDoc
$cppr :: PredType' -> SDoc
Outputable

instance Eq PredType' where
  == :: PredType' -> PredType' -> Bool
(==) = ((Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ) (Ordering -> Bool) -> (PredType' -> Ordering) -> PredType' -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((PredType' -> Ordering) -> PredType' -> Bool)
-> (PredType' -> PredType' -> Ordering)
-> PredType'
-> PredType'
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredType' -> PredType' -> Ordering
forall a. Ord a => a -> a -> Ordering
compare

instance Ord PredType' where
  compare :: PredType' -> PredType' -> Ordering
compare = PredType -> PredType -> Ordering
nonDetCmpType (PredType -> PredType -> Ordering)
-> (PredType' -> PredType) -> PredType' -> PredType' -> Ordering
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 (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
sep
    [ String -> SDoc
text String
"effect name = " SDoc -> SDoc -> SDoc
<+> PredType -> SDoc
forall a. Outputable a => a -> SDoc
ppr PredType
fcEffectName
    , String -> SDoc
text String
"effect = " SDoc -> SDoc -> SDoc
<+> PredType -> SDoc
forall a. Outputable a => a -> SDoc
ppr PredType
fcEffect
    , String -> SDoc
text String
"row = " SDoc -> SDoc -> SDoc
<+> PredType -> 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 (PolysemyStuff 'Things -> ThingOf 'Things Class
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
  Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ Class
ThingOf 'Things Class
cls Class -> Class -> Bool
forall a. Eq a => a -> a -> Bool
== Class
cls'
  FindConstraint -> [FindConstraint]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (FindConstraint -> [FindConstraint])
-> FindConstraint -> [FindConstraint]
forall a b. (a -> b) -> a -> b
$ FindConstraint :: CtLoc -> PredType -> PredType -> PredType -> FindConstraint
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
  Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ Class
cls Class -> Class -> Bool
forall a. Eq a => a -> a -> Bool
/= PolysemyStuff 'Things -> ThingOf 'Things Class
forall (l :: LookupState). PolysemyStuff l -> ThingOf l Class
findClass PolysemyStuff 'Things
things
  PredType -> [PredType]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PredType -> [PredType]) -> PredType -> [PredType]
forall a b. (a -> b) -> a -> b
$ PredType -> [PredType] -> PredType
mkAppTys (TyCon -> PredType
mkTyConTy (TyCon -> PredType) -> TyCon -> PredType
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 = [TyVar] -> Set TyVar
forall a. Ord a => [a] -> Set a
S.fromList ([TyVar] -> Set TyVar) -> [TyVar] -> Set TyVar
forall a b. (a -> b) -> a -> b
$ (FindConstraint -> [TyVar]) -> [FindConstraint] -> [TyVar]
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (PredType -> [TyVar]
tyCoVarsOfTypeWellScoped (PredType -> [TyVar])
-> (FindConstraint -> PredType) -> FindConstraint -> [TyVar]
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
        Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ PredType -> PredType -> Bool
eqType PredType
eff_name PredType
eff_name'
        Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ PredType -> PredType -> Bool
eqType PredType
r PredType
r'
        TCvSubst
subst <- Maybe TCvSubst -> [TCvSubst]
forall a. Maybe a -> [a]
maybeToList (Maybe TCvSubst -> [TCvSubst]) -> Maybe TCvSubst -> [TCvSubst]
forall a b. (a -> b) -> a -> b
$ SolveContext -> PredType -> PredType -> Maybe TCvSubst
unify (Set TyVar -> SolveContext
FunctionDef Set TyVar
skolems) PredType
wanted PredType
eff'
        (PredType, TCvSubst) -> [(PredType, TCvSubst)]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PredType
eff', TCvSubst
subst)
   in case [(PredType, TCvSubst)]
results of
        [] -> Maybe PredType -> TcM (Maybe PredType)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe PredType
forall a. Maybe a
Nothing
        -- If there is a unique member which unifies, return it.
        [(PredType
a, TCvSubst
_)] -> Maybe PredType -> TcM (Maybe PredType)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe PredType -> TcM (Maybe PredType))
-> Maybe PredType -> TcM (Maybe PredType)
forall a b. (a -> b) -> a -> b
$ PredType -> Maybe PredType
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@.
          ([[PredType]] -> Maybe PredType)
-> IOEnv (Env TcGblEnv TcLclEnv) [[PredType]]
-> TcM (Maybe PredType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([PredType] -> Maybe PredType
forall a. [a] -> Maybe a
singleListToJust ([PredType] -> Maybe PredType)
-> ([[PredType]] -> [PredType]) -> [[PredType]] -> Maybe PredType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[PredType]] -> [PredType]
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join) (IOEnv (Env TcGblEnv TcLclEnv) [[PredType]]
 -> TcM (Maybe PredType))
-> IOEnv (Env TcGblEnv TcLclEnv) [[PredType]]
-> TcM (Maybe PredType)
forall a b. (a -> b) -> a -> b
$ [(PredType, TCvSubst)]
-> ((PredType, TCvSubst)
    -> IOEnv (Env TcGblEnv TcLclEnv) [PredType])
-> IOEnv (Env TcGblEnv TcLclEnv) [[PredType]]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [(PredType, TCvSubst)]
results (((PredType, TCvSubst) -> IOEnv (Env TcGblEnv TcLclEnv) [PredType])
 -> IOEnv (Env TcGblEnv TcLclEnv) [[PredType]])
-> ((PredType, TCvSubst)
    -> IOEnv (Env TcGblEnv TcLclEnv) [PredType])
-> IOEnv (Env TcGblEnv TcLclEnv) [[PredType]]
forall a b. (a -> b) -> a -> b
$ \(PredType
eff, TCvSubst
subst) ->
            (Maybe PredType -> [PredType])
-> TcM (Maybe PredType) -> IOEnv (Env TcGblEnv TcLclEnv) [PredType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Maybe PredType -> [PredType]
forall a. Maybe a -> [a]
maybeToList (TcM (Maybe PredType) -> IOEnv (Env TcGblEnv TcLclEnv) [PredType])
-> TcM (Maybe PredType) -> IOEnv (Env TcGblEnv TcLclEnv) [PredType]
forall a b. (a -> b) -> a -> b
$
              (PredType -> IOEnv (Env TcGblEnv TcLclEnv) Bool)
-> [PredType] -> IOEnv (Env TcGblEnv TcLclEnv) Bool
forall (m :: * -> *) a. Monad m => (a -> m Bool) -> [a] -> m Bool
anyM (Set PredType'
-> TCvSubst -> PredType -> IOEnv (Env TcGblEnv TcLclEnv) Bool
checkExtraEvidence Set PredType'
extra_given TCvSubst
subst) [PredType]
extra_wanted IOEnv (Env TcGblEnv TcLclEnv) Bool
-> (Bool -> TcM (Maybe PredType)) -> TcM (Maybe PredType)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                Bool
True -> Maybe PredType -> TcM (Maybe PredType)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe PredType -> TcM (Maybe PredType))
-> Maybe PredType -> TcM (Maybe PredType)
forall a b. (a -> b) -> a -> b
$ PredType -> Maybe PredType
forall a. a -> Maybe a
Just PredType
eff
                Bool
False -> Maybe PredType -> TcM (Maybe PredType)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe PredType
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' -> TCvSubst -> PredType -> TcM Bool
checkExtraEvidence :: Set PredType'
-> TCvSubst -> PredType -> IOEnv (Env TcGblEnv TcLclEnv) Bool
checkExtraEvidence Set PredType'
givens TCvSubst
subst = (StateT (Set PredType') TcM Bool
 -> Set PredType' -> IOEnv (Env TcGblEnv TcLclEnv) Bool)
-> Set PredType'
-> StateT (Set PredType') TcM Bool
-> IOEnv (Env TcGblEnv TcLclEnv) Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT (Set PredType') TcM Bool
-> Set PredType' -> IOEnv (Env TcGblEnv TcLclEnv) Bool
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT Set PredType'
givens (StateT (Set PredType') TcM Bool
 -> IOEnv (Env TcGblEnv TcLclEnv) Bool)
-> (PredType -> StateT (Set PredType') TcM Bool)
-> PredType
-> IOEnv (Env TcGblEnv TcLclEnv) Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredType -> StateT (Set PredType') TcM Bool
getInstance (PredType -> StateT (Set PredType') TcM Bool)
-> (PredType -> PredType)
-> PredType
-> StateT (Set PredType') TcM Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasCallStack => TCvSubst -> PredType -> PredType
TCvSubst -> PredType -> PredType
substTy TCvSubst
subst


------------------------------------------------------------------------------
-- | Given an effect, compute its effect name.
getEffName :: Type -> Type
getEffName :: PredType -> PredType
getEffName PredType
t = (PredType, [PredType]) -> PredType
forall a b. (a, b) -> a
fst ((PredType, [PredType]) -> PredType)
-> (PredType, [PredType]) -> PredType
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
  (CtEvidence
ev, Coercion
_) <- TcM (CtEvidence, Coercion) -> TcPluginM (CtEvidence, Coercion)
forall a. TcM a -> TcPluginM a
unsafeTcPluginTcM
           (TcM (CtEvidence, Coercion) -> TcPluginM (CtEvidence, Coercion))
-> (TcS (CtEvidence, Coercion) -> TcM (CtEvidence, Coercion))
-> TcS (CtEvidence, Coercion)
-> TcPluginM (CtEvidence, Coercion)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcS (CtEvidence, Coercion) -> TcM (CtEvidence, Coercion)
forall a. TcS a -> TcM a
runTcSDeriveds
           (TcS (CtEvidence, Coercion) -> TcPluginM (CtEvidence, Coercion))
-> TcS (CtEvidence, Coercion) -> TcPluginM (CtEvidence, Coercion)
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
  (Unification, Ct) -> TcPluginM (Unification, Ct)
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 (PredType -> Maybe TyVar
tcGetTyVar_maybe -> Just TyVar
skolem, PredType
_) -> TyVar -> Set TyVar
forall a. a -> Set a
S.singleton TyVar
skolem
    Maybe (PredType, PredType)
_ -> Set TyVar -> (TyVar -> Set TyVar) -> Maybe TyVar -> Set TyVar
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Set TyVar
forall a. Monoid a => a
mempty TyVar -> Set TyVar
forall a. a -> Set a
S.singleton (Maybe TyVar -> Set TyVar) -> Maybe TyVar -> Set TyVar
forall a b. (a -> b) -> a -> b
$ PredType -> Maybe TyVar
tcGetTyVar_maybe PredType
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
  Bool
-> TcPluginM (Unification, Ct)
-> TcPluginM (Maybe (Unification, Ct))
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
|| Maybe TCvSubst -> Bool
forall a. Maybe a -> Bool
isJust (SolveContext -> PredType -> PredType -> Maybe TCvSubst
unify SolveContext
solve_ctx PredType
wanted PredType
given)) (TcPluginM (Unification, Ct)
 -> TcPluginM (Maybe (Unification, Ct)))
-> TcPluginM (Unification, Ct)
-> TcPluginM (Maybe (Unification, Ct))
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
    = Bool -> Maybe Bool -> Bool
forall a. a -> Maybe a -> a
fromMaybe Bool
False
    (Maybe Bool -> Bool)
-> (PredType -> Maybe Bool) -> PredType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OrdType -> Map OrdType Bool -> Maybe Bool)
-> Map OrdType Bool -> OrdType -> Maybe Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip OrdType -> Map OrdType Bool -> Maybe Bool
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Map OrdType Bool
singular_r
    (OrdType -> Maybe Bool)
-> (PredType -> OrdType) -> PredType -> Maybe Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredType -> OrdType
OrdType
  where
    singular_r :: Map OrdType Bool
singular_r = [(OrdType, Bool)] -> Map OrdType Bool
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?
               ([(OrdType, Bool)] -> Map OrdType Bool)
-> ([OrdType] -> [(OrdType, Bool)])
-> [OrdType]
-> Map OrdType Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((OrdType, Int) -> (OrdType, Bool))
-> [(OrdType, Int)] -> [(OrdType, Bool)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Int -> Bool) -> (OrdType, Int) -> (OrdType, Bool)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
1))
               ([(OrdType, Int)] -> [(OrdType, Bool)])
-> ([OrdType] -> [(OrdType, Int)])
-> [OrdType]
-> [(OrdType, Bool)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [OrdType] -> [(OrdType, Int)]
forall a. Eq a => [a] -> [(a, Int)]
countLength
               ([OrdType] -> Map OrdType Bool) -> [OrdType] -> Map OrdType Bool
forall a b. (a -> b) -> a -> b
$ PredType -> OrdType
OrdType (PredType -> OrdType)
-> (FindConstraint -> PredType) -> FindConstraint -> OrdType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FindConstraint -> PredType
fcRow (FindConstraint -> OrdType) -> [FindConstraint] -> [OrdType]
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 <- StateT (Set PredType') TcM (Set PredType')
forall (m :: * -> *) s. Monad m => StateT s m s
get
  case PredType' -> Set PredType' -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member (PredType -> PredType'
PredType' PredType
predty) Set PredType'
givens of
    Bool
True -> Bool -> StateT (Set PredType') TcM Bool
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 -> Bool -> StateT (Set PredType') TcM Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
        Just Class
cls -> do
          InstEnvs
env <- IOEnv (Env TcGblEnv TcLclEnv) InstEnvs
-> StateT (Set PredType') TcM InstEnvs
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift IOEnv (Env TcGblEnv TcLclEnv) 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
PredType -> [PredType] -> PredType
piResultTys (TyVar -> PredType
idType (TyVar -> PredType) -> TyVar -> PredType
forall a b. (a -> b) -> a -> b
$ ClsInst -> TyVar
is_dfun ClsInst
inst)
                    ([PredType] -> PredType) -> [PredType] -> PredType
forall a b. (a -> b) -> a -> b
$ (PredType -> Maybe PredType -> PredType)
-> [PredType] -> [Maybe PredType] -> [PredType]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith PredType -> Maybe PredType -> PredType
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
              (PredType -> StateT (Set PredType') TcM Bool)
-> [PredType] -> StateT (Set PredType') TcM Bool
forall (m :: * -> *) a. Monad m => (a -> m Bool) -> [a] -> m Bool
allM PredType -> StateT (Set PredType') TcM Bool
getInstance [PredType]
theta StateT (Set PredType') TcM Bool
-> (Bool -> StateT (Set PredType') TcM Bool)
-> StateT (Set PredType') TcM Bool
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
                  (Set PredType' -> Set PredType') -> StateT (Set PredType') TcM ()
forall (m :: * -> *) s. Monad m => (s -> s) -> StateT s m ()
modify ((Set PredType' -> Set PredType') -> StateT (Set PredType') TcM ())
-> (Set PredType' -> Set PredType')
-> StateT (Set PredType') TcM ()
forall a b. (a -> b) -> a -> b
$ PredType' -> Set PredType' -> Set PredType'
forall a. Ord a => a -> Set a -> Set a
S.insert (PredType' -> Set PredType' -> Set PredType')
-> PredType' -> Set PredType' -> Set PredType'
forall a b. (a -> b) -> a -> b
$ PredType -> PredType'
coerce PredType
predty
                  Bool -> StateT (Set PredType') TcM Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
                Bool
False -> Bool -> StateT (Set PredType') TcM Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
            [InstMatch]
_ -> Bool -> StateT (Set PredType') TcM Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False


solveFundep
    :: ( IORef (S.Set Unification)
       , PolysemyStuff 'Things
       )
    -> [Ct]
    -> [Ct]
    -> [Ct]
    -> TcPluginM TcPluginResult
solveFundep :: (IORef (Set Unification), PolysemyStuff 'Things) -> TcPluginSolver
solveFundep (IORef (Set Unification), PolysemyStuff 'Things)
_ [Ct]
_ [Ct]
_ [] = TcPluginResult -> TcPluginM TcPluginResult
forall (f :: * -> *) 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 [] []
solveFundep (IORef (Set Unification)
ref, PolysemyStuff 'Things
stuff) [Ct]
given [Ct]
_ [Ct]
wanted = do
  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 = [PredType'] -> Set PredType'
forall a. Ord a => [a] -> Set a
S.fromList ([PredType'] -> Set PredType') -> [PredType'] -> Set PredType'
forall a b. (a -> b) -> a -> b
$ [PredType] -> [PredType']
coerce ([PredType] -> [PredType']) -> [PredType] -> [PredType']
forall a b. (a -> b) -> a -> b
$ PolysemyStuff 'Things -> [Ct] -> [PredType]
getExtraEvidence PolysemyStuff 'Things
stuff [Ct]
given

  [Maybe (Unification, Ct)]
eqs <- [FindConstraint]
-> (FindConstraint -> TcPluginM (Maybe (Unification, Ct)))
-> TcPluginM [Maybe (Unification, Ct)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [FindConstraint]
wanted_finds ((FindConstraint -> TcPluginM (Maybe (Unification, Ct)))
 -> TcPluginM [Maybe (Unification, Ct)])
-> (FindConstraint -> TcPluginM (Maybe (Unification, Ct)))
-> TcPluginM [Maybe (Unification, Ct)]
forall a b. (a -> b) -> a -> b
$ \FindConstraint
fc -> do
    let r :: PredType
r  = FindConstraint -> PredType
fcRow FindConstraint
fc
    Maybe PredType
res <- TcM (Maybe PredType) -> TcPluginM (Maybe PredType)
forall a. TcM a -> TcPluginM a
unsafeTcPluginTcM
         (TcM (Maybe PredType) -> TcPluginM (Maybe PredType))
-> TcM (Maybe PredType) -> TcPluginM (Maybe PredType)
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' -> (Unification, Ct) -> Maybe (Unification, Ct)
forall a. a -> Maybe a
Just ((Unification, Ct) -> Maybe (Unification, Ct))
-> TcPluginM (Unification, Ct)
-> TcPluginM (Maybe (Unification, Ct))
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])
_ -> Maybe (Unification, Ct) -> TcPluginM (Maybe (Unification, Ct))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Unification, Ct)
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 <- IO (Set Unification) -> TcPluginM (Set Unification)
forall a. IO a -> TcPluginM a
tcPluginIO (IO (Set Unification) -> TcPluginM (Set Unification))
-> IO (Set Unification) -> TcPluginM (Set Unification)
forall a b. (a -> b) -> a -> b
$ IORef (Set Unification) -> IO (Set Unification)
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 ([(Unification, Ct)] -> ([Unification], [Ct]))
-> [(Unification, Ct)] -> ([Unification], [Ct])
forall a b. (a -> b) -> a -> b
$ [Maybe (Unification, Ct)] -> [(Unification, Ct)]
forall a. [Maybe a] -> [a]
catMaybes [Maybe (Unification, Ct)]
eqs
  IO () -> TcPluginM ()
forall a. IO a -> TcPluginM a
tcPluginIO (IO () -> TcPluginM ()) -> IO () -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ IORef (Set Unification)
-> (Set Unification -> Set Unification) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef (Set Unification)
ref ((Set Unification -> Set Unification) -> IO ())
-> (Set Unification -> Set Unification) -> IO ()
forall a b. (a -> b) -> a -> b
$ Set Unification -> Set Unification -> Set Unification
forall a. Ord a => Set a -> Set a -> Set a
S.union (Set Unification -> Set Unification -> Set Unification)
-> Set Unification -> Set Unification -> Set Unification
forall a b. (a -> b) -> a -> b
$ [Unification] -> Set Unification
forall a. Ord a => [a] -> Set a
S.fromList [Unification]
unifications

  TcPluginResult -> TcPluginM TcPluginResult
forall (f :: * -> *) 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]
new_wanteds