{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE UndecidableInstances #-}
module GHC.TcPlugin.API
(
TcPlugin(..)
, mkTcPlugin
, TcPluginStage(..), MonadTcPlugin
, TcPluginM
, tcPluginIO
, MonadTcPluginWork
, TcPluginErrorMessage(..)
, mkTcPluginErrorTy
, findImportedModule, fsLit, mkModuleName
, Module, ModuleName, FindResult(..)
, mkVarOcc, mkDataOcc, mkTyVarOcc, mkTcOcc, mkClsOcc
, lookupOrig
, tcLookupTyCon
, tcLookupDataCon
, tcLookupClass
, tcLookupGlobal
, tcLookup
, tcLookupId
, promoteDataCon
, TcPluginSolver
#if HAS_REWRITING
, TcPluginSolveResult(..)
#else
, TcPluginSolveResult
, pattern TcPluginContradiction, pattern TcPluginOk
#endif
, tcPluginTrace
, mkNonCanonical
, Pred
, pattern ClassPred, pattern EqPred, pattern IrredPred, pattern ForAllPred
, classifyPredType, ctPred
, TyVar, CoVar
, MetaDetails, MetaInfo
, isSkolemTyVar
, isMetaTyVar, isFilledMetaTyVar_maybe
, writeMetaTyVar
, eqType
, ctLoc, ctEvidence, ctFlavour, ctEqRel, ctOrigin
, mkPluginUnivCo
, newCoercionHole
, mkReflCo, mkSymCo, mkTransCo, mkUnivCo
, mkCoercionTy, isCoercionTy, isCoercionTy_maybe
, mkPluginUnivEvTerm
, evDataConApp
, newEvVar, setEvBind
, evCoercion, evCast
, ctEvExpr
, askEvBinds, lookupEvBind, eb_lhs, eb_rhs
, newName, mkLocalId, mkTyVar
, ctev_pred, ctev_evar, ctev_loc, ctev_dest
, classDataCon
, module GHC.Core.Make
, getInstEnvs
, newWanted, newGiven
, mkClassPred, mkPrimEqPredRole
, askDeriveds, newDerived
, setCtLocM
, setCtLocRewriteM
, bumpCtLocDepth
, TcPluginRewriter, TcPluginRewriteResult(..)
, matchFam
, getFamInstEnvs
, FamInstEnv
, askRewriteEnv, rewriteEnvCtLoc, RewriteEnv
, mkTyFamAppReduction, Reduction(..)
, newUnique
, newFlexiTyVar
, isTouchableTcPluginM
, mkTyVarTy, mkTyVarTys
, isTyVarTy, getTyVar_maybe
, TcType, TcTyVar, Unique, Kind
, mkTyConTy, mkTyConApp, splitTyConApp_maybe
, mkAppTy, mkAppTys
, mkInvisFunTyMany, mkInvisFunTysMany
, mkForAllTy, mkForAllTys
, mkPiTy, mkPiTys
#if MIN_VERSION_ghc(9,0,0)
, Mult, pattern One, pattern Many
#endif
, zonkTcType
, zonkCt
, panic, pprPanic
, UniqDFM
, lookupUDFM, lookupUDFM_Directly, elemUDFM
, UniqFM
, emptyUFM, listToUFM
, getEnvs
, module GHC.Builtin.Types
, Name, OccName, TyThing, TcTyThing
, Class(classTyCon), DataCon, TyCon, Id
, FastString
, EqRel(..), FunDep, CtFlavour
, Ct, CtLoc, CtEvidence, CtOrigin
, QCInst
, Type, PredType
, InstEnvs, TcLevel
, Coercion, Role(..), UnivCoProvenance
, CoercionHole(..)
, EvBind, EvTerm(EvExpr), EvVar, EvExpr, EvBindsVar
, Expr(Var, Type, Coercion), CoreBndr
, TcEvDest(..)
, TcGblEnv, TcLclEnv
, GenLocated(..), Located, RealLocated
, unLoc, getLoc
, SDoc, Outputable(..)
)
where
import GHC
( TyThing(..) )
import GHC.Builtin.Types
import GHC.Core
( CoreBndr, Expr(..) )
import GHC.Core.Class
( Class(..), FunDep )
import GHC.Core.Coercion
( mkReflCo, mkSymCo, mkTransCo
, mkUnivCo
#if MIN_VERSION_ghc(8,10,0)
, mkPrimEqPredRole
#endif
)
import GHC.Core.Coercion.Axiom
( Role(..) )
import GHC.Core.DataCon
( DataCon
, classDataCon, promoteDataCon
)
import GHC.Core.FamInstEnv
( FamInstEnv )
import GHC.Core.InstEnv
( InstEnvs(..) )
import GHC.Core.Make
import GHC.Core.Predicate
( EqRel(..)
#if MIN_VERSION_ghc(8,10,0)
, Pred(..)
#else
, PredTree(..), TyCoBinder
, mkPrimEqPred, mkReprPrimEqPred
#endif
, classifyPredType, mkClassPred
)
#if HAS_REWRITING
import GHC.Core.Reduction
( Reduction(..) )
#endif
import GHC.Core.TyCon
( TyCon(..) )
import GHC.Core.TyCo.Rep
( Type, PredType, Kind
, Coercion(..), CoercionHole(..)
, UnivCoProvenance(..)
#if MIN_VERSION_ghc(9,0,0)
, Mult
, mkInvisFunTyMany, mkInvisFunTysMany
#elif MIN_VERSION_ghc(8,10,0)
, mkInvisFunTy, mkInvisFunTys
#else
, mkFunTy, mkFunTys
#endif
#if MIN_VERSION_ghc(8,10,0)
, mkPiTy
#endif
, mkPiTys
, mkTyVarTy, mkTyVarTys
, mkForAllTy, mkForAllTys
)
import GHC.Core.Type
( eqType, mkTyConTy, mkTyConApp, splitTyConApp_maybe
, mkAppTy, mkAppTys, isTyVarTy, getTyVar_maybe
, mkCoercionTy, isCoercionTy, isCoercionTy_maybe
#if MIN_VERSION_ghc(9,0,0)
, pattern One, pattern Many
#endif
)
import GHC.Data.FastString
( FastString, fsLit )
import qualified GHC.Tc.Plugin
as GHC
import GHC.Tc.Types
( TcTyThing(..), TcGblEnv(..), TcLclEnv(..)
#if HAS_REWRITING
, TcPluginSolveResult(..), TcPluginRewriteResult(..)
, RewriteEnv(..)
#endif
)
import GHC.Tc.Types.Constraint
( Ct(..), CtLoc(..), CtEvidence(..), CtFlavour(..)
, QCInst(..), TcEvDest(..)
, ctPred, ctLoc, ctEvidence, ctEvExpr
, ctFlavour, ctEqRel, ctOrigin
, bumpCtLocDepth
, mkNonCanonical
)
import GHC.Tc.Types.Evidence
( EvBind(..), EvTerm(..), EvExpr, EvBindsVar(..)
, evCoercion, evCast, lookupEvBind, evDataConApp
)
import GHC.Tc.Types.Origin
( CtOrigin(..) )
import GHC.Tc.Utils.Monad
( newName )
import qualified GHC.Tc.Utils.Monad
as GHC
( traceTc, setCtLocM )
import GHC.Tc.Utils.TcType
( TcType, TcLevel, MetaDetails, MetaInfo
, isSkolemTyVar, isMetaTyVar
)
import GHC.Tc.Utils.TcMType
( isFilledMetaTyVar_maybe, writeMetaTyVar )
import GHC.Types.Id
( Id, mkLocalId )
import GHC.Types.Name
( Name )
import GHC.Types.Name.Occurrence
( OccName(..)
, mkVarOcc, mkDataOcc, mkTyVarOcc, mkTcOcc, mkClsOcc
)
import GHC.Types.SrcLoc
( GenLocated(..), Located, RealLocated
, unLoc, getLoc
)
import GHC.Types.Unique
( Unique )
#if MIN_VERSION_ghc(9,0,0)
import GHC.Types.Unique.FM as UniqFM
( UniqFM, emptyUFM, listToUFM )
#else
import qualified GHC.Types.Unique.FM as GHC
( UniqFM )
import GHC.Types.Unique.FM as UniqFM
( emptyUFM, listToUFM )
#endif
import GHC.Types.Unique.DFM
( UniqDFM, lookupUDFM, lookupUDFM_Directly, elemUDFM )
import GHC.Types.Var
( TyVar, CoVar, TcTyVar, EvVar
, mkTyVar
)
import GHC.Utils.Outputable
( Outputable(..), SDoc
#if !MIN_VERSION_ghc(9,2,0)
, panic, pprPanic
#endif
)
#if MIN_VERSION_ghc(9,2,0)
import GHC.Utils.Panic
( panic, pprPanic )
#endif
#if MIN_VERSION_ghc(9,2,0)
import GHC.Unit.Finder
( FindResult(..) )
#else
import GHC.Driver.Finder
( FindResult(..) )
#endif
import GHC.Unit.Module
( mkModuleName )
import GHC.Unit.Module.Name
( ModuleName )
import GHC.Unit.Types
( Module )
import Control.Monad.IO.Class
( MonadIO ( liftIO ) )
import GHC.TcPlugin.API.Internal
#ifndef HAS_REWRITING
import GHC.TcPlugin.API.Internal.Shim
#endif
tcPluginIO :: MonadTcPlugin m => IO a -> m a
tcPluginIO :: IO a -> m a
tcPluginIO = TcM a -> m a
forall (m :: * -> *) a. MonadTcPlugin m => TcM a -> m a
unsafeLiftTcM (TcM a -> m a) -> (IO a -> TcM a) -> IO a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IO a -> TcM a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO
tcPluginTrace :: MonadTcPlugin m
=> String
-> SDoc
-> m ()
tcPluginTrace :: String -> SDoc -> m ()
tcPluginTrace String
a SDoc
b = TcM () -> m ()
forall (m :: * -> *) a. MonadTcPlugin m => TcM a -> m a
unsafeLiftTcM (TcM () -> m ()) -> TcM () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> SDoc -> TcM ()
GHC.traceTc String
a SDoc
b
findImportedModule :: MonadTcPlugin m
=> ModuleName
-> Maybe FastString
-> m FindResult
findImportedModule :: ModuleName -> Maybe FastString -> m FindResult
findImportedModule ModuleName
mod_name Maybe FastString
mb_pkg = TcPluginM FindResult -> m FindResult
forall (m :: * -> *) a. MonadTcPlugin m => TcPluginM a -> m a
liftTcPluginM (TcPluginM FindResult -> m FindResult)
-> TcPluginM FindResult -> m FindResult
forall a b. (a -> b) -> a -> b
$ ModuleName -> Maybe FastString -> TcPluginM FindResult
GHC.findImportedModule ModuleName
mod_name Maybe FastString
mb_pkg
lookupOrig :: MonadTcPlugin m => Module -> OccName -> m Name
lookupOrig :: Module -> OccName -> m Name
lookupOrig Module
md = TcPluginM Name -> m Name
forall (m :: * -> *) a. MonadTcPlugin m => TcPluginM a -> m a
liftTcPluginM (TcPluginM Name -> m Name)
-> (OccName -> TcPluginM Name) -> OccName -> m Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Module -> OccName -> TcPluginM Name
GHC.lookupOrig Module
md
tcLookupTyCon :: MonadTcPlugin m => Name -> m TyCon
tcLookupTyCon :: Name -> m TyCon
tcLookupTyCon = TcPluginM TyCon -> m TyCon
forall (m :: * -> *) a. MonadTcPlugin m => TcPluginM a -> m a
liftTcPluginM (TcPluginM TyCon -> m TyCon)
-> (Name -> TcPluginM TyCon) -> Name -> m TyCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> TcPluginM TyCon
GHC.tcLookupTyCon
tcLookupDataCon :: MonadTcPlugin m => Name -> m DataCon
tcLookupDataCon :: Name -> m DataCon
tcLookupDataCon = TcPluginM DataCon -> m DataCon
forall (m :: * -> *) a. MonadTcPlugin m => TcPluginM a -> m a
liftTcPluginM (TcPluginM DataCon -> m DataCon)
-> (Name -> TcPluginM DataCon) -> Name -> m DataCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> TcPluginM DataCon
GHC.tcLookupDataCon
tcLookupClass :: MonadTcPlugin m => Name -> m Class
tcLookupClass :: Name -> m Class
tcLookupClass = TcPluginM Class -> m Class
forall (m :: * -> *) a. MonadTcPlugin m => TcPluginM a -> m a
liftTcPluginM (TcPluginM Class -> m Class)
-> (Name -> TcPluginM Class) -> Name -> m Class
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> TcPluginM Class
GHC.tcLookupClass
tcLookupGlobal :: MonadTcPlugin m => Name -> m TyThing
tcLookupGlobal :: Name -> m TyThing
tcLookupGlobal = TcPluginM TyThing -> m TyThing
forall (m :: * -> *) a. MonadTcPlugin m => TcPluginM a -> m a
liftTcPluginM (TcPluginM TyThing -> m TyThing)
-> (Name -> TcPluginM TyThing) -> Name -> m TyThing
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> TcPluginM TyThing
GHC.tcLookupGlobal
tcLookup :: MonadTcPlugin m => Name -> m TcTyThing
tcLookup :: Name -> m TcTyThing
tcLookup = TcPluginM TcTyThing -> m TcTyThing
forall (m :: * -> *) a. MonadTcPlugin m => TcPluginM a -> m a
liftTcPluginM (TcPluginM TcTyThing -> m TcTyThing)
-> (Name -> TcPluginM TcTyThing) -> Name -> m TcTyThing
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> TcPluginM TcTyThing
GHC.tcLookup
tcLookupId :: MonadTcPlugin m => Name -> m Id
tcLookupId :: Name -> m Id
tcLookupId = TcPluginM Id -> m Id
forall (m :: * -> *) a. MonadTcPlugin m => TcPluginM a -> m a
liftTcPluginM (TcPluginM Id -> m Id) -> (Name -> TcPluginM Id) -> Name -> m Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> TcPluginM Id
GHC.tcLookupId
getEnvs :: MonadTcPlugin m => m ( TcGblEnv, TcLclEnv )
getEnvs :: m (TcGblEnv, TcLclEnv)
getEnvs = TcPluginM (TcGblEnv, TcLclEnv) -> m (TcGblEnv, TcLclEnv)
forall (m :: * -> *) a. MonadTcPlugin m => TcPluginM a -> m a
liftTcPluginM TcPluginM (TcGblEnv, TcLclEnv)
GHC.getEnvs
getInstEnvs :: MonadTcPlugin m => m InstEnvs
getInstEnvs :: m InstEnvs
getInstEnvs = TcPluginM InstEnvs -> m InstEnvs
forall (m :: * -> *) a. MonadTcPlugin m => TcPluginM a -> m a
liftTcPluginM TcPluginM InstEnvs
GHC.getInstEnvs
getFamInstEnvs :: MonadTcPlugin m => m ( FamInstEnv, FamInstEnv )
getFamInstEnvs :: m (FamInstEnv, FamInstEnv)
getFamInstEnvs = TcPluginM (FamInstEnv, FamInstEnv) -> m (FamInstEnv, FamInstEnv)
forall (m :: * -> *) a. MonadTcPlugin m => TcPluginM a -> m a
liftTcPluginM TcPluginM (FamInstEnv, FamInstEnv)
GHC.getFamInstEnvs
matchFam :: MonadTcPlugin m
=> TyCon -> [ TcType ]
-> m ( Maybe Reduction )
matchFam :: TyCon -> [TcType] -> m (Maybe Reduction)
matchFam TyCon
tycon [TcType]
args =
#ifndef HAS_REWRITING
((Coercion, TcType) -> Reduction)
-> Maybe (Coercion, TcType) -> Maybe Reduction
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ( \ (Coercion
co,TcType
ty) -> Coercion -> TcType -> Reduction
mkReduction (Coercion -> Coercion
mkSymCo Coercion
co) TcType
ty ) (Maybe (Coercion, TcType) -> Maybe Reduction)
-> m (Maybe (Coercion, TcType)) -> m (Maybe Reduction)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
#endif
( TcPluginM (Maybe (Coercion, TcType))
-> m (Maybe (Coercion, TcType))
forall (m :: * -> *) a. MonadTcPlugin m => TcPluginM a -> m a
liftTcPluginM (TcPluginM (Maybe (Coercion, TcType))
-> m (Maybe (Coercion, TcType)))
-> TcPluginM (Maybe (Coercion, TcType))
-> m (Maybe (Coercion, TcType))
forall a b. (a -> b) -> a -> b
$ TyCon -> [TcType] -> TcPluginM (Maybe (Coercion, TcType))
GHC.matchFam TyCon
tycon [TcType]
args )
newUnique :: MonadTcPlugin m => m Unique
newUnique :: m Unique
newUnique = TcPluginM Unique -> m Unique
forall (m :: * -> *) a. MonadTcPlugin m => TcPluginM a -> m a
liftTcPluginM TcPluginM Unique
GHC.newUnique
newFlexiTyVar :: MonadTcPlugin m => Kind -> m TcTyVar
newFlexiTyVar :: TcType -> m Id
newFlexiTyVar = TcPluginM Id -> m Id
forall (m :: * -> *) a. MonadTcPlugin m => TcPluginM a -> m a
liftTcPluginM (TcPluginM Id -> m Id)
-> (TcType -> TcPluginM Id) -> TcType -> m Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcType -> TcPluginM Id
GHC.newFlexiTyVar
isTouchableTcPluginM :: MonadTcPlugin m => TcTyVar -> m Bool
isTouchableTcPluginM :: Id -> m Bool
isTouchableTcPluginM = TcPluginM Bool -> m Bool
forall (m :: * -> *) a. MonadTcPlugin m => TcPluginM a -> m a
liftTcPluginM (TcPluginM Bool -> m Bool)
-> (Id -> TcPluginM Bool) -> Id -> m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> TcPluginM Bool
GHC.isTouchableTcPluginM
zonkTcType :: MonadTcPluginWork m => TcType -> m TcType
zonkTcType :: TcType -> m TcType
zonkTcType = TcPluginM TcType -> m TcType
forall (m :: * -> *) a. MonadTcPlugin m => TcPluginM a -> m a
liftTcPluginM (TcPluginM TcType -> m TcType)
-> (TcType -> TcPluginM TcType) -> TcType -> m TcType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcType -> TcPluginM TcType
GHC.zonkTcType
zonkCt :: MonadTcPluginWork m => Ct -> m Ct
zonkCt :: Ct -> m Ct
zonkCt = TcPluginM Ct -> m Ct
forall (m :: * -> *) a. MonadTcPlugin m => TcPluginM a -> m a
liftTcPluginM (TcPluginM Ct -> m Ct) -> (Ct -> TcPluginM Ct) -> Ct -> m Ct
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> TcPluginM Ct
GHC.zonkCt
newWanted :: MonadTcPluginWork m => CtLoc -> PredType -> m CtEvidence
newWanted :: CtLoc -> TcType -> m CtEvidence
newWanted CtLoc
loc TcType
pty = TcPluginM CtEvidence -> m CtEvidence
forall (m :: * -> *) a. MonadTcPlugin m => TcPluginM a -> m a
liftTcPluginM (TcPluginM CtEvidence -> m CtEvidence)
-> TcPluginM CtEvidence -> m CtEvidence
forall a b. (a -> b) -> a -> b
$ CtLoc -> TcType -> TcPluginM CtEvidence
GHC.newWanted CtLoc
loc TcType
pty
newDerived :: MonadTcPluginWork m => CtLoc -> PredType -> m CtEvidence
newDerived :: CtLoc -> TcType -> m CtEvidence
newDerived CtLoc
loc TcType
pty = TcPluginM CtEvidence -> m CtEvidence
forall (m :: * -> *) a. MonadTcPlugin m => TcPluginM a -> m a
liftTcPluginM (TcPluginM CtEvidence -> m CtEvidence)
-> TcPluginM CtEvidence -> m CtEvidence
forall a b. (a -> b) -> a -> b
$ CtLoc -> TcType -> TcPluginM CtEvidence
GHC.newDerived CtLoc
loc TcType
pty
newGiven :: CtLoc -> PredType -> EvExpr -> TcPluginM Solve CtEvidence
newGiven :: CtLoc -> TcType -> EvExpr -> TcPluginM 'Solve CtEvidence
newGiven CtLoc
loc TcType
pty EvExpr
evtm = do
#if HAS_REWRITING
tc_evbinds <- askEvBinds
liftTcPluginM $ GHC.newGiven tc_evbinds loc pty evtm
#else
TcPluginM CtEvidence -> TcPluginM 'Solve CtEvidence
forall (m :: * -> *) a. MonadTcPlugin m => TcPluginM a -> m a
liftTcPluginM (TcPluginM CtEvidence -> TcPluginM 'Solve CtEvidence)
-> TcPluginM CtEvidence -> TcPluginM 'Solve CtEvidence
forall a b. (a -> b) -> a -> b
$ CtLoc -> TcType -> EvExpr -> TcPluginM CtEvidence
GHC.newGiven CtLoc
loc TcType
pty EvExpr
evtm
#endif
rewriteEnvCtLoc :: RewriteEnv -> CtLoc
rewriteEnvCtLoc :: RewriteEnv -> CtLoc
rewriteEnvCtLoc = RewriteEnv -> CtLoc
fe_loc
setCtLocM :: MonadTcPluginWork m => CtLoc -> m a -> m a
setCtLocM :: CtLoc -> m a -> m a
setCtLocM CtLoc
loc = (TcM a -> TcM a) -> m a -> m a
forall (m :: * -> *) a b.
MonadTcPlugin m =>
(TcM a -> TcM b) -> m a -> m b
unsafeLiftThroughTcM ( CtLoc -> TcM a -> TcM a
forall a. CtLoc -> TcM a -> TcM a
GHC.setCtLocM CtLoc
loc )
setCtLocRewriteM :: TcPluginM Rewrite a -> TcPluginM Rewrite a
setCtLocRewriteM :: TcPluginM 'Rewrite a -> TcPluginM 'Rewrite a
setCtLocRewriteM TcPluginM 'Rewrite a
ma = do
CtLoc
rewriteCtLoc <- RewriteEnv -> CtLoc
fe_loc (RewriteEnv -> CtLoc)
-> TcPluginM 'Rewrite RewriteEnv -> TcPluginM 'Rewrite CtLoc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcPluginM 'Rewrite RewriteEnv
askRewriteEnv
CtLoc -> TcPluginM 'Rewrite a -> TcPluginM 'Rewrite a
forall (m :: * -> *) a. MonadTcPluginWork m => CtLoc -> m a -> m a
setCtLocM CtLoc
rewriteCtLoc TcPluginM 'Rewrite a
ma
newEvVar :: PredType -> TcPluginM Solve EvVar
newEvVar :: TcType -> TcPluginM 'Solve Id
newEvVar = TcPluginM Id -> TcPluginM 'Solve Id
forall (m :: * -> *) a. MonadTcPlugin m => TcPluginM a -> m a
liftTcPluginM (TcPluginM Id -> TcPluginM 'Solve Id)
-> (TcType -> TcPluginM Id) -> TcType -> TcPluginM 'Solve Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcType -> TcPluginM Id
GHC.newEvVar
newCoercionHole :: PredType -> TcPluginM Solve CoercionHole
newCoercionHole :: TcType -> TcPluginM 'Solve CoercionHole
newCoercionHole = TcPluginM CoercionHole -> TcPluginM 'Solve CoercionHole
forall (m :: * -> *) a. MonadTcPlugin m => TcPluginM a -> m a
liftTcPluginM (TcPluginM CoercionHole -> TcPluginM 'Solve CoercionHole)
-> (TcType -> TcPluginM CoercionHole)
-> TcType
-> TcPluginM 'Solve CoercionHole
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcType -> TcPluginM CoercionHole
GHC.newCoercionHole
setEvBind :: EvBind -> TcPluginM Solve ()
setEvBind :: EvBind -> TcPluginM 'Solve ()
setEvBind EvBind
ev_bind = do
#if HAS_REWRITING
tc_evbinds <- askEvBinds
liftTcPluginM $ GHC.setEvBind tc_evbinds ev_bind
#else
TcPluginM () -> TcPluginM 'Solve ()
forall (m :: * -> *) a. MonadTcPlugin m => TcPluginM a -> m a
liftTcPluginM (TcPluginM () -> TcPluginM 'Solve ())
-> TcPluginM () -> TcPluginM 'Solve ()
forall a b. (a -> b) -> a -> b
$ EvBind -> TcPluginM ()
GHC.setEvBind EvBind
ev_bind
#endif
mkPluginUnivCo
:: String
-> Role
-> TcType
-> TcType
-> Coercion
mkPluginUnivCo :: String -> Role -> TcType -> TcType -> Coercion
mkPluginUnivCo String
str Role
role TcType
lhs TcType
rhs = UnivCoProvenance -> Role -> TcType -> TcType -> Coercion
mkUnivCo ( String -> UnivCoProvenance
PluginProv String
str ) Role
role TcType
lhs TcType
rhs
mkPluginUnivEvTerm
:: String
-> Role
-> TcType
-> TcType
-> EvTerm
mkPluginUnivEvTerm :: String -> Role -> TcType -> TcType -> EvTerm
mkPluginUnivEvTerm String
str Role
role TcType
lhs TcType
rhs = Coercion -> EvTerm
evCoercion (Coercion -> EvTerm) -> Coercion -> EvTerm
forall a b. (a -> b) -> a -> b
$ String -> Role -> TcType -> TcType -> Coercion
mkPluginUnivCo String
str Role
role TcType
lhs TcType
rhs
mkTyFamAppReduction
:: String
-> Role
-> TyCon
-> [TcType]
-> TcType
-> Reduction
mkTyFamAppReduction :: String -> Role -> TyCon -> [TcType] -> TcType -> Reduction
mkTyFamAppReduction String
str Role
role TyCon
tc [TcType]
args TcType
ty =
Coercion -> TcType -> Reduction
Reduction ( String -> Role -> TcType -> TcType -> Coercion
mkPluginUnivCo String
str Role
role ( TyCon -> [TcType] -> TcType
mkTyConApp TyCon
tc [TcType]
args ) TcType
ty ) TcType
ty
#if !MIN_VERSION_ghc(9,0,0)
type UniqFM ty a = GHC.UniqFM a
#if MIN_VERSION_ghc(8,10,0)
mkInvisFunTyMany :: Type -> Type -> Type
mkInvisFunTyMany :: TcType -> TcType -> TcType
mkInvisFunTyMany = TcType -> TcType -> TcType
mkInvisFunTy
mkInvisFunTysMany :: [Type] -> Type -> Type
mkInvisFunTysMany :: [TcType] -> TcType -> TcType
mkInvisFunTysMany = [TcType] -> TcType -> TcType
mkInvisFunTys
#else
type Pred = PredTree
mkInvisFunTyMany :: Type -> Type -> Type
mkInvisFunTyMany = mkFunTy
mkInvisFunTysMany :: [Type] -> Type -> Type
mkInvisFunTysMany = mkFunTys
mkPiTy :: TyCoBinder -> Type -> Type
mkPiTy bndr ty = mkPiTys [bndr] ty
mkPrimEqPredRole :: Role -> Type -> Type -> PredType
mkPrimEqPredRole Nominal = mkPrimEqPred
mkPrimEqPredRole Representational = mkReprPrimEqPred
mkPrimEqPredRole Phantom = panic "mkPrimEqPredRole phantom"
#endif
#endif