{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE UndecidableInstances #-}

{-|
Module: GHC.TcPlugin.API

This module provides a unified interface for writing type-checking plugins for GHC.

It attempts to re-export all the functionality from GHC that is relevant to plugin authors,
as well as providing utility functions to streamline certain common operations such as
creating evidence (to solve constraints), rewriting type family applications, throwing custom type errors.

Consider making use of the table of contents to help navigate this documentation;
don't hesitate to jump between sections to get an overview of the relevant aspects.

For an illustration of the functionality, check the examples in the associated
<https://github.com/sheaf/ghc-tcplugin-api GitHub repository>.

The internal module "GHC.TcPlugin.API.Internal" can be used to directly
lift and unlift computations in GHC's 'GHC.Tc.Types.TcM' monad, but it is hoped that
the interface provided in this module is sufficient.

-}

module GHC.TcPlugin.API
  ( -- * Basic TcPlugin functionality


    -- ** The 'TcPlugin' type

    TcPlugin(..)
  , mkTcPlugin

    -- ** Plugin state

    -- | A type-checker plugin can define its own state, corresponding to the existential parameter @s@

    -- in the definition of 'TcPlugin'.

    -- This allows a plugin to look up information a single time

    -- on initialisation, and pass it on for access in all further invocations of the plugin.

    --

    -- For example:

    --

    -- > data MyDefinitions { myTyFam :: !TyCon, myClass :: !Class }

    --

    -- Usually, the 'tcPluginInit' part of the plugin looks up all this information and returns it:

    --

    -- > myTcPluginInit :: TcPluginM Init MyDefinitions

    --

    -- This step should also be used to initialise any external tools,

    -- such as an external SMT solver.

    --

    -- This information will then be passed to other stages of the plugin:

    --

    -- > myTcPluginSolve :: MyDefinitions -> TcPluginSolver


    -- ** The type-checking plugin monads


    -- | Different stages of type-checking plugins have access to different information.

    -- For a unified interface, an MTL-style approach is used, with the 'MonadTcPlugin'

    -- typeclass providing overloading (for operations that work in all stages).

  , TcPluginStage(..), MonadTcPlugin
  , TcPluginM
  , tcPluginIO

    -- *** Emitting new work, and throwing type-errors


    -- | Some operations only make sense in the two main phases, solving and rewriting.

    -- This is captured by the 'MonadTcPluginWork' typeclass, which allows emitting

    -- new work, including throwing type errors.

  , MonadTcPluginWork
  , TcPluginErrorMessage(..)
  , mkTcPluginErrorTy

    -- * Name resolution


    -- | Name resolution is usually the first step in writing a type-checking plugin:

    -- plugins need to look up the names of the objects they want to manipulate.

    --

    -- For instance, to lookup the type family @MyFam@ in module @MyModule@ in package @my-pkg@:

    --

    -- > lookupMyModule :: MonadTcPlugin m => m Module

    -- > lookupMyModule = do

    -- >    findResult <- findImportedModule ( mkModuleName "MyModule" ) ( Just $ fsLit "my-pkg" )

    -- >    case findResult of

    -- >      Found _ myModule -> pure myModule

    -- >      _ -> error "MyPlugin couldn't find MyModule in my-pkg"

    -- >

    -- > lookupMyFam :: MonadTcPlugin m => Module -> m TyCon

    -- > lookupMyFam myModule = tcLookupTyCon =<< lookupOrig myModule ( mkTcOcc "MyFam" )

    --

    -- Most of these operations should be performed in 'tcPluginInit', and passed on

    -- to the other stages: the plugin initialisation is called only once in each module

    -- that the plugin is used, whereas the solver and rewriter are usually called repeatedly.


    -- ** Packages and modules


    -- | Use these functions to lookup a module,

    -- from the current package or imported packages.

  , findImportedModule, fsLit, mkModuleName
  , Module, ModuleName, FindResult(..)

    -- ** Names


    -- *** Occurence names


    -- | The most basic type of name is the 'OccName', which is a

    -- simple textual name within a namespace (e.g. the class namespace),

    -- without any disambiguation (no module qualifier, etc).

  , mkVarOcc, mkDataOcc, mkTyVarOcc, mkTcOcc, mkClsOcc

    -- *** Names


    -- | After having looked up the 'Module', we can obtain the full 'Name'

    -- referred to by an 'OccName'. This is fully unambiguous, as it

    -- contains a 'Unique' identifier for the name.

  , lookupOrig

    -- *** 'TyCon', 'Class', 'DataCon', etc


    -- | Finally, we can obtain the actual objects we're interested in handling,

    -- such as classes, type families, data constructors... by looking them up

    -- using their 'Name'.

  , tcLookupTyCon
  , tcLookupDataCon
  , tcLookupClass
  , tcLookupGlobal
  , tcLookup
  , tcLookupId
  , promoteDataCon

    -- * Constraint solving


    -- | Type-checking plugins will often want to manipulate constraints,

    -- e.g. solve constraints that GHC can't solve on its own, or emit

    -- their own constraints.

    --

    -- There are two different constraint flavours:

    --

    --   - Given constraints, which are already known and

    --     have evidence associated to them,

    --   - Wanted constraints, for which evidence has not yet been found.

    --

    -- When GHC can't solve a Wanted constraint, it will get reported to the

    -- user as a type error.


  , TcPluginSolver
#if HAS_REWRITING
  , TcPluginSolveResult(..)
#else
  , TcPluginSolveResult
  , pattern TcPluginContradiction, pattern TcPluginOk
#endif

    -- | The 'tcPluginSolve' method of a typechecker plugin will be invoked

    -- in two different ways:

    --

    -- 1. to simplify Given constraints. In this case, the 'tcPluginSolve' function

    --    will not be passed any Wanted constraints, and

    -- 2. to solve Wanted constraints.

    --

    -- The plugin can then respond in one of two ways:

    --

    --   - with @TcPluginOk solved new@, where @solved@ is a list of solved constraints

    --     and @new@ is a list of new constraints for GHC to process;

    --   - with @TcPluginContradiction contras@, where @contras@ is a list of impossible

    --     constraints, so that they can be turned into errors.

    --

    -- In both cases, the plugin must respond with constraints of the same flavour,

    -- i.e. in (1) it should return only Givens, and for (2) it should return only

    -- Wanteds; all other constraints will be ignored.


    -- ** Getting started with constraint solving


    -- | To get started, it can be helpful to immediately print out all the constraints

    -- that the plugin is given, using 'tcPluginTrace':

    --

    -- > solver _ givens wanteds = do

    -- >   tcPluginTrace "---Plugin start---" (ppr givens $$ ppr wanteds)

    -- >   pure $ TcPluginOk [] []

    --

    -- This creates a plugin that prints outs the constraints it is passed,

    -- without doing anything with them.

    --

    -- To see this output, you will need to pass the flags @-ddump-tc-trace@

    -- and @-ddump-to-file@ to GHC. This will output the trace as a log file,

    -- and you can search for @"---Plugin start---"@ to find the plugin inputs.

    --

    -- Note that pretty-printing in GHC is done using the 'Outputable' type class.

    -- We use its 'ppr' method to turn things into pretty-printable documents,

    -- and '($$)' to combine documents vertically.

    -- If you need more capabilities for pretty-printing documents,

    -- import GHC's "GHC.Utils.Outputable" module.

  , tcPluginTrace

    -- ** Inspecting constraints & predicates


    -- *** Canonical and non-canonical constraints


    -- | A constraint in GHC starts out as "non-canonical", which means that

    -- GHC doesn't know what type of constraint it is.

    -- GHC will inspect the constraint to turn it into a canonical form

    -- (class constraint, equality constraint, etc.) which satisfies certain

    -- invariants used during constraint solving.

    --

    -- Thus, whenever emitting new constraints, it is usually best to emit a

    -- non-canonical constraint, letting GHC canonicalise it.

  , mkNonCanonical

    -- *** Predicates


    -- | A type-checking plugin will usually need to inspect constraints,

    -- so that it can pick out the constraints it is going to interact with.

    --

    -- In general, type-checking plugins can encounter all sorts of constraints,

    -- whether in canonical form or not.

    -- In order to handle these constraints in a uniform manner, it is usually

    -- preferable to inspect each constraint's predicate, which can be obtained

    -- by using 'classifyPredType' and 'ctPred'.

    --

    -- This allows the plugin to determine what kind of constraints it is dealing with:

    --

    --   - an equality constraint? at 'Nominal' or 'Representational' role?

    --   - a type-class constraint? for which class?

    --   - an irreducible constraint, e.g. something of the form @c a@?

    --   - a quantified constraint?

  , Pred
  , pattern ClassPred, pattern EqPred, pattern IrredPred, pattern ForAllPred
  , classifyPredType, ctPred

    -- | == Handling type variables

  , TyVar, CoVar
  , MetaDetails, MetaInfo
  , isSkolemTyVar
  , isMetaTyVar, isFilledMetaTyVar_maybe
  , writeMetaTyVar

    -- | == Some further functions for inspecting constraints

  , eqType
  , ctLoc, ctEvidence, ctFlavour, ctEqRel, ctOrigin

    -- ** Constraint evidence


    -- *** Coercions


    -- | 'GHC.Core.TyCo.Rep.Coercion's are the evidence for type equalities.

    -- As such, when proving an equality, a type-checker plugin needs

    -- to construct the associated coercions.

  , mkPluginUnivCo
  , newCoercionHole
  , mkReflCo, mkSymCo, mkTransCo, mkUnivCo
  , mkCoercionTy, isCoercionTy, isCoercionTy_maybe

    -- *** Evidence terms


    -- | Typeclass constraints have a different notion of evidence: evidence terms.

    --

    -- A plugin that wants to solve a class constraint will need to provide

    -- an evidence term. Such evidence can be created from scratch, or it can be obtained

    -- by combining evidence that is already available.


  , mkPluginUnivEvTerm
  , evDataConApp
  , newEvVar, setEvBind
  , evCoercion, evCast
  , ctEvExpr
  , askEvBinds, lookupEvBind, eb_lhs, eb_rhs
  , newName, mkLocalId, mkTyVar
  , ctev_pred, ctev_evar, ctev_loc, ctev_dest

    -- *** Class dictionaries


    -- | To create evidence terms for class constraints, type-checking plugins

    -- need to be able to construct the appropriate dictionaries containing

    -- the values for the class methods.

    --

    -- The class dictionary constructor can be obtained using 'classDataCon'.

    -- Functions from "GHC.Core.Make", re-exported here, will be useful for

    -- constructing the necessary terms.

    --

    -- For instance, we can apply the class data constructor using 'mkCoreConApps'.

    -- Remember that the type-level arguments (the typeclass variables) come first,

    -- before the actual evidence term (the class dictionary expression).


  , classDataCon
  , module GHC.Core.Make

    -- | ==== Class instances


    -- | In some cases, a type-checking plugin might need to access the

    -- class instances that are currently in scope, e.g. to obtain certain

    -- evidence terms.

  , getInstEnvs

    -- ** Emitting new constraints


  , newWanted, newGiven

    -- | The following functions allow plugins to create constraints

    -- for typeclasses and type equalities.

  , mkClassPred, mkPrimEqPredRole

    -- | === Deriveds


    -- | Derived constraints are like Wanted constraints, except that they

    -- don't require evidence in order to be solved, and won't be seen

    -- in error messages if they go unsolved.

    --

    -- Solver plugins usually ignore this type of constraint entirely.

    -- They occur mostly when dealing with functional dependencies and type-family

    -- injectivity annotations.

    --

    -- GHC 9.4 removes this flavour of constraints entirely, subsuming their uses into

    -- Wanted constraints.

  , askDeriveds, newDerived

    -- ** Location information and 'CtLoc's


    -- | When creating new constraints, one still needs a mechanism allowing GHC

    -- to report a certain source location associated to them when throwing an error,

    -- as well as other information the type-checker was aware of at that point

    -- (e.g. available instances, given constraints, etc).

    --

    -- This is the purpose of 'CtLoc'.

  , setCtLocM
  , setCtLocRewriteM

    -- | 'bumpCtLocDepth' adds one to the "depth" of the constraint.

    -- Can help avoid loops, by triggering a "maximum depth exceeded" error.

  , bumpCtLocDepth

    -- * Rewriting type-family applications


  , TcPluginRewriter, TcPluginRewriteResult(..)

    -- ** Querying for type family reductions


  , matchFam
  , getFamInstEnvs
  , FamInstEnv

    -- ** Specifying type family reductions


    -- | A plugin that wants to rewrite a type family application must provide two

    -- pieces of information:

    --

    --   - the type that the type family application reduces to,

    --   - evidence for this reduction, i.e. a 'GHC.Core.TyCo.Rep.Coercion' proving the equality.

    --

    -- In the rewriting stage, type-checking plugins have access to the rewriter

    -- environment 'RewriteEnv', which has information about the location of the

    -- type family application, the local type-checking environment, among other things.

    --

    -- Note that a plugin should provide a 'UniqFM' from 'TyCon' to rewriting functions,

    -- which specifies a rewriting function for each type family.

    -- Use 'emptyUFM' or 'listToUFM' to construct this map,

    -- or import the GHC module "GHC.Types.Unique.FM" for a more complete API.

  , askRewriteEnv, rewriteEnvCtLoc, RewriteEnv
  , mkTyFamAppReduction, Reduction(..)

    -- * Handling Haskell types


    -- ** Type variables

  , newUnique
  , newFlexiTyVar
  , isTouchableTcPluginM
  , mkTyVarTy, mkTyVarTys
  , isTyVarTy, getTyVar_maybe
  , TcType, TcTyVar, Unique, Kind

    -- ** Creating and decomposing applications

  , mkTyConTy, mkTyConApp, splitTyConApp_maybe
  , mkAppTy, mkAppTys

    -- ** Function types

  , mkInvisFunTyMany, mkInvisFunTysMany
  , mkForAllTy, mkForAllTys
  , mkPiTy, mkPiTys

#if MIN_VERSION_ghc(9,0,0)
  , Mult, pattern One, pattern Many
#endif

    -- ** Zonking


    -- | Zonking is the operation in which GHC actually switches out mutable unification variables

    -- for their actual filled in type.

    --

    -- See the Note [What is zonking?] in GHC's source code for more information.

  , zonkTcType
  , zonkCt

    -- ** Panicking


    -- | It is often better for type-checking plugins to panic when encountering a problem,

    -- as opposed to silently doing something wrong. Use 'pprPanic' to throw an informative

    -- error message, so that users of your plugin can report an issue if a problem occurs.

  , panic, pprPanic

    -- ** Map-like data structures based on 'Unique's


    -- | Import "GHC.Types.Unique.FM" or "GHC.Types.Unique.DFM" for

    -- a more complete interface to maps whose keys are 'Unique's.


  , UniqDFM
  , lookupUDFM, lookupUDFM_Directly, elemUDFM
  , UniqFM
  , emptyUFM, listToUFM

    -- * The type-checking environment

  , getEnvs

    -- * Built-in types


    -- | This module also re-exports the built-in types that GHC already knows about.

    --

    -- This allows plugins to directly refer to e.g. the promoted data constructor

    -- 'True' without having to look up its name.

  , module GHC.Builtin.Types

    -- * GHC types


    -- | These are the types that the plugin will inspect and manipulate.


    -- | = END OF API DOCUMENTATION, RE-EXPORTS FOLLOW


    -- | == Names

  , Name, OccName, TyThing, TcTyThing
  , Class(classTyCon), DataCon, TyCon, Id
  , FastString

    -- | == Constraints

  , EqRel(..), FunDep, CtFlavour
  , Ct, CtLoc, CtEvidence, CtOrigin
  , QCInst
  , Type, PredType
  , InstEnvs, TcLevel

    -- | === Coercions and evidence

  , Coercion, Role(..), UnivCoProvenance
  , CoercionHole(..)
  , EvBind, EvTerm(EvExpr), EvVar, EvExpr, EvBindsVar
  , Expr(Var, Type, Coercion), CoreBndr
  , TcEvDest(..)

    -- | == The type-checking environment

  , TcGblEnv, TcLclEnv

    -- | == Source locations

  , GenLocated(..), Located, RealLocated
  , unLoc, getLoc

    -- | == Pretty-printing

  , SDoc, Outputable(..)

  )
  where

-- ghc

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 )

-- transformers

import Control.Monad.IO.Class
  ( MonadIO ( liftIO ) )

-- ghc-tcplugin-api

import GHC.TcPlugin.API.Internal
#ifndef HAS_REWRITING
import GHC.TcPlugin.API.Internal.Shim
#endif

--------------------------------------------------------------------------------


-- | Run an 'IO' computation within the plugin.

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

-- | Output some debugging information within the plugin.

tcPluginTrace :: MonadTcPlugin m
              => String -- ^ Text at the top of the debug message.

              -> SDoc   -- ^ Formatted document to print (use the 'ppr' pretty-printing function to obtain an 'SDoc' from any 'Outputable')

              -> 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

--------------------------------------------------------------------------------


-- | Lookup a Haskell module from the given package.

findImportedModule :: MonadTcPlugin m
                   => ModuleName -- ^ Module name, e.g. @"Data.List"@.

                   -> Maybe FastString -- ^ Package name, e.g. @Just "base"@.

                                       -- Use @Nothing@ for the current home package

                   -> 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

-- | Obtain the full internal 'Name' (with its unique identifier, etc) from its 'OccName'.

--

-- Example usage:

--

-- > lookupOrig preludeModule ( mkTcOcc "Bool" )

--

-- This will obtain the 'Name' associated with the type 'Bool'.

--

-- You can then call 'tcLookupTyCon' to obtain the associated 'TyCon'.

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

-- | Lookup a type constructor from its name (datatype, type synonym or type family).

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

-- | Lookup a data constructor (such as 'True', 'Just', ...) from its name.

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

-- | Lookup a typeclass from its name.

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

-- | Lookup a global typecheckable-thing from its name.

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

-- | Lookup a typecheckable-thing available in a local context,

-- such as a local type variable.

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

-- | Lookup an identifier, such as a type variable.

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

--------------------------------------------------------------------------------


{-
getTopEnv :: MonadTcPlugin m => m HscEnv
getTopEnv = liftTcPluginM GHC.getTopEnv
-}

-- | Obtain the current global and local type-checking environments.

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

-- | Obtain all currently-reachable typeclass instances.

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

-- | Obtain all currently-reachable data/type family instances.

--

-- First result: external instances.

-- Second result: instances in the current home package.

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

-- | Ask GHC what a type family application reduces to.

--

-- __Warning__: can cause a loop when used within 'tcPluginRewrite'.

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
<$>
  -- GHC 9.0 and 9.2 use a different orientation

  -- when rewriting type family applications.

#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 )

--------------------------------------------------------------------------------


-- | Create a new unique. Useful for generating new variables in the plugin.

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

-- | Create a new meta-variable (unification variable) of the given kind.

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

-- | Query whether a type variable is touchable:

--   - is it a unification variable (and not a skolem variable)?

--   - is it actually unifiable given the current 'TcLevel'?

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

--------------------------------------------------------------------------------


-- | Zonk the given type, which takes the metavariables in the type and

-- substitutes their actual value.

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

-- | Zonk a given constraint.

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

--------------------------------------------------------------------------------


-- | Create a new derived constraint.

--

-- Requires a location (so that error messages can say where the constraint came from,

-- what things were in scope at that point, etc), as well as the actual constraint (encoded as a type).

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

-- | Create a new derived constraint. See also 'newWanted'.

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

-- | Create a new given constraint.

--

-- Unlike 'newWanted' and 'newDerived', we need to supply evidence

-- for this constraint.

--

-- Use 'setCtLocM' to pass along the location information,

-- as only the 'CtOrigin' gets taken into account here.

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


-- | Obtain the 'CtLoc' from a 'RewriteEnv'.

--

-- This can be useful to obtain the location of the

-- constraint currently being rewritten,

-- so that newly emitted constraints can be given

-- the same location information.

rewriteEnvCtLoc :: RewriteEnv -> CtLoc
rewriteEnvCtLoc :: RewriteEnv -> CtLoc
rewriteEnvCtLoc = RewriteEnv -> CtLoc
fe_loc

-- | Set the location information for a computation,

-- so that the constraint solver reports an error at the given location.

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 )

-- | Use the 'RewriteEnv' to set the 'CtLoc' for a computation.

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

--------------------------------------------------------------------------------


-- | Create a fresh evidence variable.

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

-- | Create a fresh coercion hole.

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

-- | Bind an evidence variable.

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

--------------------------------------------------------------------------------


-- | Conjure up a coercion witnessing an equality between two types

-- at the given 'Role' ('Nominal' or 'Representational').

--

-- This amounts to telling GHC "believe me, these things are equal".

--

-- The plugin is responsible for not emitting any unsound coercions,

-- such as a coercion between 'Int' and 'Float'.

mkPluginUnivCo
  :: String -- ^ Name of equality (for the plugin's internal use, or for debugging)

  -> Role
  -> TcType -- ^ LHS

  -> TcType -- ^ RHS

  -> 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

-- | Conjure up an evidence term for an equality between two types

-- at the given 'Role' ('Nominal' or 'Representational').

--

-- This can be used to supply a proof of a wanted equality in 'TcPluginOk'.

--

-- The plugin is responsible for not emitting any unsound equalities,

-- such as an equality between 'Int' and 'Float'.

mkPluginUnivEvTerm
  :: String -- ^ Name of equality (for the plugin's internal use, or for debugging)

  -> Role
  -> TcType -- ^ LHS

  -> TcType -- ^ RHS

  -> 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

-- | Provide a rewriting of a saturated type family application

-- at the given 'Role' ('Nominal' or 'Representational').

--

-- The result can be passed to 'TcPluginRewriteTo' to specify the outcome

-- of rewriting a type family application.

mkTyFamAppReduction
  :: String   -- ^ Name of reduction (for debugging)

  -> Role     -- ^ Role of reduction ('Nominal' or 'Representational')

  -> TyCon    -- ^ Type family 'TyCon'

  -> [TcType] -- ^ Type family arguments

  -> TcType   -- ^ The type that the type family application reduces to

  -> 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

-- | Makes a lifted equality predicate at the given role

mkPrimEqPredRole :: Role -> Type -> Type -> PredType
mkPrimEqPredRole Nominal          = mkPrimEqPred
mkPrimEqPredRole Representational = mkReprPrimEqPred
mkPrimEqPredRole Phantom          = panic "mkPrimEqPredRole phantom"

#endif
#endif