-- | This module provides an interface for typechecker plugins to
-- access select functions of the 'TcM', principally those to do with
-- reading parts of the state.
module GHC.Tc.Plugin (
        -- * Basic TcPluginM functionality
        TcPluginM,
        tcPluginIO,
        tcPluginTrace,
        unsafeTcPluginTcM,

        -- * Finding Modules and Names
        Finder.FindResult(..),
        findImportedModule,
        lookupOrig,

        -- * Looking up Names in the typechecking environment
        tcLookupGlobal,
        tcLookupTyCon,
        tcLookupDataCon,
        tcLookupClass,
        tcLookup,
        tcLookupId,

        -- * Getting the TcM state
        getTopEnv,
        getTargetPlatform,
        getEnvs,
        getInstEnvs,
        getFamInstEnvs,
        matchFam,

        -- * Type variables
        newUnique,
        newFlexiTyVar,
        isTouchableTcPluginM,

        -- * Zonking
        zonkTcType,
        zonkCt,

        -- * Creating constraints
        newWanted,
        newGiven,
        newCoercionHole,

        -- * Manipulating evidence bindings
        newEvVar,
        setEvBind,
    ) where

import GHC.Prelude

import GHC.Platform (Platform)

import qualified GHC.Tc.Utils.Monad     as TcM
import qualified GHC.Tc.Solver.Monad    as TcS
import qualified GHC.Tc.Utils.Env       as TcM
import qualified GHC.Tc.Utils.TcMType   as TcM
import qualified GHC.Tc.Zonk.TcType       as TcM
import qualified GHC.Tc.Instance.Family as TcM
import qualified GHC.Iface.Env          as IfaceEnv
import qualified GHC.Unit.Finder        as Finder

import GHC.Core.FamInstEnv     ( FamInstEnv )
import GHC.Tc.Utils.Monad      ( TcGblEnv, TcLclEnv, TcPluginM
                               , unsafeTcPluginTcM
                               , liftIO, traceTc )
import GHC.Tc.Types.Constraint ( Ct, CtLoc, CtEvidence(..) )
import GHC.Tc.Utils.TcMType    ( TcTyVar, TcType )
import GHC.Tc.Utils.Env        ( TcTyThing )
import GHC.Tc.Types.Evidence   ( CoercionHole, EvTerm(..)
                               , EvExpr, EvBindsVar, EvBind, mkGivenEvBind )
import GHC.Types.Var           ( EvVar )

import GHC.Unit.Module    ( ModuleName, Module )
import GHC.Types.Name     ( OccName, Name )
import GHC.Types.TyThing  ( TyThing )
import GHC.Core.Reduction ( Reduction )
import GHC.Core.TyCon     ( TyCon )
import GHC.Core.DataCon   ( DataCon )
import GHC.Core.Class     ( Class )
import GHC.Driver.Env       ( HscEnv(..) )
import GHC.Utils.Outputable ( SDoc )
import GHC.Core.Type        ( Kind, Type, PredType )
import GHC.Types.Id         ( Id )
import GHC.Core.InstEnv     ( InstEnvs )
import GHC.Types.Unique     ( Unique )
import GHC.Types.PkgQual    ( PkgQual )


-- | Perform some IO, typically to interact with an external tool.
tcPluginIO :: IO a -> TcPluginM a
tcPluginIO :: forall a. IO a -> TcPluginM a
tcPluginIO IO a
a = TcM a -> TcPluginM a
forall a. TcM a -> TcPluginM a
unsafeTcPluginTcM (IO a -> TcM a
forall a. IO a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO a
a)

-- | Output useful for debugging the compiler.
tcPluginTrace :: String -> SDoc -> TcPluginM ()
tcPluginTrace :: String -> SDoc -> TcPluginM ()
tcPluginTrace String
a SDoc
b = TcM () -> TcPluginM ()
forall a. TcM a -> TcPluginM a
unsafeTcPluginTcM (String -> SDoc -> TcM ()
traceTc String
a SDoc
b)


findImportedModule :: ModuleName -> PkgQual -> TcPluginM Finder.FindResult
findImportedModule :: ModuleName -> PkgQual -> TcPluginM FindResult
findImportedModule ModuleName
mod_name PkgQual
mb_pkg = do
    HscEnv
hsc_env <- TcPluginM HscEnv
getTopEnv
    IO FindResult -> TcPluginM FindResult
forall a. IO a -> TcPluginM a
tcPluginIO (IO FindResult -> TcPluginM FindResult)
-> IO FindResult -> TcPluginM FindResult
forall a b. (a -> b) -> a -> b
$ HscEnv -> ModuleName -> PkgQual -> IO FindResult
Finder.findImportedModule HscEnv
hsc_env ModuleName
mod_name PkgQual
mb_pkg

lookupOrig :: Module -> OccName -> TcPluginM Name
lookupOrig :: Module -> OccName -> TcPluginM Name
lookupOrig Module
mod = TcM Name -> TcPluginM Name
forall a. TcM a -> TcPluginM a
unsafeTcPluginTcM (TcM Name -> TcPluginM Name)
-> (OccName -> TcM Name) -> OccName -> TcPluginM Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Module -> OccName -> TcM Name
forall a b. Module -> OccName -> TcRnIf a b Name
IfaceEnv.lookupOrig Module
mod


tcLookupGlobal :: Name -> TcPluginM TyThing
tcLookupGlobal :: Name -> TcPluginM TyThing
tcLookupGlobal = TcM TyThing -> TcPluginM TyThing
forall a. TcM a -> TcPluginM a
unsafeTcPluginTcM (TcM TyThing -> TcPluginM TyThing)
-> (Name -> TcM TyThing) -> Name -> TcPluginM TyThing
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> TcM TyThing
TcM.tcLookupGlobal

tcLookupTyCon :: Name -> TcPluginM TyCon
tcLookupTyCon :: Name -> TcPluginM TyCon
tcLookupTyCon = TcM TyCon -> TcPluginM TyCon
forall a. TcM a -> TcPluginM a
unsafeTcPluginTcM (TcM TyCon -> TcPluginM TyCon)
-> (Name -> TcM TyCon) -> Name -> TcPluginM TyCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> TcM TyCon
TcM.tcLookupTyCon

tcLookupDataCon :: Name -> TcPluginM DataCon
tcLookupDataCon :: Name -> TcPluginM DataCon
tcLookupDataCon = TcM DataCon -> TcPluginM DataCon
forall a. TcM a -> TcPluginM a
unsafeTcPluginTcM (TcM DataCon -> TcPluginM DataCon)
-> (Name -> TcM DataCon) -> Name -> TcPluginM DataCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> TcM DataCon
TcM.tcLookupDataCon

tcLookupClass :: Name -> TcPluginM Class
tcLookupClass :: Name -> TcPluginM Class
tcLookupClass = TcM Class -> TcPluginM Class
forall a. TcM a -> TcPluginM a
unsafeTcPluginTcM (TcM Class -> TcPluginM Class)
-> (Name -> TcM Class) -> Name -> TcPluginM Class
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> TcM Class
TcM.tcLookupClass

tcLookup :: Name -> TcPluginM TcTyThing
tcLookup :: Name -> TcPluginM TcTyThing
tcLookup = TcM TcTyThing -> TcPluginM TcTyThing
forall a. TcM a -> TcPluginM a
unsafeTcPluginTcM (TcM TcTyThing -> TcPluginM TcTyThing)
-> (Name -> TcM TcTyThing) -> Name -> TcPluginM TcTyThing
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> TcM TcTyThing
TcM.tcLookup

tcLookupId :: Name -> TcPluginM Id
tcLookupId :: Name -> TcPluginM Id
tcLookupId = TcM Id -> TcPluginM Id
forall a. TcM a -> TcPluginM a
unsafeTcPluginTcM (TcM Id -> TcPluginM Id)
-> (Name -> TcM Id) -> Name -> TcPluginM Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> TcM Id
TcM.tcLookupId


getTopEnv :: TcPluginM HscEnv
getTopEnv :: TcPluginM HscEnv
getTopEnv = TcM HscEnv -> TcPluginM HscEnv
forall a. TcM a -> TcPluginM a
unsafeTcPluginTcM TcM HscEnv
forall gbl lcl. TcRnIf gbl lcl HscEnv
TcM.getTopEnv

getTargetPlatform :: TcPluginM Platform
getTargetPlatform :: TcPluginM Platform
getTargetPlatform = TcM Platform -> TcPluginM Platform
forall a. TcM a -> TcPluginM a
unsafeTcPluginTcM TcM Platform
forall a b. TcRnIf a b Platform
TcM.getPlatform


getEnvs :: TcPluginM (TcGblEnv, TcLclEnv)
getEnvs :: TcPluginM (TcGblEnv, TcLclEnv)
getEnvs = TcM (TcGblEnv, TcLclEnv) -> TcPluginM (TcGblEnv, TcLclEnv)
forall a. TcM a -> TcPluginM a
unsafeTcPluginTcM TcM (TcGblEnv, TcLclEnv)
forall gbl lcl. TcRnIf gbl lcl (gbl, lcl)
TcM.getEnvs

getInstEnvs :: TcPluginM InstEnvs
getInstEnvs :: TcPluginM InstEnvs
getInstEnvs = TcM InstEnvs -> TcPluginM InstEnvs
forall a. TcM a -> TcPluginM a
unsafeTcPluginTcM TcM InstEnvs
TcM.tcGetInstEnvs

getFamInstEnvs :: TcPluginM (FamInstEnv, FamInstEnv)
getFamInstEnvs :: TcPluginM (FamInstEnv, FamInstEnv)
getFamInstEnvs = TcM (FamInstEnv, FamInstEnv) -> TcPluginM (FamInstEnv, FamInstEnv)
forall a. TcM a -> TcPluginM a
unsafeTcPluginTcM TcM (FamInstEnv, FamInstEnv)
TcM.tcGetFamInstEnvs

matchFam :: TyCon -> [Type]
         -> TcPluginM (Maybe Reduction)
matchFam :: TyCon -> [Type] -> TcPluginM (Maybe Reduction)
matchFam TyCon
tycon [Type]
args = TcM (Maybe Reduction) -> TcPluginM (Maybe Reduction)
forall a. TcM a -> TcPluginM a
unsafeTcPluginTcM (TcM (Maybe Reduction) -> TcPluginM (Maybe Reduction))
-> TcM (Maybe Reduction) -> TcPluginM (Maybe Reduction)
forall a b. (a -> b) -> a -> b
$ TyCon -> [Type] -> TcM (Maybe Reduction)
TcS.matchFamTcM TyCon
tycon [Type]
args

newUnique :: TcPluginM Unique
newUnique :: TcPluginM Unique
newUnique = TcM Unique -> TcPluginM Unique
forall a. TcM a -> TcPluginM a
unsafeTcPluginTcM TcM Unique
forall gbl lcl. TcRnIf gbl lcl Unique
TcM.newUnique

newFlexiTyVar :: Kind -> TcPluginM TcTyVar
newFlexiTyVar :: Type -> TcPluginM Id
newFlexiTyVar = TcM Id -> TcPluginM Id
forall a. TcM a -> TcPluginM a
unsafeTcPluginTcM (TcM Id -> TcPluginM Id)
-> (Type -> TcM Id) -> Type -> TcPluginM Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> TcM Id
TcM.newFlexiTyVar

isTouchableTcPluginM :: TcTyVar -> TcPluginM Bool
isTouchableTcPluginM :: Id -> TcPluginM Bool
isTouchableTcPluginM = TcM Bool -> TcPluginM Bool
forall a. TcM a -> TcPluginM a
unsafeTcPluginTcM (TcM Bool -> TcPluginM Bool)
-> (Id -> TcM Bool) -> Id -> TcPluginM Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> TcM Bool
TcM.isTouchableTcM

-- | Confused by zonking? See Note [What is zonking?] in "GHC.Tc.Zonk.Type".
zonkTcType :: TcType -> TcPluginM TcType
zonkTcType :: Type -> TcPluginM Type
zonkTcType = TcM Type -> TcPluginM Type
forall a. TcM a -> TcPluginM a
unsafeTcPluginTcM (TcM Type -> TcPluginM Type)
-> (Type -> TcM Type) -> Type -> TcPluginM Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ZonkM Type -> TcM Type
forall a. ZonkM a -> TcM a
TcM.liftZonkM (ZonkM Type -> TcM Type)
-> (Type -> ZonkM Type) -> Type -> TcM Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> ZonkM Type
TcM.zonkTcType

zonkCt :: Ct -> TcPluginM Ct
zonkCt :: Ct -> TcPluginM Ct
zonkCt = TcM Ct -> TcPluginM Ct
forall a. TcM a -> TcPluginM a
unsafeTcPluginTcM (TcM Ct -> TcPluginM Ct) -> (Ct -> TcM Ct) -> Ct -> TcPluginM Ct
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ZonkM Ct -> TcM Ct
forall a. ZonkM a -> TcM a
TcM.liftZonkM (ZonkM Ct -> TcM Ct) -> (Ct -> ZonkM Ct) -> Ct -> TcM Ct
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> ZonkM Ct
TcM.zonkCt

-- | Create a new Wanted constraint with the given 'CtLoc'.
newWanted :: CtLoc -> PredType -> TcPluginM CtEvidence
newWanted :: CtLoc -> Type -> TcPluginM CtEvidence
newWanted CtLoc
loc Type
pty
  = TcM CtEvidence -> TcPluginM CtEvidence
forall a. TcM a -> TcPluginM a
unsafeTcPluginTcM (CtLoc -> Type -> TcM CtEvidence
TcM.newWantedWithLoc CtLoc
loc Type
pty)

-- | Create a new given constraint, with the supplied evidence.
--
-- This should only be invoked within 'tcPluginSolve'.
newGiven :: EvBindsVar -> CtLoc -> PredType -> EvExpr -> TcPluginM CtEvidence
newGiven :: EvBindsVar -> CtLoc -> Type -> EvExpr -> TcPluginM CtEvidence
newGiven EvBindsVar
tc_evbinds CtLoc
loc Type
pty EvExpr
evtm = do
   Id
new_ev <- Type -> TcPluginM Id
newEvVar Type
pty
   EvBindsVar -> EvBind -> TcPluginM ()
setEvBind EvBindsVar
tc_evbinds (EvBind -> TcPluginM ()) -> EvBind -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ Id -> EvTerm -> EvBind
mkGivenEvBind Id
new_ev (EvExpr -> EvTerm
EvExpr EvExpr
evtm)
   CtEvidence -> TcPluginM CtEvidence
forall a. a -> TcPluginM a
forall (m :: * -> *) a. Monad m => a -> m a
return CtGiven { ctev_pred :: Type
ctev_pred = Type
pty, ctev_evar :: Id
ctev_evar = Id
new_ev, ctev_loc :: CtLoc
ctev_loc = CtLoc
loc }

-- | Create a fresh evidence variable.
--
-- This should only be invoked within 'tcPluginSolve'.
newEvVar :: PredType -> TcPluginM EvVar
newEvVar :: Type -> TcPluginM Id
newEvVar = TcM Id -> TcPluginM Id
forall a. TcM a -> TcPluginM a
unsafeTcPluginTcM (TcM Id -> TcPluginM Id)
-> (Type -> TcM Id) -> Type -> TcPluginM Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> TcM Id
forall gbl lcl. Type -> TcRnIf gbl lcl Id
TcM.newEvVar

-- | Create a fresh coercion hole.
-- This should only be invoked within 'tcPluginSolve'.
newCoercionHole :: PredType -> TcPluginM CoercionHole
newCoercionHole :: Type -> TcPluginM CoercionHole
newCoercionHole = TcM CoercionHole -> TcPluginM CoercionHole
forall a. TcM a -> TcPluginM a
unsafeTcPluginTcM (TcM CoercionHole -> TcPluginM CoercionHole)
-> (Type -> TcM CoercionHole) -> Type -> TcPluginM CoercionHole
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> TcM CoercionHole
TcM.newVanillaCoercionHole

-- | Bind an evidence variable.
--
-- This should only be invoked within 'tcPluginSolve'.
setEvBind :: EvBindsVar -> EvBind -> TcPluginM ()
setEvBind :: EvBindsVar -> EvBind -> TcPluginM ()
setEvBind EvBindsVar
tc_evbinds EvBind
ev_bind = do
    TcM () -> TcPluginM ()
forall a. TcM a -> TcPluginM a
unsafeTcPluginTcM (TcM () -> TcPluginM ()) -> TcM () -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ EvBindsVar -> EvBind -> TcM ()
TcM.addTcEvBind EvBindsVar
tc_evbinds EvBind
ev_bind