ghc-tcplugin-api (empty) → 0.2.0.0
raw patch · 5 files changed
+2347/−0 lines, 5 filesdep +basedep +ghcdep +transformers
Dependencies added: base, ghc, transformers
Files
- changelog.md +5/−0
- ghc-tcplugin-api.cabal +67/−0
- src/GHC/TcPlugin/API.hs +800/−0
- src/GHC/TcPlugin/API/Internal.hs +584/−0
- src/GHC/TcPlugin/API/Internal/Shim.hs +891/−0
+ changelog.md view
@@ -0,0 +1,5 @@+ + +# Version 0.2.0.0 (2021-07-22) + +Initial release on Hackage.
+ ghc-tcplugin-api.cabal view
@@ -0,0 +1,67 @@+cabal-version: 3.0 +name: ghc-tcplugin-api +version: 0.2.0.0 +synopsis: An API for type-checker plugins. +license: BSD-3-Clause +build-type: Simple +author: Sam Derbyshire +maintainer: Sam Derbyshire +copyright: 2021 Sam Derbyshire +homepage: https://github.com/sheaf/ghc-tcplugin-api +category: Type System, GHC, Plugin +description: + + This library provides a streamlined monadic interface + for writing GHC type-checking plugins. + + Each stage in a type-checking plugin (initialisation, solving, rewriting, + shutdown) has a corresponding monad, preventing operations that are only + allowed in some stages to be used in the other stages. + Operations that work across multiple stages are overloaded across monads + using MTL-like typeclasses. + + Some operations, like creating evidence for constraints or creating + custom type error messages, are also simplified. + + Please refer to the <https://github.com/sheaf/ghc-tcplugin-api associated GitHub repository> + for example usage. + +extra-source-files: + changelog.md + +library + + build-depends: + base + >= 4.15.0 && < 4.18, + ghc + >= 9.0 && < 9.5, + transformers + >= 0.5 && < 0.6, + + default-language: + Haskell2010 + + ghc-options: + -Wall + -Wcompat + -fwarn-missing-local-signatures + -fwarn-incomplete-uni-patterns + -fwarn-missing-deriving-strategies + -fno-warn-unticked-promoted-constructors + + hs-source-dirs: + src + + exposed-modules: + GHC.TcPlugin.API, + GHC.TcPlugin.API.Internal + + if impl(ghc >= 9.3.0) + cpp-options: -DHAS_REWRITING + else + other-modules: + GHC.TcPlugin.API.Internal.Shim + + if impl(ghc < 9.5.0) + cpp-options: -DHAS_DERIVEDS
+ src/GHC/TcPlugin/API.hs view
@@ -0,0 +1,800 @@+{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# 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.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? + , classifyPredType, ctPred + + -- | == 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 + , pattern Coercion + + -- *** 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 + , newEvVar, setEvBind + , evCoercion, evCast + , ctEvExpr + , pattern Type +--, askEvBinds + + -- *** 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, e.g. 'mkCoreApp' for an application. + + , 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 + + , AnonArgFlag(..), Mult + , mkFunTy, mkVisFunTy, mkInvisFunTy, mkVisFunTys + , mkForAllTy, mkForAllTys, mkInvisForAllTys + , mkPiTy, mkPiTys + , mkFunTyMany + , mkScaledFunTy + , mkVisFunTyMany, mkVisFunTysMany + , mkInvisFunTyMany, mkInvisFunTysMany + + -- ** 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 + + -- ** 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 + , Pred(..), EqRel(..), FunDep, CtFlavour + , Ct, CtLoc, CtEvidence, CtOrigin + , QCInst +#if MIN_VERSION_ghc(9,2,0) + , CanEqLHS +#endif + , Type, PredType + , InstEnvs, TcLevel + + -- | === Coercions and evidence + , Coercion, Role(..), UnivCoProvenance + , CoercionHole + , EvBind, EvTerm, EvVar, EvExpr, EvBindsVar + + -- | == The type-checking environment + , TcGblEnv, TcLclEnv + + -- | == Pretty-printing + , SDoc, Outputable(..) + + ) + where + +-- ghc +import GHC + ( TyThing(..) ) +import GHC.Builtin.Types +import GHC.Core + ( Expr(Type, Coercion) ) +import GHC.Core.Class + ( Class(..), FunDep ) +import GHC.Core.Coercion + ( mkReflCo, mkSymCo, mkTransCo + , mkUnivCo, mkPrimEqPredRole +#if HAS_REWRITING + , Reduction(..) +#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 + ( Pred(..), EqRel(..) + , classifyPredType, mkClassPred + ) +import GHC.Core.TyCon + ( TyCon(..) ) +import GHC.Core.TyCo.Rep + ( Type, PredType, Kind + , Coercion(..), CoercionHole(..) + , UnivCoProvenance(..) + , AnonArgFlag(..), Mult + , mkTyVarTy, mkTyVarTys + , mkFunTy, mkVisFunTy, mkInvisFunTy, mkVisFunTys + , mkForAllTy, mkForAllTys, mkInvisForAllTys + , mkPiTy, mkPiTys + , mkFunTyMany + , mkScaledFunTy + , mkVisFunTyMany, mkVisFunTysMany + , mkInvisFunTyMany, mkInvisFunTysMany + ) +import GHC.Core.Type + ( eqType, mkTyConTy, mkTyConApp, splitTyConApp_maybe + , mkAppTy, mkAppTys, isTyVarTy, getTyVar_maybe + , mkCoercionTy, isCoercionTy, isCoercionTy_maybe + ) +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(..) +#else + , TcPluginResult(..) +#endif + ) +import GHC.Tc.Types.Constraint + ( Ct(..), CtLoc(..), CtEvidence(..), CtFlavour(..) + , QCInst(..) +#if MIN_VERSION_ghc(9,2,0) + , CanEqLHS(..) +#endif + , ctPred, ctLoc, ctEvidence, ctEvExpr + , ctFlavour, ctEqRel, ctOrigin + , bumpCtLocDepth + , mkNonCanonical + ) +import GHC.Tc.Types.Evidence + ( EvBind(..), EvTerm(..), EvExpr, EvBindsVar(..) + , evCoercion, evCast + ) +import GHC.Tc.Types.Origin + ( CtOrigin(..) ) +import qualified GHC.Tc.Utils.Monad + as GHC + ( traceTc, setCtLocM ) +import GHC.Tc.Utils.TcType + ( TcType, TcLevel ) +import GHC.Types.Name + ( Name ) +import GHC.Types.Name.Occurrence + ( OccName(..) + , mkVarOcc, mkDataOcc, mkTyVarOcc, mkTcOcc, mkClsOcc + ) +import GHC.Types.Unique + ( Unique ) +import GHC.Types.Unique.FM + ( UniqFM, emptyUFM, listToUFM ) +import GHC.Types.Unique.DFM + ( UniqDFM, lookupUDFM, lookupUDFM_Directly, elemUDFM ) +import GHC.Types.Var + ( Id, TcTyVar, EvVar ) +import GHC.Utils.Outputable + ( Outputable(..), SDoc ) +#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 = unsafeLiftTcM . 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 a b = unsafeLiftTcM $ GHC.traceTc a 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 mod_name mb_pkg = liftTcPluginM $ GHC.findImportedModule mod_name 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 md = liftTcPluginM . GHC.lookupOrig md + +-- | Lookup a type constructor from its name (datatype, type synonym or type family). +tcLookupTyCon :: MonadTcPlugin m => Name -> m TyCon +tcLookupTyCon = liftTcPluginM . GHC.tcLookupTyCon + +-- | Lookup a data constructor (such as 'True', 'Just', ...) from its name. +tcLookupDataCon :: MonadTcPlugin m => Name -> m DataCon +tcLookupDataCon = liftTcPluginM . GHC.tcLookupDataCon + +-- | Lookup a typeclass from its name. +tcLookupClass :: MonadTcPlugin m => Name -> m Class +tcLookupClass = liftTcPluginM . GHC.tcLookupClass + +-- | Lookup a global typecheckable-thing from its name. +tcLookupGlobal :: MonadTcPlugin m => Name -> m TyThing +tcLookupGlobal = liftTcPluginM . GHC.tcLookupGlobal + +-- | Lookup a typecheckable-thing available in a local context, +-- such as a local type variable. +tcLookup :: MonadTcPlugin m => Name -> m TcTyThing +tcLookup = liftTcPluginM . GHC.tcLookup + +-- | Lookup an identifier, such as a type variable. +tcLookupId :: MonadTcPlugin m => Name -> m Id +tcLookupId = liftTcPluginM . 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 = liftTcPluginM GHC.getEnvs + +-- | Obtain all currently-reachable typeclass instances. +getInstEnvs :: MonadTcPlugin m => m InstEnvs +getInstEnvs = liftTcPluginM 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 = liftTcPluginM 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 args = +#ifndef HAS_REWRITING + fmap mkReduction <$> +#endif + ( liftTcPluginM $ GHC.matchFam tycon args ) + +-------------------------------------------------------------------------------- + +-- | Create a new unique. Useful for generating new variables in the plugin. +newUnique :: MonadTcPlugin m => m Unique +newUnique = liftTcPluginM GHC.newUnique + +-- | Create a new meta-variable (unification variable) of the given kind. +newFlexiTyVar :: MonadTcPlugin m => Kind -> m TcTyVar +newFlexiTyVar = liftTcPluginM . 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 = liftTcPluginM . 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 = liftTcPluginM . GHC.zonkTcType + +-- | Zonk a given constraint. +zonkCt :: MonadTcPluginWork m => Ct -> m Ct +zonkCt = liftTcPluginM . 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 loc pty = liftTcPluginM $ GHC.newWanted loc pty + +-- | Create a new derived constraint. See also 'newWanted'. +newDerived :: MonadTcPluginWork m => CtLoc -> PredType -> m CtEvidence +newDerived loc pty = liftTcPluginM $ GHC.newDerived loc 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 loc pty evtm = do +#if HAS_REWRITING + tc_evbinds <- askEvBinds + liftTcPluginM $ GHC.newGiven tc_evbinds loc pty evtm +#else + liftTcPluginM $ GHC.newGiven loc pty 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 = 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 loc = unsafeLiftThroughTcM ( GHC.setCtLocM loc ) + +-- | Use the 'RewriteEnv' to set the 'CtLoc' for a computation. +setCtLocRewriteM :: TcPluginM Rewrite a -> TcPluginM Rewrite a +setCtLocRewriteM ma = do + rewriteCtLoc <- fe_loc <$> askRewriteEnv + setCtLocM rewriteCtLoc ma + +-------------------------------------------------------------------------------- + +-- | Create a fresh evidence variable. +newEvVar :: PredType -> TcPluginM Solve EvVar +newEvVar = liftTcPluginM . GHC.newEvVar + +-- | Create a fresh coercion hole. +newCoercionHole :: PredType -> TcPluginM Solve CoercionHole +newCoercionHole = liftTcPluginM . GHC.newCoercionHole + +-- | Bind an evidence variable. +setEvBind :: EvBind -> TcPluginM Solve () +setEvBind ev_bind = do +#if HAS_REWRITING + tc_evbinds <- askEvBinds + liftTcPluginM $ GHC.setEvBind tc_evbinds ev_bind +#else + liftTcPluginM $ GHC.setEvBind 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 str role lhs rhs = mkUnivCo ( PluginProv str ) role lhs 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 str role lhs rhs = evCoercion $ mkPluginUnivCo str role lhs 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 str role tc args ty = + Reduction ty ( mkPluginUnivCo str role ty ( mkTyConApp tc args ) )
+ src/GHC/TcPlugin/API/Internal.hs view
@@ -0,0 +1,584 @@+{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DerivingVia #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} + +{-| +Module: GHC.TcPlugin.API.Internal + +This module provides operations to directly lift and unlift computations in +GHC's 'GHC.Tc.TcM' monad to the various type-checking plugin monads, in the form +of the functions + + > unsafeLiftTcM :: TcM a -> m a + + > unsafeWithRunInTcM :: ( ( forall a. m a -> TcM a ) -> TcM b ) -> m b + +Here 'GHC.Tc.TcM' is GHC's internal type-checker monad. + +It also exposes extra environment available in the solving/rewriting stages: + + > askRewriteEnv :: TcPluginM Rewrite RewriteEnv + + > askEvBinds :: TcPluginM Solve EvBindsVar + +It is hoped that none of these internal operations are necessary, and that users +can fulfill their needs without importing this internal module. + +Please file a bug on the issue tracker if you have encountered a situation +which requires the import of this module. + +-} + +module GHC.TcPlugin.API.Internal + ( -- * Internal functions and types + MonadTcPlugin(..), MonadTcPluginWork + , unsafeLiftThroughTcM + -- * Re-exported functions and types + , TcPlugin(..), TcPluginStage(..) + , TcPluginSolver + , TcPluginM(..) + , TcPluginErrorMessage(..) + , TcPluginRewriter + , askRewriteEnv + , askDeriveds + , askEvBinds + , mkTcPlugin + , mkTcPluginErrorTy + ) + where + +-- base +#ifndef HAS_REWRITING +import Data.IORef + ( IORef, newIORef ) +#endif +import Data.Kind + ( Constraint, Type ) +import GHC.TypeLits + ( TypeError, ErrorMessage(..) ) + +-- transformers +import Control.Monad.Trans.Reader + ( ReaderT(..) ) + +-- ghc +import qualified GHC.Builtin.Names + as GHC.TypeLits + ( errorMessageTypeErrorFamName + , typeErrorTextDataConName + , typeErrorAppendDataConName + , typeErrorVAppendDataConName + , typeErrorShowTypeDataConName + ) +import qualified GHC.Builtin.Types + as GHC + ( constraintKind ) +import qualified GHC.Core.DataCon + as GHC + ( promoteDataCon ) +import qualified GHC.Core.TyCon + as GHC + ( TyCon ) +import qualified GHC.Core.TyCo.Rep + as GHC + ( PredType, Type(..), TyLit(..) ) +import qualified GHC.Core.Type + as GHC + ( mkTyConApp, tcTypeKind ) +import qualified GHC.Data.FastString + as GHC + ( fsLit ) +import qualified GHC.Tc.Plugin + as GHC + ( tcLookupDataCon, tcLookupTyCon +#ifndef HAS_REWRITING + , tcPluginIO +#endif + ) +import qualified GHC.Tc.Types + as GHC + ( TcM, TcPlugin(..), TcPluginM + , TcPluginSolver +#ifdef HAS_REWRITING + , TcPluginRewriter +#else + , getEvBindsTcPluginM +#endif + , runTcPluginM, unsafeTcPluginTcM + ) +#ifdef HAS_REWRITING +import GHC.Tc.Types + ( TcPluginSolveResult + , TcPluginRewriteResult + , RewriteEnv + ) +#endif +import qualified GHC.Tc.Types.Constraint + as GHC + ( Ct ) +import qualified GHC.Tc.Types.Evidence + as GHC + ( EvBindsVar ) +import qualified GHC.Types.Unique.FM + as GHC + ( UniqFM ) +#ifndef HAS_REWRITING +import qualified GHC.Types.Unique.DFM + as GHC + ( emptyUDFM ) +#endif + +-- ghc-tcplugin-api +#ifndef HAS_REWRITING +import GHC.TcPlugin.API.Internal.Shim + ( TcPluginSolveResult, TcPluginRewriteResult(..) + , RewrittenTyFamApps, RewriteEnv + , shimRewriter + ) +#endif + +-------------------------------------------------------------------------------- +-- Public types and functions. + +-- | Stage of a type-checking plugin, used as a data kind. +data TcPluginStage + = Init + | Solve + | Rewrite + | Stop + +-- | The @solve@ function of a type-checking plugin takes in Given and Wanted +-- constraints, and should return a 'GHC.Tc.Types.TcPluginSolveResult' +-- indicating which Wanted constraints it could solve, or whether any are +-- insoluble. +type TcPluginSolver + = [GHC.Ct] -- ^ Givens + -> [GHC.Ct] -- ^ Wanteds + -> TcPluginM Solve TcPluginSolveResult + +-- | For rewriting type family applications, a type-checking plugin provides +-- a function of this type for each type family 'GHC.Core.TyCon.TyCon'. +-- +-- The function is provided with the current set of Given constraints, together +-- with the arguments to the type family. +-- The type family application will always be fully saturated. +type TcPluginRewriter + = [GHC.Ct] -- ^ Givens + -> [GHC.Type] -- ^ Type family arguments (saturated) + -> TcPluginM Rewrite TcPluginRewriteResult + +-- | A record containing all the stages necessary for the +-- operation of a type-checking plugin, as defined in this API. +-- +-- __Note__: this is not the same record as GHC's built-in +-- 'GHC.Tc.Types.TcPlugin' record. Use 'mkTcPlugin' for the conversion. +-- +-- To create a type-checking plugin, define something of this type +-- and then call 'mkTcPlugin' on the result. +-- This will return something that can be passed to 'GHC.Plugins.Plugin': +-- +-- > plugin :: GHC.Plugins.Plugin +-- > plugin = +-- > GHC.Plugins.defaultPlugin +-- > { GHC.Plugins.tcPlugin = +-- > \ args -> Just $ +-- > GHC.TcPlugin.API.mkTcPlugin ( myTcPlugin args ) +-- > } +-- > +-- > myTcPlugin :: [String] -> GHC.TcPlugin.API.TcPlugin +-- > myTcPlugin args = ... +data TcPlugin = forall s. TcPlugin + { tcPluginInit :: TcPluginM Init s + -- ^ Initialise plugin, when entering type-checker. + + , tcPluginSolve :: s -> TcPluginSolver + -- ^ Solve some constraints. + -- + -- This function will be invoked at two points in the constraint solving + -- process: once to manipulate given constraints, and once to solve + -- wanted constraints. In the first case (and only in the first case), + -- no wanted constraints will be passed to the plugin. + -- + -- The plugin can either return a contradiction, + -- or specify that it has solved some constraints (with evidence), + -- and possibly emit additional wanted constraints. + -- + -- Use @ \\ _ _ _ -> pure $ TcPluginOK [] [] @ if your plugin + -- does not provide this functionality. + + , tcPluginRewrite :: s -> GHC.UniqFM GHC.TyCon TcPluginRewriter + -- ^ Rewrite saturated type family applications. + -- + -- The plugin is expected to supply a mapping from type family names to + -- rewriting functions. For each type family 'GHC.Core.TyCon.TyCon', + -- the plugin should provide a function which takes in the given constraints + -- and arguments of a saturated type family application, and return + -- a possible rewriting. + -- See 'TcPluginRewriter' for the expected shape of such a function. + -- + -- Use @ const emptyUFM @ if your plugin does not provide this functionality. + + , tcPluginStop :: s -> TcPluginM Stop () + -- ^ Clean up after the plugin, when exiting the type-checker. + } + +-- | The monad used for a type-checker plugin, parametrised by +-- the 'TcPluginStage' of the plugin. +type TcPluginM :: TcPluginStage -> ( Type -> Type ) +data family TcPluginM s +newtype instance TcPluginM Init a = + TcPluginInitM { tcPluginInitM :: GHC.TcPluginM a } + deriving newtype ( Functor, Applicative, Monad ) +#ifdef HAS_DERIVEDS +newtype instance TcPluginM Solve a = + TcPluginSolveM { tcPluginSolveM :: BuiltinDefs -> GHC.EvBindsVar -> [GHC.Ct] -> GHC.TcPluginM a } + deriving ( Functor, Applicative, Monad ) + via ( ReaderT BuiltinDefs ( ReaderT GHC.EvBindsVar ( ReaderT [GHC.Ct] GHC.TcPluginM ) ) ) +#else +newtype instance TcPluginM Solve a = + TcPluginSolveM { tcPluginSolveM :: BuiltinDefs -> GHC.EvBindsVar -> GHC.TcPluginM a } + deriving ( Functor, Applicative, Monad ) + via ( ReaderT BuiltinDefs ( ReaderT GHC.EvBindsVar GHC.TcPluginM ) ) +#endif +newtype instance TcPluginM Rewrite a = + TcPluginRewriteM { tcPluginRewriteM :: BuiltinDefs -> RewriteEnv -> GHC.TcPluginM a } + deriving ( Functor, Applicative, Monad ) + via ( ReaderT BuiltinDefs ( ReaderT RewriteEnv GHC.TcPluginM ) ) +newtype instance TcPluginM Stop a = + TcPluginStopM { tcPluginStopM :: GHC.TcPluginM a } + deriving newtype ( Functor, Applicative, Monad ) + +-- | Ask for the evidence currently gathered by the type-checker. +-- +-- Only available in the solver part of the type-checking plugin. +askEvBinds :: TcPluginM Solve GHC.EvBindsVar +askEvBinds = TcPluginSolveM + \ _defs + evBinds +#ifdef HAS_DERIVEDS + _deriveds +#endif + -> pure evBinds + +-- | Ask for the Derived constraints that the solver was provided with. +-- +-- Always returns the empty list on GHC 9.4 or above. +askDeriveds :: TcPluginM Solve [GHC.Ct] +askDeriveds = +#ifdef HAS_DERIVEDS + TcPluginSolveM \ _defs _evBinds deriveds -> pure deriveds +#else + pure [] +#endif + +-- | Ask for the current rewriting environment. +-- +-- Only available in the rewriter part of the type-checking plugin. +askRewriteEnv :: TcPluginM Rewrite RewriteEnv +askRewriteEnv = TcPluginRewriteM ( \ _ rewriteEnv -> pure rewriteEnv ) + +-- | A 'MonadTcPlugin' is essentially a reader monad over GHC's 'GHC.Tc.TcM' monad. +-- +-- This means we have both a @lift@ and an @unlift@ operation, +-- similar to @MonadUnliftIO@ or @MonadBaseControl@. +-- +-- See for instance 'unsafeLiftThroughTcM', which is an example of function that +-- one would not be able to write using only a @lift@ operation. +-- +-- Note that you must import the internal module in order to access the methods. +-- Please report a bug if you find yourself needing this functionality. +type MonadTcPlugin :: ( Type -> Type ) -> Constraint +class Monad m => MonadTcPlugin m where + + {-# MINIMAL liftTcPluginM, unsafeWithRunInTcM #-} + + -- N.B.: these methods are not re-exported from the main module. + + -- | Lift a computation from GHC's 'GHC.TcPluginM' monad. + liftTcPluginM :: GHC.TcPluginM a -> m a + + -- | Lift a computation from the 'GHC.Tc.TcM' monad. + unsafeLiftTcM :: GHC.TcM a -> m a + unsafeLiftTcM = liftTcPluginM . GHC.unsafeTcPluginTcM + + -- | Unlift a computation from the 'GHC.Tc.TcM' monad. + -- + -- If this type signature seems confusing, I recommend reading Alexis King's + -- excellent blog post on @MonadBaseControl@: + -- + -- <https://lexi-lambda.github.io/blog/2019/09/07/demystifying-monadbasecontrol/ Demystifying MonadBaseControl> + unsafeWithRunInTcM :: ( ( forall a. m a -> GHC.TcM a ) -> GHC.TcM b ) -> m b + +instance MonadTcPlugin ( TcPluginM Init ) where + liftTcPluginM = TcPluginInitM + unsafeWithRunInTcM runInTcM + = unsafeLiftTcM $ runInTcM +#ifdef HAS_REWRITING + ( GHC.runTcPluginM . tcPluginInitM ) +#else + ( ( `GHC.runTcPluginM` ( error "tcPluginInit: cannot access EvBindsVar" ) ) . tcPluginInitM ) +#endif +instance MonadTcPlugin ( TcPluginM Solve ) where + liftTcPluginM = TcPluginSolveM +#ifdef HAS_DERIVEDS + . ( \ ma _defs _evBinds _deriveds -> ma ) +#else + . ( \ ma _defs _evBinds -> ma ) +#endif + unsafeWithRunInTcM runInTcM + = TcPluginSolveM + \ builtinDefs + evBinds +#ifdef HAS_DERIVEDS + deriveds +#endif + -> + GHC.unsafeTcPluginTcM $ runInTcM +#ifdef HAS_REWRITING + ( GHC.runTcPluginM +#ifdef HAS_DERIVEDS + . ( \ f -> f builtinDefs evBinds deriveds ) +#else + . ( \ f -> f builtinDefs evBinds ) +#endif + . tcPluginSolveM ) +#else + ( ( `GHC.runTcPluginM` evBinds ) + . ( \ f -> f builtinDefs evBinds deriveds ) + . tcPluginSolveM + ) +#endif +instance MonadTcPlugin ( TcPluginM Rewrite ) where + liftTcPluginM = TcPluginRewriteM . ( \ ma _ _ -> ma ) + unsafeWithRunInTcM runInTcM + = TcPluginRewriteM \ builtinDefs rewriteEnv -> + GHC.unsafeTcPluginTcM $ runInTcM +#ifdef HAS_REWRITING + ( GHC.runTcPluginM +#else + ( ( `GHC.runTcPluginM` ( error "tcPluginRewrite: cannot access EvBindsVar" ) ) +#endif + . ( \ f -> f builtinDefs rewriteEnv ) + . tcPluginRewriteM ) +instance MonadTcPlugin ( TcPluginM Stop ) where + liftTcPluginM = TcPluginStopM + unsafeWithRunInTcM runInTcM + = unsafeLiftTcM $ runInTcM +#ifdef HAS_REWRITING + ( GHC.runTcPluginM . tcPluginStopM ) +#else + ( ( `GHC.runTcPluginM` ( error "tcPluginStop: cannot access EvBindsVar" ) ) . tcPluginStopM ) +#endif + +-- | Take a function whose argument and result types are both within the 'GHC.Tc.TcM' monad, +-- and return a function that works within a type-checking plugin monad. +-- +-- Please report a bug if you find yourself needing to use this function. +unsafeLiftThroughTcM :: MonadTcPlugin m => ( GHC.TcM a -> GHC.TcM b ) -> m a -> m b +unsafeLiftThroughTcM f ma = unsafeWithRunInTcM \ runInTcM -> f ( runInTcM ma ) + +-- | Use this function to create a type-checker plugin to pass to GHC. +mkTcPlugin + :: TcPlugin -- ^ type-checking plugin written with this library + -> GHC.TcPlugin -- ^ type-checking plugin for GHC +mkTcPlugin ( TcPlugin + { tcPluginInit = tcPluginInit :: TcPluginM Init userDefs + , tcPluginSolve + , tcPluginRewrite + , tcPluginStop + } + ) = + GHC.TcPlugin + { GHC.tcPluginInit = adaptUserInit tcPluginInit +#ifdef HAS_REWRITING + , GHC.tcPluginSolve = adaptUserSolve tcPluginSolve + , GHC.tcPluginRewrite = adaptUserRewrite tcPluginRewrite +#else + , GHC.tcPluginSolve = adaptUserSolveAndRewrite + tcPluginSolve tcPluginRewrite +#endif + , GHC.tcPluginStop = adaptUserStop tcPluginStop + } + where + adaptUserInit :: TcPluginM Init userDefs -> GHC.TcPluginM ( TcPluginDefs userDefs ) + adaptUserInit userInit = do + tcPluginBuiltinDefs <- initBuiltinDefs + tcPluginUserDefs <- tcPluginInitM userInit + pure ( TcPluginDefs { tcPluginBuiltinDefs, tcPluginUserDefs }) + +#ifdef HAS_REWRITING + adaptUserSolve :: ( userDefs -> TcPluginSolver ) + -> TcPluginDefs userDefs + -> GHC.EvBindsVar + -> GHC.TcPluginSolver + adaptUserSolve userSolve ( TcPluginDefs { tcPluginUserDefs, tcPluginBuiltinDefs } ) + evBindsVar +#ifdef HAS_DERIVEDS + = \ givens deriveds wanteds -> do + tcPluginSolveM ( userSolve tcPluginUserDefs givens wanteds ) + tcPluginBuiltinDefs evBindsVar deriveds +#else + = \ givens _deriveds wanteds -> do + tcPluginSolveM ( userSolve tcPluginUserDefs givens wanteds ) + tcPluginBuiltinDefs evBindsVar +#endif + + adaptUserRewrite :: ( userDefs -> GHC.UniqFM GHC.TyCon TcPluginRewriter ) + -> TcPluginDefs userDefs -> GHC.UniqFM GHC.TyCon GHC.TcPluginRewriter + adaptUserRewrite userRewrite ( TcPluginDefs { tcPluginUserDefs, tcPluginBuiltinDefs }) + = fmap + ( \ userRewriter rewriteEnv givens tys -> + tcPluginRewriteM ( userRewriter givens tys ) tcPluginBuiltinDefs rewriteEnv + ) + ( userRewrite tcPluginUserDefs ) +#else + adaptUserSolveAndRewrite + :: ( userDefs -> TcPluginSolver ) + -> ( userDefs -> GHC.UniqFM GHC.TyCon TcPluginRewriter ) + -> TcPluginDefs userDefs + -> GHC.TcPluginSolver + adaptUserSolveAndRewrite userSolve userRewrite ( TcPluginDefs { tcPluginUserDefs, tcPluginBuiltinDefs } ) + = \ givens deriveds wanteds -> do + evBindsVar <- GHC.getEvBindsTcPluginM + shimRewriter + givens deriveds wanteds + ( rewrittenTyFamsIORef tcPluginBuiltinDefs ) + ( fmap + ( \ userRewriter rewriteEnv gs tys -> + tcPluginRewriteM ( userRewriter gs tys ) + tcPluginBuiltinDefs rewriteEnv + ) + ( userRewrite tcPluginUserDefs ) + ) + ( \ gs ds ws -> + tcPluginSolveM ( userSolve tcPluginUserDefs gs ws ) + tcPluginBuiltinDefs evBindsVar ds + ) +#endif + + adaptUserStop :: ( userDefs -> TcPluginM Stop () ) -> TcPluginDefs userDefs -> GHC.TcPluginM () + adaptUserStop userStop ( TcPluginDefs { tcPluginUserDefs } ) = + tcPluginStopM $ userStop tcPluginUserDefs + +-- | Monads for type-checking plugins which are able to emit new constraints +-- and throw errors. +-- +-- These operations are supported by the monads that 'tcPluginSolve' +-- and 'tcPluginRewrite' use; it is not possible to emit work or +-- throw type errors in 'tcPluginInit' or 'tcPluginStop'. +-- +-- See 'mkTcPluginErrorTy' and 'GHC.TcPlugin.API.emitWork' for functions +-- which require this typeclass. +type MonadTcPluginWork :: ( Type -> Type ) -> Constraint +class MonadTcPlugin m => MonadTcPluginWork m where + {-# MINIMAL #-} -- to avoid the methods appearing in the haddocks + askBuiltins :: m BuiltinDefs + askBuiltins = error "askBuiltins: no default implementation" +instance MonadTcPluginWork ( TcPluginM Solve ) where + askBuiltins = TcPluginSolveM + \ builtinDefs + _evBinds +#ifdef HAS_DERIVEDS + _deriveds +#endif + -> pure builtinDefs +instance MonadTcPluginWork ( TcPluginM Rewrite ) where + askBuiltins = TcPluginRewriteM \ builtinDefs _evBinds -> pure builtinDefs + +instance TypeError ( 'Text "Cannot emit new work in 'tcPluginInit'." ) + => MonadTcPluginWork ( TcPluginM Init ) where + askBuiltins = error "Cannot emit new work in 'tcPluginInit'." +instance TypeError ( 'Text "Cannot emit new work in 'tcPluginStop'." ) + => MonadTcPluginWork ( TcPluginM Stop ) where + askBuiltins = error "Cannot emit new work in 'tcPluginStop'." + +-- | Use this type like 'GHC.TypeLits.ErrorMessage' to write an error message. +-- This error message can then be thrown at the type-level by the plugin, +-- by emitting a wanted constraint whose predicate is obtained from 'mkTcPluginErrorTy'. +-- +-- A 'GHC.Tc.Types.Constraint.CtLoc' will still need to be provided in order to inform GHC of the +-- origin of the error (e.g.: which part of the source code should be +-- highlighted?). See 'GHC.TcPlugin.API.setCtLocM'. +data TcPluginErrorMessage + = Txt !String + -- ^ Show the text as is. + | PrintType !GHC.Type + -- ^ Pretty print the given type. + | (:|:) !TcPluginErrorMessage !TcPluginErrorMessage + -- ^ Put two messages side by side. + | (:-:) !TcPluginErrorMessage !TcPluginErrorMessage + -- ^ Stack two messages vertically. +infixl 5 :|: +infixl 6 :-: + +-- | Create an error type with the desired error message. +-- +-- The result can be paired with a 'GHC.Tc.Types.Constraint.CtLoc' in order to throw a type error, +-- for instance by using 'GHC.TcPlugin.API.newWanted'. +mkTcPluginErrorTy :: MonadTcPluginWork m => TcPluginErrorMessage -> m GHC.PredType +mkTcPluginErrorTy msg = do + builtinDefs@( BuiltinDefs { typeErrorTyCon } ) <- askBuiltins + let + errorMsgTy :: GHC.PredType + errorMsgTy = interpretErrorMessage builtinDefs msg + pure $ GHC.mkTyConApp typeErrorTyCon [ GHC.constraintKind, errorMsgTy ] + +-------------------------------------------------------------------------------- +-- Private types and functions. +-- Not exposed at all, even from the internal module. + +data BuiltinDefs = + BuiltinDefs + { typeErrorTyCon :: !GHC.TyCon + , textTyCon :: !GHC.TyCon + , showTypeTyCon :: !GHC.TyCon + , concatTyCon :: !GHC.TyCon + , vcatTyCon :: !GHC.TyCon +#ifndef HAS_REWRITING + , rewrittenTyFamsIORef :: !( IORef RewrittenTyFamApps ) +#endif + } + +data TcPluginDefs s + = TcPluginDefs + { tcPluginBuiltinDefs :: !BuiltinDefs + , tcPluginUserDefs :: !s + } + +initBuiltinDefs :: GHC.TcPluginM BuiltinDefs +initBuiltinDefs = do + typeErrorTyCon <- GHC.tcLookupTyCon GHC.TypeLits.errorMessageTypeErrorFamName + textTyCon <- GHC.promoteDataCon <$> GHC.tcLookupDataCon GHC.TypeLits.typeErrorTextDataConName + showTypeTyCon <- GHC.promoteDataCon <$> GHC.tcLookupDataCon GHC.TypeLits.typeErrorShowTypeDataConName + concatTyCon <- GHC.promoteDataCon <$> GHC.tcLookupDataCon GHC.TypeLits.typeErrorAppendDataConName + vcatTyCon <- GHC.promoteDataCon <$> GHC.tcLookupDataCon GHC.TypeLits.typeErrorVAppendDataConName +#ifndef HAS_REWRITING + rewrittenTyFamsIORef <- GHC.tcPluginIO $ newIORef GHC.emptyUDFM +#endif + pure ( BuiltinDefs { .. } ) + +interpretErrorMessage :: BuiltinDefs -> TcPluginErrorMessage -> GHC.PredType +interpretErrorMessage ( BuiltinDefs { .. } ) = go + where + go :: TcPluginErrorMessage -> GHC.PredType + go ( Txt str ) = + GHC.mkTyConApp textTyCon [ GHC.LitTy . GHC.StrTyLit . GHC.fsLit $ str ] + go ( PrintType ty ) = + GHC.mkTyConApp showTypeTyCon [ GHC.tcTypeKind ty, ty ] + -- The kind gets ignored by GHC when printing the error message (see GHC.Core.Type.pprUserTypeErrorTy). + -- However, including the wrong kind can lead to ASSERT failures, so we compute the kind and pass it. + go ( msg1 :|: msg2 ) = + GHC.mkTyConApp concatTyCon [ go msg1, go msg2 ] + go ( msg1 :-: msg2 ) = + GHC.mkTyConApp vcatTyCon [ go msg1, go msg2 ]
+ src/GHC/TcPlugin/API/Internal/Shim.hs view
@@ -0,0 +1,891 @@+{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE DerivingVia #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE ViewPatterns #-} + +{-| +Module: GHC.TcPlugin.API.Internal.Shim + +This module defines a compatibility shim which allows +the library to support a limited form of type-family rewriting +in typechecking plugins on GHC 9.0 and 9.2. +-} + +module GHC.TcPlugin.API.Internal.Shim where + +-- base +import Control.Monad + ( forM, when ) +#if !MIN_VERSION_ghc(9,2,0) +import Data.Foldable + ( foldlM ) +#endif +import Data.IORef + ( IORef, readIORef, writeIORef ) +#if MIN_VERSION_ghc(9,2,0) +import Data.List.NonEmpty + ( NonEmpty((:|)) ) +#endif +import Data.Maybe + ( fromMaybe ) + +-- transformers +import Control.Monad.Trans.Reader + ( ReaderT(..) ) +import Control.Monad.Trans.State.Strict + ( StateT(..) ) + +-- ghc +import GHC.Core.Coercion + ( castCoercionKind1 + , mkReflCo, mkSymCo, mkFunCo, mkHomoForAllCos + , mkTransCo, mkAppCos, mkNomReflCo, mkSubCo + , mkTyConAppCo, tyConRolesX + , tyConRolesRepresentational + , simplifyArgsWorker +#if !MIN_VERSION_ghc(9,2,0) + , coToMCo +#endif + ) +#if MIN_VERSION_ghc(9,2,0) +import GHC.Core.Map.Type + ( LooseTypeMap ) +#else +import GHC.Core.Map + ( LooseTypeMap ) +#endif +import GHC.Core.Predicate + ( EqRel(..), eqRelRole ) +import GHC.Core.TyCo.Rep + ( Type(..), Kind, Coercion(..) + , TyCoBinder(..) + , MCoercion(..), MCoercionN + , binderVars, mkForAllTys + , isNamedBinder + , mkTyVarTy + ) +import GHC.Core.TyCon + ( TyCon(..), TyConBinder, TyConBndrVis(..) +#if MIN_VERSION_ghc(9,2,0) + , isForgetfulSynTyCon +#endif + , isFamFreeTyCon, isTypeSynonymTyCon + , isTypeFamilyTyCon + , tyConBinders, tyConResKind + , tyConArity + ) +import GHC.Core.Type + ( TyVar + , tcView + , mkCoercionTy, mkCastTy, mkAppTys + , mkTyConApp, mkScaled, coreView + , tymult, tyVarKind + ) +#if MIN_VERSION_ghc(9,2,0) +import GHC.Data.Maybe + ( firstJustsM ) +#endif +import GHC.Data.TrieMap + ( ListMap ) +import GHC.Tc.Plugin + ( tcPluginIO, newWanted, newDerived ) +import GHC.Tc.Solver.Monad + ( TcS + , zonkCo, zonkTcType + , isFilledMetaTyVar_maybe + , getInertEqs + , checkReductionDepth + , matchFam, findFunEq, insertFunEq + , runTcPluginTcS, runTcSWithEvBinds + , traceTcS +#if MIN_VERSION_ghc(9,2,0) + , lookupFamAppCache, lookupFamAppInert, extendFamAppCache + , pattern EqualCtList +#else + , lookupFlatCache, extendFlatCache +#endif + ) +import GHC.Tc.Types + ( TcPluginM, TcPluginResult(..) + , unsafeTcPluginTcM, getEvBindsTcPluginM + ) +import GHC.Tc.Types.Constraint + ( Ct(..) + , CtLoc, CtFlavour(..), CtFlavourRole, ShadowInfo(..) + , Xi +#if MIN_VERSION_ghc(9,2,0) + , CanEqLHS(..) +#endif + , ctLoc, ctFlavour, ctEvidence, ctEqRel, ctEvPred + , ctEvExpr, ctEvCoercion, ctEvFlavour + , bumpCtLocDepth, eqCanRewriteFR, mkNonCanonical + ) +import GHC.Tc.Types.Evidence + ( EvTerm(..), Role(..) + , evCast + , mkTcReflCo, mkTcTransCo, mkTcSymCo + , mkTcTyConAppCo + , tcDowngradeRole + ) +import GHC.Tc.Utils.TcType + ( TcTyCoVarSet +#if MIN_VERSION_ghc(9,2,0) + , tcSplitForAllTyVarBinders +#else + , tcSplitForAllVarBndrs +#endif + , tcSplitTyConApp_maybe + , tcTypeKind + , tyCoVarsOfType + ) +#if !MIN_VERSION_ghc(9,2,0) +import GHC.Types.Unique + ( Unique ) +#endif +import GHC.Types.Unique.DFM + ( UniqDFM ) +import GHC.Types.Unique.FM + ( UniqFM, lookupUFM, isNullUFM ) +import GHC.Types.Var + ( TcTyVar, VarBndr(..) +#if !MIN_VERSION_ghc(9,2,0) + , TyVarBinder +#endif + , updateTyVarKindM + ) +import GHC.Types.Var.Env + ( lookupDVarEnv ) +import GHC.Types.Var.Set + ( emptyVarSet ) +import GHC.Utils.Misc + ( dropList ) +import GHC.Utils.Monad + ( zipWith3M ) +import GHC.Utils.Outputable + ( Outputable(ppr), SDoc + , empty, text, ($$) + ) + +-------------------------------------------------------------------------------- + +-- | A reduction to the provided type, with a coercion witnessing the equality. +data Reduction = Reduction !Type Coercion +instance Outputable Reduction where + ppr (Reduction ty co) = text "Reduction" $$ ppr ty $$ ppr co + +data RewriteEnv + = FE { fe_loc :: !CtLoc + , fe_flavour :: !CtFlavour + , fe_eq_rel :: !EqRel + } + +mkReduction :: ( Coercion, Type ) -> Reduction +mkReduction ( co, ty ) = Reduction ty co + +runReduction1 :: Reduction -> ( Type, Coercion ) +runReduction1 ( Reduction ty co ) = ( ty, co ) + +runReduction2 :: Reduction -> ( Coercion, Type ) +runReduction2 ( Reduction ty co ) = ( co, ty ) + +type TcPluginSolveResult = TcPluginResult + +data TcPluginRewriteResult + = + -- | The plugin does not rewrite the type family application. + -- + -- The plugin can also emit additional wanted constraints, + -- including insoluble ones (e.g. a type error message). + TcPluginNoRewrite { tcRewriterWanteds :: [Ct] } + + -- | The plugin rewrites the type family application + -- providing a rewriting together with evidence. + -- + -- The plugin can also emit additional wanted constraints. + | TcPluginRewriteTo + { tcPluginReduction :: !Reduction + , tcRewriterWanteds :: [Ct] + } + +type Rewriter = RewriteEnv -> [Ct] -> [Type] -> TcPluginM TcPluginRewriteResult + +type Rewriters = UniqFM TyCon Rewriter + +shimRewriter :: [Ct] -> [Ct] -> [Ct] + -> IORef RewrittenTyFamApps + -> Rewriters + -> ( [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginSolveResult ) + -> TcPluginM TcPluginSolveResult +shimRewriter givens deriveds wanteds cacheRef rws solver + | isNullUFM rws + = solver givens deriveds wanteds + | otherwise + = do + res <- solver givens deriveds wanteds + case res of + contra@( TcPluginContradiction {} ) -> + pure contra + TcPluginOk solved new -> do + ( rewrittenDeriveds, solvedDeriveds, newCts1 ) <- traverseCts ( reduceCt cacheRef rws givens ) deriveds + ( rewrittenWanteds , solvedWanteds , newCts2 ) <- traverseCts ( reduceCt cacheRef rws givens ) wanteds + pure $ + TcPluginOk + ( solved ++ solvedDeriveds ++ solvedWanteds ) + ( new ++ newCts1 ++ rewrittenDeriveds ++ newCts2 ++ rewrittenWanteds ) + +reduceCt :: IORef RewrittenTyFamApps + -> Rewriters + -> [Ct] + -> Ct + -> TcPluginM ( Maybe ( Ct, (EvTerm, Ct) ), [Ct] ) +reduceCt cacheRef rws givens ct = do + let + predTy :: Type + predTy = ctEvPred ( ctEvidence ct ) + rwEnv :: RewriteEnv + rwEnv = FE ( ctLoc ct ) ( ctFlavour ct ) ( ctEqRel ct ) + shimRewriteEnv :: ShimRewriteEnv + shimRewriteEnv = ShimRewriteEnv rws rwEnv ct givens cacheRef + ( res, newCts ) <- runRewritePluginM shimRewriteEnv ( rewrite_one predTy ) + case res of + Nothing -> pure ( Nothing, newCts ) + Just ( Reduction predTy' co ) -> do + ctEv' <- case ctFlavour ct of + Given -> error "ghc-tcplugin-api: unexpected Given in reduceCt" + Wanted {} -> newWanted ( ctLoc ct ) predTy' + Derived -> newDerived ( ctLoc ct ) predTy' + pure ( Just + ( mkNonCanonical ctEv' + , ( evCast ( ctEvExpr ctEv' ) co, ct ) + ) + , newCts + ) + +traverseCts :: Monad m + => ( a -> m ( Maybe (b, c), [d] ) ) + -> [a] + -> m ( [b], [c], [d] ) +traverseCts _ [] = pure ( [], [], [] ) +traverseCts f (a : as) = do + ( mb_bc, ds ) <- f a + ( bs, cs, dss ) <- traverseCts f as + case mb_bc of + Nothing -> pure ( bs, cs, ds ++ dss ) + Just (b,c) -> pure ( b : bs, c : cs, ds ++ dss ) + +-------------------------------------------------------------------------------- +-- The following is (mostly) copied from GHC 9.4's GHC.Tc.Solver.Rewrite module. + +rewrite_one :: Type -> RewriteM Reduction +rewrite_one = \case + ( rewriterView -> Just ty' ) + -> rewrite_one ty' + ty@( LitTy {} ) + -> do + role <- getRole + pure $ Reduction ty ( mkReflCo role ty ) + TyVarTy tv + -> rewriteTyVar tv + AppTy ty1 ty2 + -> rewrite_app_tys ty1 [ty2] + TyConApp tc tys + | isTypeFamilyTyCon tc + -> rewrite_fam_app tc tys + | otherwise + -> rewrite_ty_con_app tc tys + ty@( FunTy { ft_mult = mult, ft_arg = ty1, ft_res = ty2 } ) + -> do + Reduction xi1 co1 <- rewrite_one ty1 + Reduction xi2 co2 <- rewrite_one ty2 + Reduction xi3 co3 <- setEqRel NomEq $ rewrite_one mult + role <- getRole + return $ + Reduction + ( ty { ft_mult = xi3, ft_arg = xi1, ft_res = xi2 } ) + ( mkFunCo role co3 co1 co2 ) + ty@( ForAllTy {} ) + -> do + let + (bndrs, rho) = tcSplitForAllTyVarBinders ty + tvs = binderVars bndrs + Reduction rho' co <- rewrite_one rho + pure $ Reduction + ( mkForAllTys bndrs rho' ) + ( mkHomoForAllCos tvs co ) + CastTy ty g + -> do + Reduction xi co <- rewrite_one ty + (g', _) <- rewrite_co g + role <- getRole + pure $ Reduction + ( mkCastTy xi g' ) + ( castCoercionKind1 co role xi ty g' ) + CoercionTy co + -> do + ( co1, co2 ) <- rewrite_co co + pure $ Reduction ( mkCoercionTy co1 ) co2 + +rewrite_app_tys :: Type -> [Type] -> RewriteM Reduction +rewrite_app_tys ( AppTy ty1 ty2 ) tys = + rewrite_app_tys ty1 ( ty2 : tys ) +rewrite_app_tys fun_ty arg_tys = do + Reduction fun_xi fun_co <- rewrite_one fun_ty + rewrite_app_ty_args fun_xi fun_co arg_tys + +rewrite_app_ty_args :: Xi -> Coercion -> [Type] -> RewriteM Reduction +rewrite_app_ty_args fun_xi fun_co [] = pure $ Reduction fun_xi fun_co +rewrite_app_ty_args fun_xi fun_co arg_tys = do + (xi, co, kind_co) <- case tcSplitTyConApp_maybe fun_xi of + Just (tc, xis) -> do + let tc_roles = tyConRolesRepresentational tc + arg_roles = dropList xis tc_roles + (arg_xis, arg_cos, kind_co) + <- rewrite_vector (tcTypeKind fun_xi) arg_roles arg_tys + eq_rel <- getEqRel + let app_xi = mkTyConApp tc (xis ++ arg_xis) + app_co = case eq_rel of + NomEq -> mkAppCos fun_co arg_cos + ReprEq -> mkTcTyConAppCo Representational tc + (zipWith mkReflCo tc_roles xis ++ arg_cos) + `mkTcTransCo` + mkAppCos fun_co (map mkNomReflCo arg_tys) + return (app_xi, app_co, kind_co) + Nothing -> do + (arg_xis, arg_cos, kind_co) + <- rewrite_vector (tcTypeKind fun_xi) (repeat Nominal) arg_tys + let arg_xi = mkAppTys fun_xi arg_xis + arg_co = mkAppCos fun_co arg_cos + return (arg_xi, arg_co, kind_co) + role <- getRole + return (homogenise_result xi co role kind_co) + +{-# INLINE rewrite_args_tc #-} +rewrite_args_tc :: TyCon -> Maybe [Role] -> [Type] -> RewriteM ( [Xi], [Coercion] , MCoercionN) +rewrite_args_tc tc = rewrite_args all_bndrs any_named_bndrs inner_ki emptyVarSet + where + (bndrs, named) + = ty_con_binders_ty_binders' (tyConBinders tc) + (inner_bndrs, inner_ki, inner_named) = split_pi_tys' (tyConResKind tc) + !all_bndrs = bndrs `chkAppend` inner_bndrs + !any_named_bndrs = named || inner_named + +rewrite_fam_app :: TyCon -> [Type] -> RewriteM Reduction +rewrite_fam_app tc tys = do + let (tys1, tys_rest) = splitAt (tyConArity tc) tys + Reduction xi1 co1 <- rewrite_exact_fam_app tc tys1 + rewrite_app_ty_args xi1 co1 tys_rest + +rewrite_exact_fam_app :: TyCon -> [Type] -> RewriteM Reduction +rewrite_exact_fam_app tc tys = do + checkStackDepth (mkTyConApp tc tys) + rws <- getRewriters + let + mbRewriter :: Maybe Rewriter + mbRewriter = lookupUFM rws tc + result1 <- try_to_reduce tc tys mbRewriter + case result1 of + Just redn -> finish False redn + _ -> do + eq_rel <- getEqRel + (xis, coercions, kind_co) <- + if eq_rel == NomEq + then rewrite_args_tc tc Nothing tys + else setEqRel NomEq $ + rewrite_args_tc tc Nothing tys + let role = eqRelRole eq_rel + args_co = mkTyConAppCo role tc coercions + homogenise :: Reduction -> Reduction + homogenise (Reduction xi co) = + homogenise_result xi (co `mkTcTransCo` args_co) role kind_co + giveUp :: Reduction + giveUp = homogenise $ Reduction reduced (mkTcReflCo role reduced) + where reduced = mkTyConApp tc xis + result2 <- liftTcS $ lookupFamAppInert tc xis + flavour <- getFlavour + case result2 of + Just (co, xi, fr@(_, inert_eq_rel)) + | fr `eqCanRewriteFR` (flavour, eq_rel) + -> finish True (homogenise $ Reduction xi downgraded_co) + where + inert_role = eqRelRole inert_eq_rel + role' = eqRelRole eq_rel + downgraded_co = tcDowngradeRole role' inert_role (mkTcSymCo co) + _ -> do + result3 <- try_to_reduce tc xis mbRewriter + case result3 of + Just redn -> finish True (homogenise redn) + _ -> return giveUp + where + finish :: Bool -> Reduction -> RewriteM Reduction + finish use_cache (Reduction xi co) = do + Reduction fully fully_co <- bumpDepth $ rewrite_one xi + let final_redn = Reduction fully (fully_co `mkTcTransCo` co) + eq_rel <- getEqRel + flavour <- getFlavour + when (use_cache && eq_rel == NomEq && flavour /= Derived) $ + liftTcS $ + extendFamAppCache tc tys + ( runReduction2 final_redn ) +#if !MIN_VERSION_ghc(9,2,0) + flavour +#endif + return final_redn + {-# INLINE finish #-} + +-- Returned coercion is output ~r input, where r is the role in the RewriteM monad +-- See Note [How to normalise a family application] +try_to_reduce :: TyCon -> [Type] -> Maybe Rewriter + -> RewriteM (Maybe Reduction) +try_to_reduce tc tys mb_rewriter = do + result <- + firstJustsM + [ runTcPluginRewriter mb_rewriter tc tys + , liftTcS $ mkRed <$> lookupFamAppCache tc tys + , liftTcS $ mkRed <$> matchFam tc tys ] + forM result downgrade + where + mkRed :: Maybe (Coercion, Type) -> Maybe Reduction + mkRed = fmap $ uncurry ( flip Reduction ) + downgrade :: Reduction -> RewriteM Reduction + downgrade redn@(Reduction xi co) = do + eq_rel <- getEqRel + case eq_rel of + NomEq -> return redn + ReprEq -> return $ Reduction xi (mkSubCo co) + +runTcPluginRewriter :: Maybe Rewriter + -> TyCon -> [Type] + -> RewriteM (Maybe Reduction) +runTcPluginRewriter mbRewriter tc tys = + case mbRewriter of + Nothing -> return Nothing + Just rewriter -> do + traceRewriteM "runTcPluginRewriter { " empty + res <- runRewriter rewriter + traceRewriteM "runTcPluginRewriter }" ( ppr res ) + pure res + where + runRewriter :: Rewriter -> RewriteM (Maybe Reduction) + runRewriter rewriter = do + rewriteResult <- RewriteM \ env s -> do + res <- runTcPluginTcS ( rewriter ( rewriteEnv env ) ( rewriteGivens env ) tys ) + pure ( res, s ) + case rewriteResult of + TcPluginRewriteTo + { tcPluginReduction = redn + , tcRewriterWanteds = wanteds + } -> + addRewriting tc tys ( Just redn ) wanteds + TcPluginNoRewrite { tcRewriterWanteds = wanteds } -> do + addRewriting tc tys Nothing wanteds + +rewrite_ty_con_app :: TyCon -> [Type] -> RewriteM Reduction +rewrite_ty_con_app tc tys = do + role <- getRole + let m_roles | Nominal <- role = Nothing + | otherwise = Just $ tyConRolesX role tc + (xis, coercions, kind_co) <- rewrite_args_tc tc m_roles tys + let tyconapp_xi = mkTyConApp tc xis + tyconapp_co = mkTyConAppCo role tc coercions + return (homogenise_result tyconapp_xi tyconapp_co role kind_co) + +rewrite_co :: Coercion -> RewriteM ( Coercion, Coercion ) +rewrite_co co = do + zonked_co <- liftTcS $ zonkCo co + env_role <- getRole + let co' = mkTcReflCo env_role ( mkCoercionTy zonked_co ) + pure ( zonked_co, co' ) + +rewriterView :: Type -> Maybe Type +rewriterView ty@(TyConApp tc _) + | ( isTypeSynonymTyCon tc && not (isFamFreeTyCon tc) ) +#if MIN_VERSION_ghc(9,2,0) + || isForgetfulSynTyCon tc +#endif + = tcView ty +rewriterView _other = Nothing + +rewriteTyVar :: TyVar -> RewriteM Reduction +rewriteTyVar tv = do + mb_yes <- rewrite_tyvar1 tv + case mb_yes of + RTRFollowed ty1 co1 -> do + Reduction ty2 co2 <- rewrite_one ty1 + pure $ Reduction ty2 (co2 `mkTransCo` co1) + RTRNotFollowed -> do + tv' <- liftTcS $ updateTyVarKindM zonkTcType tv + role <- getRole + let ty' = mkTyVarTy tv' + return $ Reduction ty' (mkTcReflCo role ty') + +data RewriteTvResult + = RTRNotFollowed + | RTRFollowed Type Coercion + +rewrite_tyvar1 :: TcTyVar -> RewriteM RewriteTvResult +rewrite_tyvar1 tv = do + mb_ty <- liftTcS $ isFilledMetaTyVar_maybe tv + case mb_ty of + Just ty -> do + role <- getRole + return (RTRFollowed ty (mkReflCo role ty)) + Nothing -> do + fr <- getFlavourRole + rewrite_tyvar2 tv fr + +rewrite_tyvar2 :: TcTyVar -> CtFlavourRole -> RewriteM RewriteTvResult +rewrite_tyvar2 tv fr@(_, eq_rel) = do + ieqs <- liftTcS $ getInertEqs + case lookupDVarEnv ieqs tv of +#if MIN_VERSION_ghc(9,2,0) + Just (EqualCtList (ct :| _)) + | CEqCan { cc_ev = ctev, cc_lhs = TyVarLHS {} + , cc_rhs = rhs_ty, cc_eq_rel = ct_eq_rel } <- ct +#else + Just (ct : _) + | CTyEqCan { cc_ev = ctev + , cc_rhs = rhs_ty, cc_eq_rel = ct_eq_rel } <- ct +#endif + , let ct_fr = (ctEvFlavour ctev, ct_eq_rel) + , ct_fr `eqCanRewriteFR` fr + -> do + let rewrite_co1 = mkSymCo (ctEvCoercion ctev) + rewrite_co2 = case (ct_eq_rel, eq_rel) of + (ReprEq, _rel) -> rewrite_co1 + (NomEq, NomEq) -> rewrite_co1 + (NomEq, ReprEq) -> mkSubCo rewrite_co1 + return (RTRFollowed rhs_ty rewrite_co2) + _other -> return RTRNotFollowed + +rewrite_vector :: Kind + -> [Role] + -> [Type] + -> RewriteM ([Xi], [Coercion], MCoercionN) +rewrite_vector ki roles tys = do + eq_rel <- getEqRel + case eq_rel of + NomEq -> + rewrite_args bndrs + any_named_bndrs + inner_ki + fvs + Nothing + tys + ReprEq -> + rewrite_args bndrs + any_named_bndrs + inner_ki + fvs + (Just roles) + tys + where + (bndrs, inner_ki, any_named_bndrs) = split_pi_tys' ki + fvs = tyCoVarsOfType ki +{-# INLINE rewrite_vector #-} + +homogenise_result :: Xi + -> Coercion + -> Role + -> MCoercionN + -> Reduction +homogenise_result xi co _ MRefl = Reduction xi co +homogenise_result xi co r mco@(MCo kind_co) + = Reduction (xi `mkCastTy` kind_co) ((mkSymCo $ GRefl r xi mco) `mkTransCo` co) +split_pi_tys' :: Type -> ([TyCoBinder], Type, Bool) +split_pi_tys' ty = split ty ty + where + split _ (ForAllTy b res) = + let !(bs, ty', _) = split res res + in (Named b : bs, ty', True) + split _ (FunTy { ft_af = af, ft_mult = w, ft_arg = arg, ft_res = res }) = + let !(bs, ty', named) = split res res + in (Anon af (mkScaled w arg) : bs, ty', named) + split orig_ty ty' | Just ty'' <- coreView ty' = split orig_ty ty'' + split orig_ty _ = ([], orig_ty, False) +{-# INLINE split_pi_tys' #-} + +ty_con_binders_ty_binders' :: [TyConBinder] -> ([TyCoBinder], Bool) +ty_con_binders_ty_binders' = foldr go ([], False) + where + go (Bndr tv (NamedTCB vis)) (bndrs, _) + = (Named (Bndr tv vis) : bndrs, True) + go (Bndr tv (AnonTCB af)) (bndrs, n) + = (Anon af (tymult (tyVarKind tv)) : bndrs, n) + {-# INLINE go #-} +{-# INLINE ty_con_binders_ty_binders' #-} + +rewrite_args :: [TyCoBinder] -> Bool + -> Kind -> TcTyCoVarSet + -> Maybe [Role] -> [Type] + -> RewriteM ([Xi], [Coercion], MCoercionN) +rewrite_args orig_binders + any_named_bndrs + orig_inner_ki + orig_fvs + orig_m_roles + orig_tys + = case (orig_m_roles, any_named_bndrs) of + (Nothing, False) -> rewrite_args_fast orig_tys + _ -> rewrite_args_slow orig_binders orig_inner_ki orig_fvs orig_roles orig_tys + where orig_roles = fromMaybe (repeat Nominal) orig_m_roles + +{-# INLINE rewrite_args_fast #-} +rewrite_args_fast :: [Type] + -> RewriteM ([Xi], [Coercion], MCoercionN) +rewrite_args_fast orig_tys + = fmap finish (iterateRewrite orig_tys) + where + + iterateRewrite :: [Type] -> RewriteM ([Xi], [Coercion]) + iterateRewrite (ty:tys) = do + Reduction xi co <- rewrite_one ty + (xis, coercions) <- iterateRewrite tys + pure (xi : xis, co : coercions) + iterateRewrite [] = pure ([], []) + + {-# INLINE finish #-} + finish :: ([Xi], [Coercion]) -> ([Xi], [Coercion], MCoercionN) + finish (xis, coercions) = (xis, coercions, MRefl) + +{-# INLINE rewrite_args_slow #-} +rewrite_args_slow :: [TyCoBinder] -> Kind -> TcTyCoVarSet + -> [Role] -> [Type] + -> RewriteM ([Xi], [Coercion], MCoercionN) +rewrite_args_slow binders inner_ki fvs roles tys = do + rewritten_args <- + zipWith3M fl (map isNamedBinder binders ++ repeat True) + roles tys + pure +#if !MIN_VERSION_ghc(9,2,0) + $ ( \ ( xs, cs, c ) -> ( xs, cs, coToMCo c ) ) +#endif + $ simplifyArgsWorker binders inner_ki fvs roles rewritten_args + where + {-# INLINE fl #-} + fl :: Bool -> Role -> Type -> RewriteM ( Type, Coercion ) + fl True r ty = noBogusCoercions $ runReduction1 <$> fl1 r ty + fl False r ty = runReduction1 <$> fl1 r ty + + {-# INLINE fl1 #-} + fl1 :: Role -> Type -> RewriteM Reduction + fl1 Nominal ty + = setEqRel NomEq $ + rewrite_one ty + + fl1 Representational ty + = setEqRel ReprEq $ + rewrite_one ty + + fl1 Phantom ty + = do { ty' <- liftTcS $ zonkTcType ty + ; pure $ Reduction ty' ( mkReflCo Phantom ty' ) } + +noBogusCoercions :: RewriteM a -> RewriteM a +noBogusCoercions thing_inside + = RewriteM \ env s -> + let !renv = rewriteEnv env + !renv' = case fe_flavour renv of + Derived -> renv { fe_flavour = Wanted WDeriv } + _ -> renv + !env' = env { rewriteEnv = renv' } + in + runRewriteM thing_inside env' s + +chkAppend :: [a] -> [a] -> [a] +chkAppend xs ys + | null ys = xs + | otherwise = xs ++ ys + +-------------------------------------------------------------------------------- + +data ReduceQ = NoReduction | DidReduce +instance Semigroup ReduceQ where + NoReduction <> NoReduction = NoReduction + _ <> _ = DidReduce +instance Monoid ReduceQ where + mempty = NoReduction + +data RewriteState = + RewriteState + { rewrittenCts :: ![ Ct ] + , reductionOccurred :: !ReduceQ + } + +type RewrittenTyFamApps = + UniqDFM +#if MIN_VERSION_ghc(9,2,0) + TyCon +#else + Unique +#endif + ( ListMap LooseTypeMap ( Maybe Reduction, [Ct] ) ) + +data ShimRewriteEnv + = ShimRewriteEnv + { rewriters :: !Rewriters + , rewriteEnv :: !RewriteEnv + , rewriteCt :: !Ct + , rewriteGivens :: ![ Ct ] + , rewriteCache :: !( IORef RewrittenTyFamApps ) + } + +newtype RewriteM a + = RewriteM + { runRewriteM + :: ShimRewriteEnv + -> RewriteState + -> TcS ( a, RewriteState ) + } + deriving ( Functor, Applicative, Monad ) + via ( ReaderT ShimRewriteEnv + ( StateT RewriteState TcS ) + ) + +runRewritePluginM :: ShimRewriteEnv + -> RewriteM a + -> TcPluginM ( Maybe a, [Ct] ) +runRewritePluginM env ( RewriteM { runRewriteM = run } ) = do + + evBindsVar <- getEvBindsTcPluginM + ( a, RewriteState newCts didReduce ) + <- unsafeTcPluginTcM + $ runTcSWithEvBinds evBindsVar + $ run env ( RewriteState [] NoReduction ) + let + mb_a = case didReduce of + NoReduction -> Nothing + DidReduce -> Just a + pure ( mb_a, newCts ) + +setDidReduce :: RewriteM () +setDidReduce = RewriteM \ _env ( RewriteState cts _ ) -> + pure ( (), RewriteState cts DidReduce ) + +addRewriting :: TyCon -> [Type] -> Maybe Reduction -> [Ct] -> RewriteM ( Maybe Reduction ) +addRewriting tc tys mbRedn newCts = RewriteM \ env ( RewriteState cts s ) -> do + rewritings <- liftIOTcS $ readIORef ( rewriteCache env ) + let + s' :: ReduceQ + s' + | Just _ <- mbRedn + = DidReduce + | otherwise + = s + newRewritings :: RewrittenTyFamApps + newRewritings = insertFunEq rewritings tc tys ( mbRedn, newCts ) + mbEmittedWork :: Maybe ( Maybe Reduction, [Ct] ) + mbEmittedWork = findFunEq rewritings tc tys + case mbEmittedWork of + -- We've already rewritten this. + -- Avoid emitting constraints for it again, + -- to avoid sending the constraint solver in a loop. + -- TODO: this is quite fragile. + Just _ -> pure ( mbRedn, RewriteState cts s' ) + Nothing -> do + liftIOTcS $ writeIORef ( rewriteCache env ) newRewritings + pure ( mbRedn , RewriteState ( cts <> newCts ) s' ) + +-- Silly workaround because wrapTcS is not exported in GHC 9.0 +liftIOTcS :: IO a -> TcS a +liftIOTcS = runTcPluginTcS . tcPluginIO + +getRewriters :: RewriteM Rewriters +getRewriters = RewriteM \ env s -> pure ( rewriters env, s ) + +getGivens :: RewriteM [Ct] +getGivens = RewriteM \ env s -> pure ( rewriteGivens env, s ) + +getRewriteCache :: RewriteM ( IORef RewrittenTyFamApps ) +getRewriteCache = RewriteM \ env s -> pure ( rewriteCache env, s ) + +getRewriteCt :: RewriteM Ct +getRewriteCt = RewriteM \ env s -> pure ( rewriteCt env, s ) + +getRewriteEnvField :: (RewriteEnv -> a) -> RewriteM a +getRewriteEnvField accessor = RewriteM \ env s -> + pure ( accessor ( rewriteEnv env ), s ) + +getEqRel :: RewriteM EqRel +getEqRel = getRewriteEnvField fe_eq_rel + +getRole :: RewriteM Role +getRole = eqRelRole <$> getEqRel + +getFlavour :: RewriteM CtFlavour +getFlavour = getRewriteEnvField fe_flavour + +getFlavourRole :: RewriteM CtFlavourRole +getFlavourRole = do + flavour <- getFlavour + eq_rel <- getEqRel + return (flavour, eq_rel) + +setEqRel :: EqRel -> RewriteM a -> RewriteM a +setEqRel new_eq_rel thing_inside = RewriteM \ env s -> + if new_eq_rel == fe_eq_rel ( rewriteEnv env ) + then runRewriteM thing_inside env s + else runRewriteM thing_inside ( setEqRel' env ) s + where + setEqRel' :: ShimRewriteEnv -> ShimRewriteEnv + setEqRel' env = env { rewriteEnv = ( rewriteEnv env ) { fe_eq_rel = new_eq_rel } } +{-# INLINE setEqRel #-} + +liftTcS :: TcS a -> RewriteM a +liftTcS thing_inside = RewriteM \ _env s -> do + a <- thing_inside + pure ( a, s ) + +traceRewriteM :: String -> SDoc -> RewriteM () +traceRewriteM herald doc = liftTcS $ traceTcS herald doc +{-# INLINE traceRewriteM #-} + +getLoc :: RewriteM CtLoc +getLoc = getRewriteEnvField fe_loc + +checkStackDepth :: Type -> RewriteM () +checkStackDepth ty = do + loc <- getLoc + liftTcS $ checkReductionDepth loc ty + +bumpDepth :: RewriteM a -> RewriteM a +bumpDepth (RewriteM thing_inside) = RewriteM \ env s -> do + let !renv = rewriteEnv env + !renv' = renv { fe_loc = bumpCtLocDepth ( fe_loc renv ) } + !env' = env { rewriteEnv = renv' } + thing_inside env' s + +#if !MIN_VERSION_ghc(9,2,0) +-------------------------------------------------------------------------------- +-- GHC 9.0 compatibility. + +firstJustsM :: (Monad m, Foldable f) => f (m (Maybe a)) -> m (Maybe a) +firstJustsM = foldlM go Nothing where + go :: Monad m => Maybe a -> m (Maybe a) -> m (Maybe a) + go Nothing action = action + go result@(Just _) _action = return result + +lookupFamAppCache :: TyCon -> [Type] -> TcS (Maybe (Coercion, Type)) +lookupFamAppCache fam_tc tys = do + res <- lookupFlatCache fam_tc tys + pure $ case res of + Nothing -> Nothing + Just ( co, ty, _ ) -> Just ( co, ty ) + +extendFamAppCache :: TyCon -> [Type] -> (Coercion, Type) -> CtFlavour -> TcS () +extendFamAppCache tc xi_args (co, ty) f = extendFlatCache tc xi_args (co, ty, f) + +lookupFamAppInert :: TyCon -> [Type] -> TcS (Maybe (Coercion, Type, CtFlavourRole)) +lookupFamAppInert tc tys = do + res <- lookupFlatCache tc tys + pure $ case res of + Nothing -> Nothing + Just ( co, ty, f ) -> Just ( co, ty, (f, NomEq) ) + +tcSplitForAllTyVarBinders :: Type -> ([TyVarBinder], Type) +tcSplitForAllTyVarBinders = tcSplitForAllVarBndrs + +#endif