diff --git a/changelog.md b/changelog.md --- a/changelog.md +++ b/changelog.md @@ -1,102 +1,106 @@ - -# Version 0.8.0.0 (2022-07-07) - -- Compatibility for GHC 9.4. - -- Change API for `lookupImportedModule` to use `PkgQual` and `UnitId` - instead of `Maybe FastString`, with back-compatibility function `pkgQual_pkg` - for use with older module lookup functions. - -- Re-export `splitAppTys` and `unpackFS`. - -# Version 0.7.1.0 (2022-01-04) - -- `newWanted` now always uses the `CtLoc` information that it is provided with, - as opposed to obtaining some information from the monadic environment. - This means you no longer need to wrap calls to `newWanted` in `setCtLocM` - to ensure that GHC reports the correct source span when reporting unsolved - Wanteds in error messages. - -- Remove the `newDerived` function, as Derived constraints are going to be - removed from GHC. - -# Version 0.7.0.0 (2021-12-31) - -- Re-export functions for dealing with type-level literals, - such as `mkNumLitTy` and `isStrLitTy`. - -- Re-export functions for splitting apart type applications, such as - `splitAppTy_maybe` and `tyConAppTyCon_maybe`. - -- Redefine and re-export `mkUncheckedIntExpr` for GHC versions prior to 9.0. - -- Re-export some basic types from `GHC.Types.Basic` such as `Arity`, - `PromotionFlag` and `Boxity`. - -- Re-export `GHC.Builtin.Names` and `GHC.Builin.Types.Prim`. - -- Provide `MonadThings` instances for `TcPluginM` monads. - -# Version 0.6.1.0 (2021-12-13) - -- Re-export various useful types and functions to deal with type and coercion variables. - -- Re-export a few types and functions to deal with source locations. - -- Remove some re-exports for constructing function types, as not all functions make sense - across all GHC versions supported by the library. - -- Re-export `panic` and `pprPanic`. - -# Version 0.6.0.0 (2021-12-13) - -- Add support for GHC 8.8. - -- Re-export `evDataConApp`, which is useful for constructing typeclass dictionaries. - -# Version 0.5.1.0 (2021-08-31) - -- Fix a bug in the type-family rewriting compatibility layer (GHC 8.10, 9.0, 9.2) - by correctly downgrading the coercion used to cast the evidence, when necessary. - -# Version 0.5.0.0 (2021-08-30) - -- Re-export some additional types and functions that are useful for inspecting - and constructing evidence terms, such as `mkTyVar`, `newName`, `mkLocalId`, `lookupEvBind`... - -# Version 0.4.1.0 (2021-08-24) - -- Re-export a few GHC modules, such as GHC.Core.Make and GHC.Plugins. - These re-exports might be changed to be more selective in the future - to aid cross-version compatibility. - -# Version 0.4.0.0 (2021-08-24) - -- Adapt to GHC 9.4 changes in the `TcPluginSolveResult` datatype: - are now able to solve and emit constraints even when reporting - a contradiction. This can help with error messages. - Unfortunately these extra constraints will be dropped in versions - of GHC prior to 9.4. - -- Add a utility module for name resolution using constrained traversals. - -- Add compatibility for GHC 8.10. - -# Version 0.3.1.0 (2021-08-09) - -Ensure that the coercions stored in `Reduction`s are always -oriented left-to-right, by making the internal rewriting compatibility layer -also use left-to-right coercions. - -# Version 0.3.0.0 (2021-08-04) - -Account for changes in rewriting in GHC 9.4: - - - rewriter plugins can no longer emit new Wanted constraints - if they don't rewrite the type family application; - - coercions in the rewriter are now oriented left-to-right, - requiring `mkTyFamAppReduction` to be adapted. - -# Version 0.2.0.0 (2021-07-22) - -Initial release on Hackage. +# Version 0.8.1.0 (2022-10-05) + +- Bugfix for the GHC 9.2 (and below) rewriter plugin compatibility shim: + fix coercion orientations. + +# Version 0.8.0.0 (2022-07-07) + +- Compatibility for GHC 9.4. + +- Change API for `lookupImportedModule` to use `PkgQual` and `UnitId` + instead of `Maybe FastString`, with back-compatibility function `pkgQual_pkg` + for use with older module lookup functions. + +- Re-export `splitAppTys` and `unpackFS`. + +# Version 0.7.1.0 (2022-01-04) + +- `newWanted` now always uses the `CtLoc` information that it is provided with, + as opposed to obtaining some information from the monadic environment. + This means you no longer need to wrap calls to `newWanted` in `setCtLocM` + to ensure that GHC reports the correct source span when reporting unsolved + Wanteds in error messages. + +- Remove the `newDerived` function, as Derived constraints are going to be + removed from GHC. + +# Version 0.7.0.0 (2021-12-31) + +- Re-export functions for dealing with type-level literals, + such as `mkNumLitTy` and `isStrLitTy`. + +- Re-export functions for splitting apart type applications, such as + `splitAppTy_maybe` and `tyConAppTyCon_maybe`. + +- Redefine and re-export `mkUncheckedIntExpr` for GHC versions prior to 9.0. + +- Re-export some basic types from `GHC.Types.Basic` such as `Arity`, + `PromotionFlag` and `Boxity`. + +- Re-export `GHC.Builtin.Names` and `GHC.Builin.Types.Prim`. + +- Provide `MonadThings` instances for `TcPluginM` monads. + +# Version 0.6.1.0 (2021-12-13) + +- Re-export various useful types and functions to deal with type and coercion variables. + +- Re-export a few types and functions to deal with source locations. + +- Remove some re-exports for constructing function types, as not all functions make sense + across all GHC versions supported by the library. + +- Re-export `panic` and `pprPanic`. + +# Version 0.6.0.0 (2021-12-13) + +- Add support for GHC 8.8. + +- Re-export `evDataConApp`, which is useful for constructing typeclass dictionaries. + +# Version 0.5.1.0 (2021-08-31) + +- Fix a bug in the type-family rewriting compatibility layer (GHC 8.10, 9.0, 9.2) + by correctly downgrading the coercion used to cast the evidence, when necessary. + +# Version 0.5.0.0 (2021-08-30) + +- Re-export some additional types and functions that are useful for inspecting + and constructing evidence terms, such as `mkTyVar`, `newName`, `mkLocalId`, `lookupEvBind`... + +# Version 0.4.1.0 (2021-08-24) + +- Re-export a few GHC modules, such as GHC.Core.Make and GHC.Plugins. + These re-exports might be changed to be more selective in the future + to aid cross-version compatibility. + +# Version 0.4.0.0 (2021-08-24) + +- Adapt to GHC 9.4 changes in the `TcPluginSolveResult` datatype: + are now able to solve and emit constraints even when reporting + a contradiction. This can help with error messages. + Unfortunately these extra constraints will be dropped in versions + of GHC prior to 9.4. + +- Add a utility module for name resolution using constrained traversals. + +- Add compatibility for GHC 8.10. + +# Version 0.3.1.0 (2021-08-09) + +Ensure that the coercions stored in `Reduction`s are always +oriented left-to-right, by making the internal rewriting compatibility layer +also use left-to-right coercions. + +# Version 0.3.0.0 (2021-08-04) + +Account for changes in rewriting in GHC 9.4: + + - rewriter plugins can no longer emit new Wanted constraints + if they don't rewrite the type family application; + - coercions in the rewriter are now oriented left-to-right, + requiring `mkTyFamAppReduction` to be adapted. + +# Version 0.2.0.0 (2021-07-22) + +Initial release on Hackage. diff --git a/ghc-tcplugin-api.cabal b/ghc-tcplugin-api.cabal --- a/ghc-tcplugin-api.cabal +++ b/ghc-tcplugin-api.cabal @@ -1,158 +1,158 @@ -cabal-version: 3.0 -name: ghc-tcplugin-api -version: 0.8.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 - for example usage. - -extra-source-files: - changelog.md - -library - - build-depends: - base - >= 4.13.0 && < 4.19, - ghc - >= 8.8 && < 9.7, - 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.Names, - GHC.TcPlugin.API.Internal - - reexported-modules: - GHC.Builtin.Names - , GHC.Builtin.Types - , GHC.Builtin.Types.Prim - , GHC.Core.Make - , GHC.Plugins - , GHC.Types.Unique.DFM - , GHC.Types.Unique.FM - , GHC.Utils.Outputable - - if impl(ghc >= 9.3.0) - cpp-options: -DHAS_REWRITING - else - cpp-options: -DHAS_DERIVEDS - other-modules: - GHC.TcPlugin.API.Internal.Shim - GHC.TcPlugin.API.Internal.Shim.Reduction - - -- Compatibility for versions of GHC prior to 9.0. - if impl(ghc < 9.0) - - mixins: - ghc - ( GHC as GHC - - , PrelNames as GHC.Builtin.Names - , TysWiredIn as GHC.Builtin.Types - , TysPrim as GHC.Builtin.Types.Prim - - , CoreSyn as GHC.Core - , CoAxiom as GHC.Core.Coercion.Axiom - , Coercion as GHC.Core.Coercion - , Class as GHC.Core.Class - , DataCon as GHC.Core.DataCon - , FamInstEnv as GHC.Core.FamInstEnv - , InstEnv as GHC.Core.InstEnv - , MkCore as GHC.Core.Make - , TyCoRep as GHC.Core.TyCo.Rep - , TyCon as GHC.Core.TyCon - , Type as GHC.Core.Type - - , FastString as GHC.Data.FastString - , Pair as GHC.Data.Pair - - , Finder as GHC.Driver.Finder - , DynFlags as GHC.Driver.Session - , HscTypes as GHC.Driver.Types - - , GhcPlugins as GHC.Plugins - - , TcPluginM as GHC.Tc.Plugin - , TcSMonad as GHC.Tc.Solver.Monad - , TcRnTypes as GHC.Tc.Types - , TcEvidence as GHC.Tc.Types.Evidence - , TcRnMonad as GHC.Tc.Utils.Monad - , TcType as GHC.Tc.Utils.TcType - , TcMType as GHC.Tc.Utils.TcMType - - , BasicTypes as GHC.Types.Basic - , Id as GHC.Types.Id - , Literal as GHC.Types.Literal - , Name as GHC.Types.Name - , OccName as GHC.Types.Name.Occurrence - , SrcLoc as GHC.Types.SrcLoc - , Unique as GHC.Types.Unique - , UniqDFM as GHC.Types.Unique.DFM - , UniqFM as GHC.Types.Unique.FM - , Var as GHC.Types.Var - , VarEnv as GHC.Types.Var.Env - , VarSet as GHC.Types.Var.Set - - , Module as GHC.Unit.Module - , Module as GHC.Unit.Module.Name - , Module as GHC.Unit.Types - - , Util as GHC.Utils.Misc - , TcRnMonad as GHC.Utils.Monad - , Outputable as GHC.Utils.Outputable - , Panic as GHC.Utils.Panic - ) - - if impl(ghc > 8.10) - - mixins: - ghc - ( Predicate as GHC.Core.Predicate - , Constraint as GHC.Tc.Types.Constraint - , TcOrigin as GHC.Tc.Types.Origin - ) - - else - - mixins: - ghc - ( Type as GHC.Core.Predicate - , TcRnTypes as GHC.Tc.Types.Constraint - , TcRnTypes as GHC.Tc.Types.Origin - ) +cabal-version: 3.0 +name: ghc-tcplugin-api +version: 0.8.1.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 + for example usage. + +extra-source-files: + changelog.md + +library + + build-depends: + base + >= 4.13.0 && < 4.19, + ghc + >= 8.8 && < 9.7, + 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.Names, + GHC.TcPlugin.API.Internal + + reexported-modules: + GHC.Builtin.Names + , GHC.Builtin.Types + , GHC.Builtin.Types.Prim + , GHC.Core.Make + , GHC.Plugins + , GHC.Types.Unique.DFM + , GHC.Types.Unique.FM + , GHC.Utils.Outputable + + if impl(ghc >= 9.3.0) + cpp-options: -DHAS_REWRITING + else + cpp-options: -DHAS_DERIVEDS + other-modules: + GHC.TcPlugin.API.Internal.Shim + GHC.TcPlugin.API.Internal.Shim.Reduction + + -- Compatibility for versions of GHC prior to 9.0. + if impl(ghc < 9.0) + + mixins: + ghc + ( GHC as GHC + + , PrelNames as GHC.Builtin.Names + , TysWiredIn as GHC.Builtin.Types + , TysPrim as GHC.Builtin.Types.Prim + + , CoreSyn as GHC.Core + , CoAxiom as GHC.Core.Coercion.Axiom + , Coercion as GHC.Core.Coercion + , Class as GHC.Core.Class + , DataCon as GHC.Core.DataCon + , FamInstEnv as GHC.Core.FamInstEnv + , InstEnv as GHC.Core.InstEnv + , MkCore as GHC.Core.Make + , TyCoRep as GHC.Core.TyCo.Rep + , TyCon as GHC.Core.TyCon + , Type as GHC.Core.Type + + , FastString as GHC.Data.FastString + , Pair as GHC.Data.Pair + + , Finder as GHC.Driver.Finder + , DynFlags as GHC.Driver.Session + , HscTypes as GHC.Driver.Types + + , GhcPlugins as GHC.Plugins + + , TcPluginM as GHC.Tc.Plugin + , TcSMonad as GHC.Tc.Solver.Monad + , TcRnTypes as GHC.Tc.Types + , TcEvidence as GHC.Tc.Types.Evidence + , TcRnMonad as GHC.Tc.Utils.Monad + , TcType as GHC.Tc.Utils.TcType + , TcMType as GHC.Tc.Utils.TcMType + + , BasicTypes as GHC.Types.Basic + , Id as GHC.Types.Id + , Literal as GHC.Types.Literal + , Name as GHC.Types.Name + , OccName as GHC.Types.Name.Occurrence + , SrcLoc as GHC.Types.SrcLoc + , Unique as GHC.Types.Unique + , UniqDFM as GHC.Types.Unique.DFM + , UniqFM as GHC.Types.Unique.FM + , Var as GHC.Types.Var + , VarEnv as GHC.Types.Var.Env + , VarSet as GHC.Types.Var.Set + + , Module as GHC.Unit.Module + , Module as GHC.Unit.Module.Name + , Module as GHC.Unit.Types + + , Util as GHC.Utils.Misc + , TcRnMonad as GHC.Utils.Monad + , Outputable as GHC.Utils.Outputable + , Panic as GHC.Utils.Panic + ) + + if impl(ghc > 8.10) + + mixins: + ghc + ( Predicate as GHC.Core.Predicate + , Constraint as GHC.Tc.Types.Constraint + , TcOrigin as GHC.Tc.Types.Origin + ) + + else + + mixins: + ghc + ( Type as GHC.Core.Predicate + , TcRnTypes as GHC.Tc.Types.Constraint + , TcRnTypes as GHC.Tc.Types.Origin + ) diff --git a/src/GHC/TcPlugin/API.hs b/src/GHC/TcPlugin/API.hs --- a/src/GHC/TcPlugin/API.hs +++ b/src/GHC/TcPlugin/API.hs @@ -1,1005 +1,1005 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE LambdaCase #-} -{-# 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 -. - -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, unpackFS, mkModuleName - , unitIdFS, stringToUnitId, pkgQual_pkg - , Module, ModuleName, FindResult(..), UnitId, PkgQual(..) - - -- ** 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", which is re-exported by this library, - -- 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 -#if !MIN_VERSION_ghc(9,0,0) - , mkUncheckedIntExpr -#endif - - -- | ==== 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 - - -- ** 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 - - -- ** Type literals (natural numbers, type-level strings) - , mkNumLitTy, isNumLitTy - , mkStrLitTy, isStrLitTy - - -- ** Creating and decomposing applications - , mkTyConTy, mkTyConApp, mkAppTy, mkAppTys - , splitTyConApp_maybe - , tyConAppTyConPicky_maybe, tyConAppTyCon_maybe - , splitAppTy_maybe, splitAppTys - - -- ** Function types - , mkVisFunTyMany, mkVisFunTysMany - , 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. - -- - -- Refer to "GHC.Builtin.Names", "GHC.Builtin.Types" and "GHC.Builtin.Types.Prim". - - -- * GHC types - - -- | These are the types that the plugin will inspect and manipulate. - - -- | = END OF API DOCUMENTATION, RE-EXPORTS FOLLOW - - -- | == Some basic types - - , module GHC.Types.Basic - - -- | == Names - , Name, OccName, TyThing, TcTyThing - , MonadThings(..) - , 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, CoreExpr - , TcEvDest(..) - - -- | == The type-checking environment - , TcGblEnv, TcLclEnv - - -- | == Source locations - , GenLocated(..), Located, RealLocated - , unLoc, getLoc - - -- | == Pretty-printing - , SDoc, Outputable(..) - - ) - where - --- ghc -import GHC - ( TyThing(..) ) -#if !MIN_VERSION_ghc(9,0,0) -import GHC.Builtin.Types - ( intDataCon ) -import GHC.Builtin.Types.Prim - ( intPrimTy ) -#endif -import GHC.Core - ( CoreBndr, CoreExpr, 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(..) ) -#if !MIN_VERSION_ghc(9,0,0) -import GHC.Core.Make - ( mkCoreConApps ) -#endif -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 - , mkVisFunTyMany, mkVisFunTysMany - , mkInvisFunTyMany, mkInvisFunTysMany -#elif MIN_VERSION_ghc(8,10,0) - , mkVisFunTy, mkVisFunTys - , 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 - , splitAppTy_maybe, splitAppTys - , tyConAppTyConPicky_maybe, tyConAppTyCon_maybe - , mkAppTy, mkAppTys, isTyVarTy, getTyVar_maybe - , mkCoercionTy, isCoercionTy, isCoercionTy_maybe - , mkNumLitTy, isNumLitTy, mkStrLitTy, isStrLitTy -#if MIN_VERSION_ghc(9,0,0) - , pattern One, pattern Many -#endif - ) -import GHC.Data.FastString - ( FastString, fsLit, unpackFS ) -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.Basic - ( Arity, PromotionFlag(..), isPromoted - , Boxity(..), TupleSort(..) - ) -import GHC.Types.Id - ( Id, mkLocalId ) -#if !MIN_VERSION_ghc(9,0,0) -import GHC.Types.Literal - ( Literal(..), LitNumType(..) ) -#endif -import GHC.Types.Name - ( Name ) -import GHC.Types.Name.Occurrence - ( OccName(..) - , mkVarOcc, mkDataOcc, mkTyVarOcc, mkTcOcc, mkClsOcc - ) -#if MIN_VERSION_ghc(9,3,0) -import GHC.Types.PkgQual - ( PkgQual(..) ) -#endif -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,3,0) - , (<+>), doubleQuotes, empty, text -#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 - ( UnitId, unitIdFS, stringToUnitId, mkModuleName ) -#if MIN_VERSION_ghc(9,5,0) -import Language.Haskell.Syntax.Module.Name - ( ModuleName ) -#else -import GHC.Unit.Module.Name - ( ModuleName ) -#endif -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 - --------------------------------------------------------------------------------- - -#if !MIN_VERSION_ghc(9,3,0) --- | Package-qualifier after renaming -data PkgQual - = NoPkgQual -- ^ No package qualifier - | ThisPkg UnitId -- ^ Import from home-unit - | OtherPkg UnitId -- ^ Import from another unit - deriving stock ( Ord, Eq ) - -instance Outputable PkgQual where - ppr = \case - NoPkgQual -> empty - ThisPkg u -> doubleQuotes (ppr u) - OtherPkg u -> doubleQuotes (ppr u) -#endif - --- | Compatibility function to convert a 'PkgQual' to @Maybe FastString@ --- on older versions of GHC (9.2 and below). --- --- On newer GHCs, this is the identity function. -pkgQual_pkg :: PkgQual -#if MIN_VERSION_ghc(9,3,0) - -> PkgQual -#else - -> Maybe FastString -#endif -pkgQual_pkg pkg = -#if MIN_VERSION_ghc(9,3,0) - pkg -#else - case pkg of - NoPkgQual -> Nothing - ThisPkg this -> - let fs = unitIdFS this - in if fs == fsLit "this" - then Just fs - else pprPanic "pkgQual_pkg: \'ThisPkg\' package name should be \"this\"" (text "pkg:" <+> ppr pkg) - OtherPkg unit_id -> Just $ unitIdFS unit_id -#endif - --- | Lookup a Haskell module from the given package. -findImportedModule :: MonadTcPlugin m - => ModuleName -- ^ Module name, e.g. @"Data.List"@. - -> PkgQual -- ^ Package name, e.g. @Just "base"@. - -- Use @Nothing@ for the current home package - -> m FindResult -findImportedModule mod_name pkg - = liftTcPluginM - $ GHC.findImportedModule mod_name (pkgQual_pkg 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 ( \ (co,ty) -> mkReduction (mkSymCo co) ty ) <$> - -- GHC 9.0 and 9.2 use a different orientation - -- when rewriting type family applications. -#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 Wanted 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 = -#if !HAS_REWRITING - -- On GHC 9.2 and below, 'newWanted' doesn't use the location information - -- that is passed to it, retrieving it from the 'TcM' environment instead. - -- https://gitlab.haskell.org/ghc/ghc/-/issues/20895 - setCtLocM loc $ -#endif - liftTcPluginM $ GHC.newWanted loc pty - --- | Create a new Given constraint. --- --- Unlike 'newWanted', we need to supply evidence for this constraint. -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 = -#if MIN_VERSION_ghc(9,3,0) - re_loc -#else - fe_loc -#endif - --- | Set the location information for a computation. -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 <- rewriteEnvCtLoc <$> 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 ( mkPluginUnivCo str role ( mkTyConApp tc args ) ty ) ty - --------------------------------------------------------------------------------- - -#if !MIN_VERSION_ghc(9,0,0) - -type UniqFM ty a = GHC.UniqFM a - -mkUncheckedIntExpr :: Integer -> CoreExpr -mkUncheckedIntExpr i = mkCoreConApps intDataCon [Lit lit] - where - lit = LitNumber LitNumInt i intPrimTy - -#if MIN_VERSION_ghc(8,10,0) - -mkInvisFunTyMany, mkVisFunTyMany :: Type -> Type -> Type -mkInvisFunTyMany = mkInvisFunTy -mkVisFunTyMany = mkVisFunTy - -mkInvisFunTysMany, mkVisFunTysMany :: [Type] -> Type -> Type -mkInvisFunTysMany = mkInvisFunTys -mkVisFunTysMany = mkVisFunTys - -#else - -type Pred = PredTree - -mkInvisFunTyMany, mkVisFunTyMany :: Type -> Type -> Type -mkInvisFunTyMany = mkFunTy -mkVisFunTyMany = mkFunTy - -mkInvisFunTysMany, mkVisFunTysMany :: [Type] -> Type -> Type -mkInvisFunTysMany = mkFunTys -mkVisFunTysMany = 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 +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE LambdaCase #-} +{-# 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 +. + +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, unpackFS, mkModuleName + , unitIdFS, stringToUnitId, pkgQual_pkg + , Module, ModuleName, FindResult(..), UnitId, PkgQual(..) + + -- ** 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", which is re-exported by this library, + -- 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 +#if !MIN_VERSION_ghc(9,0,0) + , mkUncheckedIntExpr +#endif + + -- | ==== 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 + + -- ** 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 + + -- ** Type literals (natural numbers, type-level strings) + , mkNumLitTy, isNumLitTy + , mkStrLitTy, isStrLitTy + + -- ** Creating and decomposing applications + , mkTyConTy, mkTyConApp, mkAppTy, mkAppTys + , splitTyConApp_maybe + , tyConAppTyConPicky_maybe, tyConAppTyCon_maybe + , splitAppTy_maybe, splitAppTys + + -- ** Function types + , mkVisFunTyMany, mkVisFunTysMany + , 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. + -- + -- Refer to "GHC.Builtin.Names", "GHC.Builtin.Types" and "GHC.Builtin.Types.Prim". + + -- * GHC types + + -- | These are the types that the plugin will inspect and manipulate. + + -- | = END OF API DOCUMENTATION, RE-EXPORTS FOLLOW + + -- | == Some basic types + + , module GHC.Types.Basic + + -- | == Names + , Name, OccName, TyThing, TcTyThing + , MonadThings(..) + , 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, CoreExpr + , TcEvDest(..) + + -- | == The type-checking environment + , TcGblEnv, TcLclEnv + + -- | == Source locations + , GenLocated(..), Located, RealLocated + , unLoc, getLoc + + -- | == Pretty-printing + , SDoc, Outputable(..) + + ) + where + +-- ghc +import GHC + ( TyThing(..) ) +#if !MIN_VERSION_ghc(9,0,0) +import GHC.Builtin.Types + ( intDataCon ) +import GHC.Builtin.Types.Prim + ( intPrimTy ) +#endif +import GHC.Core + ( CoreBndr, CoreExpr, 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(..) ) +#if !MIN_VERSION_ghc(9,0,0) +import GHC.Core.Make + ( mkCoreConApps ) +#endif +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 + , mkVisFunTyMany, mkVisFunTysMany + , mkInvisFunTyMany, mkInvisFunTysMany +#elif MIN_VERSION_ghc(8,10,0) + , mkVisFunTy, mkVisFunTys + , 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 + , splitAppTy_maybe, splitAppTys + , tyConAppTyConPicky_maybe, tyConAppTyCon_maybe + , mkAppTy, mkAppTys, isTyVarTy, getTyVar_maybe + , mkCoercionTy, isCoercionTy, isCoercionTy_maybe + , mkNumLitTy, isNumLitTy, mkStrLitTy, isStrLitTy +#if MIN_VERSION_ghc(9,0,0) + , pattern One, pattern Many +#endif + ) +import GHC.Data.FastString + ( FastString, fsLit, unpackFS ) +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.Basic + ( Arity, PromotionFlag(..), isPromoted + , Boxity(..), TupleSort(..) + ) +import GHC.Types.Id + ( Id, mkLocalId ) +#if !MIN_VERSION_ghc(9,0,0) +import GHC.Types.Literal + ( Literal(..), LitNumType(..) ) +#endif +import GHC.Types.Name + ( Name ) +import GHC.Types.Name.Occurrence + ( OccName(..) + , mkVarOcc, mkDataOcc, mkTyVarOcc, mkTcOcc, mkClsOcc + ) +#if MIN_VERSION_ghc(9,3,0) +import GHC.Types.PkgQual + ( PkgQual(..) ) +#endif +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,3,0) + , (<+>), doubleQuotes, empty, text +#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 + ( UnitId, unitIdFS, stringToUnitId, mkModuleName ) +#if MIN_VERSION_ghc(9,5,0) +import Language.Haskell.Syntax.Module.Name + ( ModuleName ) +#else +import GHC.Unit.Module.Name + ( ModuleName ) +#endif +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 + +-------------------------------------------------------------------------------- + +#if !MIN_VERSION_ghc(9,3,0) +-- | Package-qualifier after renaming +data PkgQual + = NoPkgQual -- ^ No package qualifier + | ThisPkg UnitId -- ^ Import from home-unit + | OtherPkg UnitId -- ^ Import from another unit + deriving stock ( Ord, Eq ) + +instance Outputable PkgQual where + ppr = \case + NoPkgQual -> empty + ThisPkg u -> doubleQuotes (ppr u) + OtherPkg u -> doubleQuotes (ppr u) +#endif + +-- | Compatibility function to convert a 'PkgQual' to @Maybe FastString@ +-- on older versions of GHC (9.2 and below). +-- +-- On newer GHCs, this is the identity function. +pkgQual_pkg :: PkgQual +#if MIN_VERSION_ghc(9,3,0) + -> PkgQual +#else + -> Maybe FastString +#endif +pkgQual_pkg pkg = +#if MIN_VERSION_ghc(9,3,0) + pkg +#else + case pkg of + NoPkgQual -> Nothing + ThisPkg this -> + let fs = unitIdFS this + in if fs == fsLit "this" + then Just fs + else pprPanic "pkgQual_pkg: \'ThisPkg\' package name should be \"this\"" (text "pkg:" <+> ppr pkg) + OtherPkg unit_id -> Just $ unitIdFS unit_id +#endif + +-- | Lookup a Haskell module from the given package. +findImportedModule :: MonadTcPlugin m + => ModuleName -- ^ Module name, e.g. @"Data.List"@. + -> PkgQual -- ^ Package name, e.g. @Just "base"@. + -- Use @Nothing@ for the current home package + -> m FindResult +findImportedModule mod_name pkg + = liftTcPluginM + $ GHC.findImportedModule mod_name (pkgQual_pkg 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 ( \ (co,ty) -> mkReduction (mkSymCo co) ty ) <$> + -- GHC 9.0 and 9.2 use a different orientation + -- when rewriting type family applications. +#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 Wanted 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 = +#if !HAS_REWRITING + -- On GHC 9.2 and below, 'newWanted' doesn't use the location information + -- that is passed to it, retrieving it from the 'TcM' environment instead. + -- https://gitlab.haskell.org/ghc/ghc/-/issues/20895 + setCtLocM loc $ +#endif + liftTcPluginM $ GHC.newWanted loc pty + +-- | Create a new Given constraint. +-- +-- Unlike 'newWanted', we need to supply evidence for this constraint. +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 = +#if MIN_VERSION_ghc(9,3,0) + re_loc +#else + fe_loc +#endif + +-- | Set the location information for a computation. +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 <- rewriteEnvCtLoc <$> 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 ( mkPluginUnivCo str role ( mkTyConApp tc args ) ty ) ty + +-------------------------------------------------------------------------------- + +#if !MIN_VERSION_ghc(9,0,0) + +type UniqFM ty a = GHC.UniqFM a + +mkUncheckedIntExpr :: Integer -> CoreExpr +mkUncheckedIntExpr i = mkCoreConApps intDataCon [Lit lit] + where + lit = LitNumber LitNumInt i intPrimTy + +#if MIN_VERSION_ghc(8,10,0) + +mkInvisFunTyMany, mkVisFunTyMany :: Type -> Type -> Type +mkInvisFunTyMany = mkInvisFunTy +mkVisFunTyMany = mkVisFunTy + +mkInvisFunTysMany, mkVisFunTysMany :: [Type] -> Type -> Type +mkInvisFunTysMany = mkInvisFunTys +mkVisFunTysMany = mkVisFunTys + +#else + +type Pred = PredTree + +mkInvisFunTyMany, mkVisFunTyMany :: Type -> Type -> Type +mkInvisFunTyMany = mkFunTy +mkVisFunTyMany = mkFunTy + +mkInvisFunTysMany, mkVisFunTysMany :: [Type] -> Type -> Type +mkInvisFunTysMany = mkFunTys +mkVisFunTysMany = 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 diff --git a/src/GHC/TcPlugin/API/Internal.hs b/src/GHC/TcPlugin/API/Internal.hs --- a/src/GHC/TcPlugin/API/Internal.hs +++ b/src/GHC/TcPlugin/API/Internal.hs @@ -1,575 +1,575 @@ -{-# LANGUAGE BlockArguments #-} -{-# LANGUAGE CPP #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE DerivingVia #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE GeneralizedNewtypeDeriving #-} -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE QuantifiedConstraints #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE RecordWildCards #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# 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 - , MonadThings(..) - , askRewriteEnv - , askDeriveds - , askEvBinds - , mkTcPlugin - , mkTcPluginErrorTy - ) - where - --- base -import Data.Coerce - ( Coercible ) -import Data.Kind - ( 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 ) -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 ) -#if MIN_VERSION_ghc(9,1,0) -import GHC.Types.TyThing - ( MonadThings(..) ) -#else -import GHC.Driver.Types - ( MonadThings(..) ) -#endif - --- ghc-tcplugin-api -#ifndef HAS_REWRITING -import GHC.TcPlugin.API.Internal.Shim - ( TcPluginSolveResult, TcPluginRewriteResult(..) - , 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 -#if MIN_VERSION_ghc(9,0,0) - GHC.TyCon -#endif - 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. -data family TcPluginM (s :: TcPluginStage) :: Type -> Type -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. -class ( Monad m, ( forall x y. Coercible x y => Coercible (m x) (m y) ) ) => MonadTcPlugin (m :: Type -> Type) 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@: - -- - -- - 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 - -- (no deriveds) - ( GHC.runTcPluginM - . ( \ f -> f builtinDefs evBinds ) - . 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 - -- (no deriveds) - adaptUserSolve :: ( userDefs -> TcPluginSolver ) - -> TcPluginDefs userDefs - -> GHC.TcPluginSolver - adaptUserSolve userSolve ( TcPluginDefs { tcPluginUserDefs, tcPluginBuiltinDefs } ) - = \ evBindsVar givens wanteds -> do - tcPluginSolveM ( userSolve tcPluginUserDefs givens wanteds ) - tcPluginBuiltinDefs evBindsVar - 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 -#if MIN_VERSION_ghc(9,0,0) - GHC.TyCon -#endif - TcPluginRewriter - ) - -> TcPluginDefs userDefs - -> GHC.TcPluginSolver - adaptUserSolveAndRewrite userSolve userRewrite ( TcPluginDefs { tcPluginUserDefs, tcPluginBuiltinDefs } ) - = \ givens deriveds wanteds -> do - evBindsVar <- GHC.getEvBindsTcPluginM - shimRewriter - givens deriveds wanteds - ( 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. -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 ] - -instance ( Monad (TcPluginM s), MonadTcPlugin (TcPluginM s) ) - => MonadThings (TcPluginM s) where - lookupThing = unsafeLiftTcM . lookupThing - --------------------------------------------------------------------------------- --- 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 - } - -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 - 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 ] +{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DerivingVia #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# 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 + , MonadThings(..) + , askRewriteEnv + , askDeriveds + , askEvBinds + , mkTcPlugin + , mkTcPluginErrorTy + ) + where + +-- base +import Data.Coerce + ( Coercible ) +import Data.Kind + ( 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 ) +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 ) +#if MIN_VERSION_ghc(9,1,0) +import GHC.Types.TyThing + ( MonadThings(..) ) +#else +import GHC.Driver.Types + ( MonadThings(..) ) +#endif + +-- ghc-tcplugin-api +#ifndef HAS_REWRITING +import GHC.TcPlugin.API.Internal.Shim + ( TcPluginSolveResult, TcPluginRewriteResult(..) + , 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 +#if MIN_VERSION_ghc(9,0,0) + GHC.TyCon +#endif + 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. +data family TcPluginM (s :: TcPluginStage) :: Type -> Type +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. +class ( Monad m, ( forall x y. Coercible x y => Coercible (m x) (m y) ) ) => MonadTcPlugin (m :: Type -> Type) 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@: + -- + -- + 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 + -- (no deriveds) + ( GHC.runTcPluginM + . ( \ f -> f builtinDefs evBinds ) + . 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 + -- (no deriveds) + adaptUserSolve :: ( userDefs -> TcPluginSolver ) + -> TcPluginDefs userDefs + -> GHC.TcPluginSolver + adaptUserSolve userSolve ( TcPluginDefs { tcPluginUserDefs, tcPluginBuiltinDefs } ) + = \ evBindsVar givens wanteds -> do + tcPluginSolveM ( userSolve tcPluginUserDefs givens wanteds ) + tcPluginBuiltinDefs evBindsVar + 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 +#if MIN_VERSION_ghc(9,0,0) + GHC.TyCon +#endif + TcPluginRewriter + ) + -> TcPluginDefs userDefs + -> GHC.TcPluginSolver + adaptUserSolveAndRewrite userSolve userRewrite ( TcPluginDefs { tcPluginUserDefs, tcPluginBuiltinDefs } ) + = \ givens deriveds wanteds -> do + evBindsVar <- GHC.getEvBindsTcPluginM + shimRewriter + givens deriveds wanteds + ( 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. +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 ] + +instance ( Monad (TcPluginM s), MonadTcPlugin (TcPluginM s) ) + => MonadThings (TcPluginM s) where + lookupThing = unsafeLiftTcM . lookupThing + +-------------------------------------------------------------------------------- +-- 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 + } + +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 + 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 ] diff --git a/src/GHC/TcPlugin/API/Internal/Shim.hs b/src/GHC/TcPlugin/API/Internal/Shim.hs --- a/src/GHC/TcPlugin/API/Internal/Shim.hs +++ b/src/GHC/TcPlugin/API/Internal/Shim.hs @@ -1,962 +1,962 @@ -{-# LANGUAGE BangPatterns #-} -{-# LANGUAGE BlockArguments #-} -{-# LANGUAGE CPP #-} -{-# LANGUAGE DerivingVia #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE NamedFieldPuns #-} -{-# 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 - ( Reduction(..), mkReduction - , TcPluginSolveResult(TcPluginContradiction, TcPluginOk, ..), TcPluginRewriteResult(..) - , RewriteEnv(..) - , shimRewriter - ) - where - --- base -import Prelude - hiding ( Floating(cos), iterate ) -import Control.Monad - ( forM, unless, when ) -import Data.Foldable - ( traverse_ -#if !MIN_VERSION_ghc(9,2,0) - , foldlM -#endif - ) -#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 - ( coercionRole - , mkReflCo, mkSymCo - , mkAppCos, mkNomReflCo, mkSubCo - , mkTyConAppCo, tyConRolesX - , tyConRolesRepresentational - ) -import GHC.Core.Predicate - ( EqRel(..), eqRelRole ) -import GHC.Core.TyCo.Rep - ( Type(..), Kind, Coercion(..), MCoercion(..), TyCoBinder(..) - , 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 , mkTyConApp -#if MIN_VERSION_ghc(9,0,0) - , mkScaled, tymult -#endif - , coreView, tyVarKind - ) -#if MIN_VERSION_ghc(9,2,0) -import GHC.Data.Maybe - ( firstJustsM ) -#endif -import GHC.Tc.Plugin - ( newWanted, newDerived ) -import GHC.Tc.Solver.Monad - ( TcS - , zonkCo, zonkTcType - , isFilledMetaTyVar_maybe - , getInertEqs - , checkReductionDepth - , matchFam - , runTcPluginTcS, runTcSWithEvBinds - , traceTcS - , setWantedEvTerm -#if MIN_VERSION_ghc(9,2,0) - , lookupFamAppCache, lookupFamAppInert, extendFamAppCache - , pattern EqualCtList -#else - , lookupFlatCache, extendFlatCache -#endif - ) -import GHC.Tc.Types - ( TcPluginM - , unsafeTcPluginTcM, getEvBindsTcPluginM - ) -import qualified GHC.Tc.Types as GHC - ( TcPluginResult(..) ) -import GHC.Tc.Types.Constraint - ( Ct(..), CtEvidence(..) - , CtLoc, CtFlavour(..), CtFlavourRole, ShadowInfo(..) -#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, mkTcTransCo , mkTcTyConAppCo - ) -import GHC.Tc.Utils.TcType - ( TcTyCoVarSet -#if MIN_VERSION_ghc(9,2,0) - , tcSplitForAllTyVarBinders -#else - , tcSplitForAllVarBndrs -#endif - , tcSplitTyConApp_maybe - , tcTypeKind - , tyCoVarsOfType - ) -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(..), SDoc, empty ) - --- ghc-tcplugin-api -import GHC.TcPlugin.API.Internal.Shim.Reduction - --------------------------------------------------------------------------------- - --- | The type-family rewriting environment. -data RewriteEnv - = FE { fe_loc :: !CtLoc - , fe_flavour :: !CtFlavour - , fe_eq_rel :: !EqRel - } - --- | Result of running a solver plugin. -data TcPluginSolveResult - = TcPluginSolveResult - { -- | Insoluble constraints found by the plugin. - -- - -- These constraints will be added to the inert set, - -- and reported as insoluble to the user. - tcPluginInsolubleCts :: [Ct] - -- | Solved constraints, together with their evidence. - -- - -- These are removed from the inert set, and the - -- evidence for them is recorded. - , tcPluginSolvedCts :: [(EvTerm, Ct)] - -- | New constraints that the plugin wishes to emit. - -- - -- These will be added to the work list. - , tcPluginNewCts :: [Ct] - } - --- | The plugin found a contradiction. --- The returned constraints are removed from the inert set, --- and recorded as insoluble. --- --- The returned list of constraints should never be empty. -pattern TcPluginContradiction :: [Ct] -> TcPluginSolveResult -pattern TcPluginContradiction insols - = TcPluginSolveResult - { tcPluginInsolubleCts = insols - , tcPluginSolvedCts = [] - , tcPluginNewCts = [] } - --- | The plugin has not found any contradictions, --- --- The first field is for constraints that were solved. --- The second field contains new work, that should be processed by --- the constraint solver. -pattern TcPluginOk :: [(EvTerm, Ct)] -> [Ct] -> TcPluginSolveResult -pattern TcPluginOk solved new - = TcPluginSolveResult - { tcPluginInsolubleCts = [] - , tcPluginSolvedCts = solved - , tcPluginNewCts = new } - --- The 'TcPluginSolveResult' datatype changed in GHC 9.4, --- allowing users to return solved and new constraints even in case of --- a contradiction. --- --- This function simply drops the solved and new constraints on older versions, --- although it does at least still bind the evidence in case of solved Wanteds. -adaptSolveResult :: Bool -> TcPluginSolveResult -> TcPluginM GHC.TcPluginResult -adaptSolveResult doingGivens - ( TcPluginSolveResult - { tcPluginInsolubleCts = insols - , tcPluginSolvedCts = solved - , tcPluginNewCts = new - } - ) - | null insols - = pure $ GHC.TcPluginOk solved new - | null solved && null new - = pure $ GHC.TcPluginContradiction insols - | otherwise - = do - evBinds <- getEvBindsTcPluginM - unsafeTcPluginTcM . runTcSWithEvBinds evBinds $ do - unless doingGivens $ traverse_ ( uncurry setEv ) solved - --updInertCans (removeInertCts $ fmap snd solved) -- These don't do anything, as the inert set and work list - --emitWork new -- are confined to this run of the plugin. - pure $ GHC.TcPluginContradiction insols - where - setEv :: EvTerm -> Ct -> TcS () - setEv ev ( ctEvidence -> CtWanted { ctev_dest = dest } ) - = setWantedEvTerm dest ev - setEv _ _ - = pure () - -data TcPluginRewriteResult - = - -- | The plugin does not rewrite the type family application. - TcPluginNoRewrite - - -- | 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 -#if MIN_VERSION_ghc(9,0,0) - TyCon -#endif - Rewriter - --- | Emulate type-family rewriting functionality in a constraint solving plugin, --- by traversing through all the constraints and rewriting any type-family applications --- inside them. -shimRewriter :: [Ct] -> [Ct] -> [Ct] - -> Rewriters - -> ( [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginSolveResult ) - -> TcPluginM GHC.TcPluginResult -shimRewriter givens deriveds wanteds rws solver - | isNullUFM rws - = adaptSolveResult (null wanteds) =<< solver givens deriveds wanteds - | otherwise - = do - TcPluginSolveResult - { tcPluginInsolubleCts = contras - , tcPluginSolvedCts = solved - , tcPluginNewCts = new - } <- solver givens deriveds wanteds - ( rewrittenDeriveds, solvedDeriveds, newCts1 ) <- traverseCts ( reduceCt rws givens ) deriveds - ( rewrittenWanteds , solvedWanteds , newCts2 ) <- traverseCts ( reduceCt rws givens ) wanteds - adaptSolveResult (null wanteds) $ - TcPluginSolveResult - { tcPluginInsolubleCts = contras - , tcPluginSolvedCts = solved ++ solvedDeriveds ++ solvedWanteds - , tcPluginNewCts = new ++ newCts1 ++ rewrittenDeriveds ++ newCts2 ++ rewrittenWanteds - } - -reduceCt :: Rewriters - -> [Ct] - -> Ct - -> TcPluginM ( Maybe ( Ct, (EvTerm, Ct) ), [Ct] ) -reduceCt 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 givens - ( res, newCts ) <- runRewritePluginM shimRewriteEnv ( rewrite_one predTy ) - case res of - Nothing -> pure ( Nothing, newCts ) - Just ( Reduction co predTy' ) -> 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' - let - role :: Role - role = coercionRole co - cast_co :: Coercion - cast_co = mkSymCo $ case role of - Nominal -> mkSubCo co - _ -> co - pure ( Just - ( mkNonCanonical ctEv' - , ( evCast ( ctEvExpr ctEv' ) cast_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 ty - | Just ty' <- rewriterView ty -- See Note [Rewriting synonyms] - = rewrite_one ty' - -rewrite_one xi@(LitTy {}) - = do { role <- getRole - ; return $ mkReflRedn role xi } - -rewrite_one (TyVarTy tv) - = rewriteTyVar tv - -rewrite_one (AppTy ty1 ty2) - = rewrite_app_tys ty1 [ty2] - -rewrite_one (TyConApp tc tys) - | isTypeFamilyTyCon tc - = rewrite_fam_app tc tys - - | otherwise - = rewrite_ty_con_app tc tys - -rewrite_one - (FunTy -#if MIN_VERSION_ghc(8,10,0) - vis -#endif -#if MIN_VERSION_ghc(9,0,0) - mult -#endif - ty1 - ty2 - ) - = do { arg_redn <- rewrite_one ty1 - ; res_redn <- rewrite_one ty2 -#if MIN_VERSION_ghc(9,0,0) - ; w_redn <- setEqRel NomEq $ rewrite_one mult -#endif - ; role <- getRole - ; return $ - mkFunRedn - role -#if MIN_VERSION_ghc(8,10,0) - vis -#endif -#if MIN_VERSION_ghc(9,0,0) - w_redn -#endif - arg_redn - res_redn - } - -rewrite_one ty@(ForAllTy {}) - = do { let (bndrs, rho) = tcSplitForAllTyVarBinders ty - ; redn <- rewrite_one rho - ; return $ mkHomoForAllRedn bndrs redn } - -rewrite_one (CastTy ty g) - = do { redn <- rewrite_one ty - ; g' <- rewrite_co g - ; role <- getRole - ; return $ mkCastRedn1 role ty g' redn } - -rewrite_one (CoercionTy co) - = do { co' <- rewrite_co co - ; role <- getRole - ; return $ mkReflCoRedn role co' } - -rewrite_reduction :: Reduction -> RewriteM Reduction -rewrite_reduction (Reduction co xi) = do - redn <- bumpDepth $ rewrite_one xi - pure $ co `mkTransRedn` redn - -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 { redn <- rewrite_one fun_ty - ; rewrite_app_ty_args redn arg_tys } - -rewrite_app_ty_args :: Reduction -> [Type] -> RewriteM Reduction -rewrite_app_ty_args redn [] - = return redn -rewrite_app_ty_args fun_redn@(Reduction fun_co fun_xi) arg_tys - = do { het_redn <- case tcSplitTyConApp_maybe fun_xi of - Just (tc, xis) -> - do { let tc_roles = tyConRolesRepresentational tc - arg_roles = dropList xis tc_roles - ; ArgsReductions (Reductions arg_cos arg_xis) 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 -> mkAppCos fun_co (map mkNomReflCo arg_tys) - `mkTcTransCo` - mkTcTyConAppCo Representational tc - (zipWith mkReflCo tc_roles xis ++ arg_cos) - - ; return $ - mkHetReduction - (mkReduction app_co app_xi ) - kind_co } - Nothing -> - do { ArgsReductions redns kind_co - <- rewrite_vector (tcTypeKind fun_xi) (repeat Nominal) arg_tys - ; return $ mkHetReduction (mkAppRedns fun_redn redns) kind_co } - - ; role <- getRole - ; return (homogeniseHetRedn role het_redn) } - -{-# INLINE rewrite_args_tc #-} -rewrite_args_tc :: TyCon -> Maybe [Role] -> [Type] -> RewriteM ArgsReductions -rewrite_args_tc tc = rewrite_args all_bndrs any_named_bndrs inner_ki emptyVarSet - -- NB: TyCon kinds are always closed - where - -- There are many bang patterns in here. It's been observed that they - -- greatly improve performance of an optimized build. - -- The T9872 test cases are good witnesses of this fact. - - (bndrs, named) - = ty_con_binders_ty_binders' (tyConBinders tc) - -- it's possible that the result kind has arrows (for, e.g., a type family) - -- so we must split it - (inner_bndrs, inner_ki, inner_named) = split_pi_tys' (tyConResKind tc) - !all_bndrs = bndrs `chkAppend` inner_bndrs - !any_named_bndrs = named || inner_named - -- NB: Those bangs there drop allocations in T9872{a,c,d} by 8%. - -rewrite_fam_app :: TyCon -> [Type] -> RewriteM Reduction -rewrite_fam_app tc tys = do - let (tys1, tys_rest) = splitAt (tyConArity tc) tys - redn <- rewrite_exact_fam_app tc tys1 - rewrite_app_ty_args redn 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 - ArgsReductions (Reductions cos xis) 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 cos - homogenise :: Reduction -> Reduction - homogenise redn - = homogeniseHetRedn role - $ mkHetReduction - (args_co `mkTransRedn` redn) - kind_co - give_up :: Reduction - give_up = homogenise $ mkReflRedn role (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) - , let - redn :: Reduction - redn = Reduction (mkSymCo co) xi -- inerts use a different orientation in GHC 9.0 and 9.2 - -> finish True (homogenise $ downgradeRedn role' inert_role redn) - where - inert_role = eqRelRole inert_eq_rel - role' = eqRelRole eq_rel - _ -> do - result3 <- try_to_reduce tc xis mbRewriter - case result3 of - Just redn -> finish True (homogenise redn) - _ -> return give_up - where - finish :: Bool -> Reduction -> RewriteM Reduction - finish use_cache (Reduction co xi) = do - Reduction fully_co fully <- bumpDepth $ rewrite_one xi - let final_redn@(Reduction final_co final_xi) = Reduction (fully_co `mkTcTransCo` co) fully - eq_rel <- getEqRel - flavour <- getFlavour - when (use_cache && eq_rel == NomEq && flavour /= Derived) $ - liftTcS $ - extendFamAppCache tc tys - ( mkSymCo final_co, final_xi ) -- different orientation in GHC 9.0 and 9.2 -#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 tys - , liftTcS $ mkRed <$> lookupFamAppCache tc tys - , liftTcS $ mkRed <$> matchFam tc tys ] - forM result downgrade - where - mkRed :: Maybe (Coercion, Type) -> Maybe Reduction - mkRed = fmap $ uncurry Reduction - downgrade :: Reduction -> RewriteM Reduction - downgrade redn@(Reduction co xi) = do - eq_rel <- getEqRel - case eq_rel of - NomEq -> return redn - ReprEq -> return $ Reduction (mkSubCo co) xi - -runTcPluginRewriter :: Maybe Rewriter - -> [Type] - -> RewriteM (Maybe Reduction) -runTcPluginRewriter mbRewriter 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 ( Just redn ) wanteds - TcPluginNoRewrite { } - -> addRewriting Nothing [] - -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 - ; ArgsReductions redns kind_co <- rewrite_args_tc tc m_roles tys - ; let tyconapp_redn - = mkHetReduction - (mkTyConAppRedn role tc redns) - kind_co - ; return $ homogeniseHetRedn role tyconapp_redn } - -rewrite_co :: Coercion -> RewriteM Coercion -rewrite_co co = liftTcS $ zonkCo 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 redn -> rewrite_reduction redn - RTRNotFollowed -> do - tv' <- liftTcS $ updateTyVarKindM zonkTcType tv - role <- getRole - let ty' = mkTyVarTy tv' - pure $ mkReflRedn role ty' - -data RewriteTvResult - = RTRNotFollowed - | RTRFollowed !Reduction - -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 $ mkReflRedn 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 rewriting_co1 = ctEvCoercion ctev - rewriting_co = case (ct_eq_rel, eq_rel) of - (ReprEq, _rel) -> rewriting_co1 - (NomEq, NomEq) -> rewriting_co1 - (NomEq, ReprEq) -> mkSubCo rewriting_co1 - return $ RTRFollowed $ mkReduction rewriting_co rhs_ty - _other -> return RTRNotFollowed - -rewrite_vector :: Kind - -> [Role] - -> [Type] - -> RewriteM ArgsReductions -rewrite_vector ki roles tys - = do { eq_rel <- getEqRel - ; let mb_roles = case eq_rel of { NomEq -> Nothing; ReprEq -> Just roles } - ; rewrite_args bndrs any_named_bndrs inner_ki fvs mb_roles tys - } - where - (bndrs, inner_ki, any_named_bndrs) = split_pi_tys' ki - fvs = tyCoVarsOfType ki -{-# INLINE rewrite_vector #-} - -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 -#if MIN_VERSION_ghc(8,10,0) - af -#endif -#if MIN_VERSION_ghc(9,0,0) - w -#endif - arg - res - ) = - let !(bs, ty', named) = split res res - in ( Anon -#if MIN_VERSION_ghc(8,10,0) - af -#endif -#if MIN_VERSION_ghc(9,0,0) - (mkScaled w arg) -#else - arg -#endif - : 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 -#if MIN_VERSION_ghc(8,10,0) - af -#endif - ) - ) (bndrs, n) - = (Anon -#if MIN_VERSION_ghc(8,10,0) - af -#endif - ( -#if MIN_VERSION_ghc(9,0,0) - tymult -#endif - (tyVarKind tv) - ) - : bndrs - , n) - {-# INLINE go #-} -{-# INLINE ty_con_binders_ty_binders' #-} - -{-# INLINE rewrite_args #-} -rewrite_args :: [TyCoBinder] -> Bool - -> Kind -> TcTyCoVarSet - -> Maybe [Role] -> [Type] - -> RewriteM ArgsReductions -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 ArgsReductions -rewrite_args_fast orig_tys - = fmap finish (iterate orig_tys) - where - - iterate :: [Type] -> RewriteM Reductions - iterate (ty : tys) = do - Reduction co xi <- rewrite_one ty - Reductions cos xis <- iterate tys - pure $ Reductions (co : cos) (xi : xis) - iterate [] = pure $ Reductions [] [] - - {-# INLINE finish #-} - finish :: Reductions -> ArgsReductions - finish redns = ArgsReductions redns MRefl - -{-# INLINE rewrite_args_slow #-} -rewrite_args_slow :: [TyCoBinder] -> Kind -> TcTyCoVarSet - -> [Role] -> [Type] - -> RewriteM ArgsReductions -rewrite_args_slow binders inner_ki fvs roles tys - = do { rewritten_args <- zipWith3M fl (map isNamedBinder binders ++ repeat True) - roles tys - ; return $ simplifyArgsWorker binders inner_ki fvs roles rewritten_args } - where - {-# INLINE fl #-} - fl :: Bool -- must we ensure to produce a real coercion here? - -- see comment at top of function - -> Role -> Type -> RewriteM Reduction - fl True r ty = noBogusCoercions $ fl1 r ty - fl False r ty = 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 - ; return $ mkReflRedn 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 - } - -data ShimRewriteEnv - = ShimRewriteEnv - { rewriters :: !Rewriters - , rewriteEnv :: !RewriteEnv - , rewriteGivens :: ![ Ct ] - } - -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 { rewrittenCts, reductionOccurred } ) - <- unsafeTcPluginTcM - $ runTcSWithEvBinds evBindsVar - $ run env ( RewriteState [] NoReduction ) - let - mb_a = case reductionOccurred of - NoReduction -> Nothing - DidReduce -> Just a - pure ( mb_a, rewrittenCts ) - -addRewriting :: Maybe Reduction -> [Ct] -> RewriteM ( Maybe Reduction ) -addRewriting mbRedn newCts = RewriteM \ _ ( RewriteState cts s ) -> - let - s' :: ReduceQ - s' - | Just _ <- mbRedn - = DidReduce - | otherwise - = s - in pure ( mbRedn , RewriteState ( cts <> newCts ) s' ) - -getRewriters :: RewriteM Rewriters -getRewriters = RewriteM \ env s -> pure ( rewriters 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 +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE DerivingVia #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# 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 + ( Reduction(..), mkReduction + , TcPluginSolveResult(TcPluginContradiction, TcPluginOk, ..), TcPluginRewriteResult(..) + , RewriteEnv(..) + , shimRewriter + ) + where + +-- base +import Prelude + hiding ( Floating(cos), iterate ) +import Control.Monad + ( forM, unless, when ) +import Data.Foldable + ( traverse_ +#if !MIN_VERSION_ghc(9,2,0) + , foldlM +#endif + ) +#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 + ( coercionRole + , mkReflCo, mkSymCo + , mkAppCos, mkNomReflCo, mkSubCo + , mkTyConAppCo, tyConRolesX + , tyConRolesRepresentational + ) +import GHC.Core.Predicate + ( EqRel(..), eqRelRole ) +import GHC.Core.TyCo.Rep + ( Type(..), Kind, Coercion(..), MCoercion(..), TyCoBinder(..) + , 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 , mkTyConApp +#if MIN_VERSION_ghc(9,0,0) + , mkScaled, tymult +#endif + , coreView, tyVarKind + ) +#if MIN_VERSION_ghc(9,2,0) +import GHC.Data.Maybe + ( firstJustsM ) +#endif +import GHC.Tc.Plugin + ( newWanted, newDerived ) +import GHC.Tc.Solver.Monad + ( TcS + , zonkCo, zonkTcType + , isFilledMetaTyVar_maybe + , getInertEqs + , checkReductionDepth + , matchFam + , runTcPluginTcS, runTcSWithEvBinds + , traceTcS + , setWantedEvTerm +#if MIN_VERSION_ghc(9,2,0) + , lookupFamAppCache, lookupFamAppInert, extendFamAppCache + , pattern EqualCtList +#else + , lookupFlatCache, extendFlatCache +#endif + ) +import GHC.Tc.Types + ( TcPluginM + , unsafeTcPluginTcM, getEvBindsTcPluginM + ) +import qualified GHC.Tc.Types as GHC + ( TcPluginResult(..) ) +import GHC.Tc.Types.Constraint + ( Ct(..), CtEvidence(..) + , CtLoc, CtFlavour(..), CtFlavourRole, ShadowInfo(..) +#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, mkTcTransCo , mkTcTyConAppCo + ) +import GHC.Tc.Utils.TcType + ( TcTyCoVarSet +#if MIN_VERSION_ghc(9,2,0) + , tcSplitForAllTyVarBinders +#else + , tcSplitForAllVarBndrs +#endif + , tcSplitTyConApp_maybe + , tcTypeKind + , tyCoVarsOfType + ) +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(..), SDoc, empty ) + +-- ghc-tcplugin-api +import GHC.TcPlugin.API.Internal.Shim.Reduction + +-------------------------------------------------------------------------------- + +-- | The type-family rewriting environment. +data RewriteEnv + = FE { fe_loc :: !CtLoc + , fe_flavour :: !CtFlavour + , fe_eq_rel :: !EqRel + } + +-- | Result of running a solver plugin. +data TcPluginSolveResult + = TcPluginSolveResult + { -- | Insoluble constraints found by the plugin. + -- + -- These constraints will be added to the inert set, + -- and reported as insoluble to the user. + tcPluginInsolubleCts :: [Ct] + -- | Solved constraints, together with their evidence. + -- + -- These are removed from the inert set, and the + -- evidence for them is recorded. + , tcPluginSolvedCts :: [(EvTerm, Ct)] + -- | New constraints that the plugin wishes to emit. + -- + -- These will be added to the work list. + , tcPluginNewCts :: [Ct] + } + +-- | The plugin found a contradiction. +-- The returned constraints are removed from the inert set, +-- and recorded as insoluble. +-- +-- The returned list of constraints should never be empty. +pattern TcPluginContradiction :: [Ct] -> TcPluginSolveResult +pattern TcPluginContradiction insols + = TcPluginSolveResult + { tcPluginInsolubleCts = insols + , tcPluginSolvedCts = [] + , tcPluginNewCts = [] } + +-- | The plugin has not found any contradictions, +-- +-- The first field is for constraints that were solved. +-- The second field contains new work, that should be processed by +-- the constraint solver. +pattern TcPluginOk :: [(EvTerm, Ct)] -> [Ct] -> TcPluginSolveResult +pattern TcPluginOk solved new + = TcPluginSolveResult + { tcPluginInsolubleCts = [] + , tcPluginSolvedCts = solved + , tcPluginNewCts = new } + +-- The 'TcPluginSolveResult' datatype changed in GHC 9.4, +-- allowing users to return solved and new constraints even in case of +-- a contradiction. +-- +-- This function simply drops the solved and new constraints on older versions, +-- although it does at least still bind the evidence in case of solved Wanteds. +adaptSolveResult :: Bool -> TcPluginSolveResult -> TcPluginM GHC.TcPluginResult +adaptSolveResult doingGivens + ( TcPluginSolveResult + { tcPluginInsolubleCts = insols + , tcPluginSolvedCts = solved + , tcPluginNewCts = new + } + ) + | null insols + = pure $ GHC.TcPluginOk solved new + | null solved && null new + = pure $ GHC.TcPluginContradiction insols + | otherwise + = do + evBinds <- getEvBindsTcPluginM + unsafeTcPluginTcM . runTcSWithEvBinds evBinds $ do + unless doingGivens $ traverse_ ( uncurry setEv ) solved + --updInertCans (removeInertCts $ fmap snd solved) -- These don't do anything, as the inert set and work list + --emitWork new -- are confined to this run of the plugin. + pure $ GHC.TcPluginContradiction insols + where + setEv :: EvTerm -> Ct -> TcS () + setEv ev ( ctEvidence -> CtWanted { ctev_dest = dest } ) + = setWantedEvTerm dest ev + setEv _ _ + = pure () + +data TcPluginRewriteResult + = + -- | The plugin does not rewrite the type family application. + TcPluginNoRewrite + + -- | 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 +#if MIN_VERSION_ghc(9,0,0) + TyCon +#endif + Rewriter + +-- | Emulate type-family rewriting functionality in a constraint solving plugin, +-- by traversing through all the constraints and rewriting any type-family applications +-- inside them. +shimRewriter :: [Ct] -> [Ct] -> [Ct] + -> Rewriters + -> ( [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginSolveResult ) + -> TcPluginM GHC.TcPluginResult +shimRewriter givens deriveds wanteds rws solver + | isNullUFM rws + = adaptSolveResult (null wanteds) =<< solver givens deriveds wanteds + | otherwise + = do + TcPluginSolveResult + { tcPluginInsolubleCts = contras + , tcPluginSolvedCts = solved + , tcPluginNewCts = new + } <- solver givens deriveds wanteds + ( rewrittenDeriveds, solvedDeriveds, newCts1 ) <- traverseCts ( reduceCt rws givens ) deriveds + ( rewrittenWanteds , solvedWanteds , newCts2 ) <- traverseCts ( reduceCt rws givens ) wanteds + adaptSolveResult (null wanteds) $ + TcPluginSolveResult + { tcPluginInsolubleCts = contras + , tcPluginSolvedCts = solved ++ solvedDeriveds ++ solvedWanteds + , tcPluginNewCts = new ++ newCts1 ++ rewrittenDeriveds ++ newCts2 ++ rewrittenWanteds + } + +reduceCt :: Rewriters + -> [Ct] + -> Ct + -> TcPluginM ( Maybe ( Ct, (EvTerm, Ct) ), [Ct] ) +reduceCt 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 givens + ( res, newCts ) <- runRewritePluginM shimRewriteEnv ( rewrite_one predTy ) + case res of + Nothing -> pure ( Nothing, newCts ) + Just ( Reduction co predTy' ) -> 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' + let + role :: Role + role = coercionRole co + cast_co :: Coercion + cast_co = mkSymCo $ case role of + Nominal -> mkSubCo co + _ -> co + pure ( Just + ( mkNonCanonical ctEv' + , ( evCast ( ctEvExpr ctEv' ) cast_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 ty + | Just ty' <- rewriterView ty -- See Note [Rewriting synonyms] + = rewrite_one ty' + +rewrite_one xi@(LitTy {}) + = do { role <- getRole + ; return $ mkReflRedn role xi } + +rewrite_one (TyVarTy tv) + = rewriteTyVar tv + +rewrite_one (AppTy ty1 ty2) + = rewrite_app_tys ty1 [ty2] + +rewrite_one (TyConApp tc tys) + | isTypeFamilyTyCon tc + = rewrite_fam_app tc tys + + | otherwise + = rewrite_ty_con_app tc tys + +rewrite_one + (FunTy +#if MIN_VERSION_ghc(8,10,0) + vis +#endif +#if MIN_VERSION_ghc(9,0,0) + mult +#endif + ty1 + ty2 + ) + = do { arg_redn <- rewrite_one ty1 + ; res_redn <- rewrite_one ty2 +#if MIN_VERSION_ghc(9,0,0) + ; w_redn <- setEqRel NomEq $ rewrite_one mult +#endif + ; role <- getRole + ; return $ + mkFunRedn + role +#if MIN_VERSION_ghc(8,10,0) + vis +#endif +#if MIN_VERSION_ghc(9,0,0) + w_redn +#endif + arg_redn + res_redn + } + +rewrite_one ty@(ForAllTy {}) + = do { let (bndrs, rho) = tcSplitForAllTyVarBinders ty + ; redn <- rewrite_one rho + ; return $ mkHomoForAllRedn bndrs redn } + +rewrite_one (CastTy ty g) + = do { redn <- rewrite_one ty + ; g' <- rewrite_co g + ; role <- getRole + ; return $ mkCastRedn1 role ty g' redn } + +rewrite_one (CoercionTy co) + = do { co' <- rewrite_co co + ; role <- getRole + ; return $ mkReflCoRedn role co' } + +rewrite_reduction :: Reduction -> RewriteM Reduction +rewrite_reduction (Reduction co xi) = do + redn <- bumpDepth $ rewrite_one xi + pure $ co `mkTransRedn` redn + +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 { redn <- rewrite_one fun_ty + ; rewrite_app_ty_args redn arg_tys } + +rewrite_app_ty_args :: Reduction -> [Type] -> RewriteM Reduction +rewrite_app_ty_args redn [] + = return redn +rewrite_app_ty_args fun_redn@(Reduction fun_co fun_xi) arg_tys + = do { het_redn <- case tcSplitTyConApp_maybe fun_xi of + Just (tc, xis) -> + do { let tc_roles = tyConRolesRepresentational tc + arg_roles = dropList xis tc_roles + ; ArgsReductions (Reductions arg_cos arg_xis) 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 -> mkAppCos fun_co (map mkNomReflCo arg_tys) + `mkTcTransCo` + mkTcTyConAppCo Representational tc + (zipWith mkReflCo tc_roles xis ++ arg_cos) + + ; return $ + mkHetReduction + (mkReduction app_co app_xi ) + kind_co } + Nothing -> + do { ArgsReductions redns kind_co + <- rewrite_vector (tcTypeKind fun_xi) (repeat Nominal) arg_tys + ; return $ mkHetReduction (mkAppRedns fun_redn redns) kind_co } + + ; role <- getRole + ; return (homogeniseHetRedn role het_redn) } + +{-# INLINE rewrite_args_tc #-} +rewrite_args_tc :: TyCon -> Maybe [Role] -> [Type] -> RewriteM ArgsReductions +rewrite_args_tc tc = rewrite_args all_bndrs any_named_bndrs inner_ki emptyVarSet + -- NB: TyCon kinds are always closed + where + -- There are many bang patterns in here. It's been observed that they + -- greatly improve performance of an optimized build. + -- The T9872 test cases are good witnesses of this fact. + + (bndrs, named) + = ty_con_binders_ty_binders' (tyConBinders tc) + -- it's possible that the result kind has arrows (for, e.g., a type family) + -- so we must split it + (inner_bndrs, inner_ki, inner_named) = split_pi_tys' (tyConResKind tc) + !all_bndrs = bndrs `chkAppend` inner_bndrs + !any_named_bndrs = named || inner_named + -- NB: Those bangs there drop allocations in T9872{a,c,d} by 8%. + +rewrite_fam_app :: TyCon -> [Type] -> RewriteM Reduction +rewrite_fam_app tc tys = do + let (tys1, tys_rest) = splitAt (tyConArity tc) tys + redn <- rewrite_exact_fam_app tc tys1 + rewrite_app_ty_args redn 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 + ArgsReductions (Reductions cos xis) 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 cos + homogenise :: Reduction -> Reduction + homogenise redn + = homogeniseHetRedn role + $ mkHetReduction + (args_co `mkTransRedn` redn) + kind_co + give_up :: Reduction + give_up = homogenise $ mkReflRedn role (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) + , let + redn :: Reduction + redn = Reduction (mkSymCo co) xi -- inerts use a different orientation in GHC 9.0 and 9.2 + -> finish True (homogenise $ downgradeRedn role' inert_role redn) + where + inert_role = eqRelRole inert_eq_rel + role' = eqRelRole eq_rel + _ -> do + result3 <- try_to_reduce tc xis mbRewriter + case result3 of + Just redn -> finish True (homogenise redn) + _ -> return give_up + where + finish :: Bool -> Reduction -> RewriteM Reduction + finish use_cache (Reduction co xi) = do + Reduction fully_co fully <- bumpDepth $ rewrite_one xi + let final_redn@(Reduction final_co final_xi) = Reduction (co `mkTcTransCo` fully_co) fully + eq_rel <- getEqRel + flavour <- getFlavour + when (use_cache && eq_rel == NomEq && flavour /= Derived) $ + liftTcS $ + extendFamAppCache tc tys + ( mkSymCo final_co, final_xi ) -- different orientation in GHC 9.0 and 9.2 +#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 tys + , liftTcS $ mkRed <$> lookupFamAppCache tc tys + , liftTcS $ mkRed <$> matchFam tc tys ] + forM result downgrade + where + mkRed :: Maybe (Coercion, Type) -> Maybe Reduction + mkRed = fmap $ \ (co, ty) -> Reduction (mkSymCo co) ty + downgrade :: Reduction -> RewriteM Reduction + downgrade redn@(Reduction co xi) = do + eq_rel <- getEqRel + case eq_rel of + NomEq -> return redn + ReprEq -> return $ Reduction (mkSubCo co) xi + +runTcPluginRewriter :: Maybe Rewriter + -> [Type] + -> RewriteM (Maybe Reduction) +runTcPluginRewriter mbRewriter 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 ( Just redn ) wanteds + TcPluginNoRewrite { } + -> addRewriting Nothing [] + +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 + ; ArgsReductions redns kind_co <- rewrite_args_tc tc m_roles tys + ; let tyconapp_redn + = mkHetReduction + (mkTyConAppRedn role tc redns) + kind_co + ; return $ homogeniseHetRedn role tyconapp_redn } + +rewrite_co :: Coercion -> RewriteM Coercion +rewrite_co co = liftTcS $ zonkCo 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 redn -> rewrite_reduction redn + RTRNotFollowed -> do + tv' <- liftTcS $ updateTyVarKindM zonkTcType tv + role <- getRole + let ty' = mkTyVarTy tv' + pure $ mkReflRedn role ty' + +data RewriteTvResult + = RTRNotFollowed + | RTRFollowed !Reduction + +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 $ mkReflRedn 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 rewriting_co1 = ctEvCoercion ctev + rewriting_co = case (ct_eq_rel, eq_rel) of + (ReprEq, _rel) -> rewriting_co1 + (NomEq, NomEq) -> rewriting_co1 + (NomEq, ReprEq) -> mkSubCo rewriting_co1 + return $ RTRFollowed $ mkReduction rewriting_co rhs_ty + _other -> return RTRNotFollowed + +rewrite_vector :: Kind + -> [Role] + -> [Type] + -> RewriteM ArgsReductions +rewrite_vector ki roles tys + = do { eq_rel <- getEqRel + ; let mb_roles = case eq_rel of { NomEq -> Nothing; ReprEq -> Just roles } + ; rewrite_args bndrs any_named_bndrs inner_ki fvs mb_roles tys + } + where + (bndrs, inner_ki, any_named_bndrs) = split_pi_tys' ki + fvs = tyCoVarsOfType ki +{-# INLINE rewrite_vector #-} + +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 +#if MIN_VERSION_ghc(8,10,0) + af +#endif +#if MIN_VERSION_ghc(9,0,0) + w +#endif + arg + res + ) = + let !(bs, ty', named) = split res res + in ( Anon +#if MIN_VERSION_ghc(8,10,0) + af +#endif +#if MIN_VERSION_ghc(9,0,0) + (mkScaled w arg) +#else + arg +#endif + : 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 +#if MIN_VERSION_ghc(8,10,0) + af +#endif + ) + ) (bndrs, n) + = (Anon +#if MIN_VERSION_ghc(8,10,0) + af +#endif + ( +#if MIN_VERSION_ghc(9,0,0) + tymult +#endif + (tyVarKind tv) + ) + : bndrs + , n) + {-# INLINE go #-} +{-# INLINE ty_con_binders_ty_binders' #-} + +{-# INLINE rewrite_args #-} +rewrite_args :: [TyCoBinder] -> Bool + -> Kind -> TcTyCoVarSet + -> Maybe [Role] -> [Type] + -> RewriteM ArgsReductions +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 ArgsReductions +rewrite_args_fast orig_tys + = fmap finish (iterate orig_tys) + where + + iterate :: [Type] -> RewriteM Reductions + iterate (ty : tys) = do + Reduction co xi <- rewrite_one ty + Reductions cos xis <- iterate tys + pure $ Reductions (co : cos) (xi : xis) + iterate [] = pure $ Reductions [] [] + + {-# INLINE finish #-} + finish :: Reductions -> ArgsReductions + finish redns = ArgsReductions redns MRefl + +{-# INLINE rewrite_args_slow #-} +rewrite_args_slow :: [TyCoBinder] -> Kind -> TcTyCoVarSet + -> [Role] -> [Type] + -> RewriteM ArgsReductions +rewrite_args_slow binders inner_ki fvs roles tys + = do { rewritten_args <- zipWith3M fl (map isNamedBinder binders ++ repeat True) + roles tys + ; return $ simplifyArgsWorker binders inner_ki fvs roles rewritten_args } + where + {-# INLINE fl #-} + fl :: Bool -- must we ensure to produce a real coercion here? + -- see comment at top of function + -> Role -> Type -> RewriteM Reduction + fl True r ty = noBogusCoercions $ fl1 r ty + fl False r ty = 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 + ; return $ mkReflRedn 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 + } + +data ShimRewriteEnv + = ShimRewriteEnv + { rewriters :: !Rewriters + , rewriteEnv :: !RewriteEnv + , rewriteGivens :: ![ Ct ] + } + +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 { rewrittenCts, reductionOccurred } ) + <- unsafeTcPluginTcM + $ runTcSWithEvBinds evBindsVar + $ run env ( RewriteState [] NoReduction ) + let + mb_a = case reductionOccurred of + NoReduction -> Nothing + DidReduce -> Just a + pure ( mb_a, rewrittenCts ) + +addRewriting :: Maybe Reduction -> [Ct] -> RewriteM ( Maybe Reduction ) +addRewriting mbRedn newCts = RewriteM \ _ ( RewriteState cts s ) -> + let + s' :: ReduceQ + s' + | Just _ <- mbRedn + = DidReduce + | otherwise + = s + in pure ( mbRedn , RewriteState ( cts <> newCts ) s' ) + +getRewriters :: RewriteM Rewriters +getRewriters = RewriteM \ env s -> pure ( rewriters 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 diff --git a/src/GHC/TcPlugin/API/Internal/Shim/Reduction.hs b/src/GHC/TcPlugin/API/Internal/Shim/Reduction.hs --- a/src/GHC/TcPlugin/API/Internal/Shim/Reduction.hs +++ b/src/GHC/TcPlugin/API/Internal/Shim/Reduction.hs @@ -1,604 +1,604 @@ -{-# LANGUAGE BangPatterns #-} -{-# LANGUAGE CPP #-} - -module GHC.TcPlugin.API.Internal.Shim.Reduction where - --- base -import Prelude - hiding (Floating(cos)) - --- ghc -import GHC.Core.Class - ( Class(classTyCon) ) -import GHC.Core.Coercion - ( Coercion, CoercionN, MCoercion(..) - , Role(Nominal), LiftingContext -#if MIN_VERSION_ghc(9,0,0) - , castCoercionKind1, castCoercionKind2 - , coercionLKind, coercionRKind -#else - , mkCoherenceLeftCo, mkNomReflCo -#endif - , coercionKind -#if MIN_VERSION_ghc(8,10,0) - , coToMCo -#else - , isReflCo -#endif - , decomposePiCos, downgradeRole - , liftCoSubst, emptyLiftingContext, extendLiftingContextAndInScope, zapLiftingContext - , mkAppCo, mkAppCos - , mkCoherenceRightCo - , mkForAllCo, mkFunCo - , mkGReflLeftCo, mkGReflRightCo - , mkHomoForAllCos, mkProofIrrelCo - , mkReflCo, mkSubCo, mkSymCo, mkTransCo, mkTyConAppCo - ) -import GHC.Core.Predicate - ( mkClassPred ) -import GHC.Core.TyCo.Rep - ( TyCoBinder, mkFunTy -#if !MIN_VERSION_ghc(9,0,0) - , Coercion(..) -#endif - ) -import GHC.Core.TyCon - ( TyCon ) -import GHC.Core.Type - ( ArgFlag, Kind, Type, TyVar, TyVarBinder -#if MIN_VERSION_ghc(8,10,0) - , AnonArgFlag -#endif - , binderVars - , mkAppTy, mkAppTys, mkCastTy, mkCoercionTy, mkForAllTy, mkForAllTys - , mkTyConApp, mkPiTys - , noFreeVarsOfType - , splitPiTys, tyCoBinderType, tyCoBinderVar_maybe - ) -import GHC.Data.Pair - ( Pair(Pair) ) -import GHC.Types.Var - ( setTyVarKind ) -import GHC.Types.Var.Env - ( mkInScopeSet ) -import GHC.Types.Var.Set - ( TyCoVarSet ) -import GHC.Utils.Outputable - ( Outputable(ppr), (<+>) - , braces, text, vcat - ) - --------------------------------------------------------------------------------- - - --- | A 'Reduction' is the result of an operation that rewrites a type @ty_in@. --- The 'Reduction' includes the rewritten type @ty_out@ and a 'Coercion' @co@ --- such that @co :: ty_in ~ ty_out@, where the role of the coercion is determined --- by the context. That is, the LHS type of the coercion is the original type --- @ty_in@, while its RHS type is the rewritten type @ty_out@. --- --- A Reduction is always homogeneous, unless it is wrapped inside a 'HetReduction', --- which separately stores the kind coercion. -data Reduction = - Reduction - { reductionCoercion :: Coercion - , reductionReducedType :: !Type - } - --- | Stores a heterogeneous reduction. --- --- The stored kind coercion must relate the kinds of the --- stored reduction. That is, in @HetReduction (Reduction co xi) kco@, --- we must have: --- --- > co :: ty ~ xi --- > kco :: typeKind ty ~ typeKind xi -data HetReduction = - HetReduction - Reduction - MCoercion - --- | Create a heterogeneous reduction. --- --- Pre-condition: the provided kind coercion (second argument) --- relates the kinds of the stored reduction. --- That is, if the coercion stored in the 'Reduction' is of the form --- --- > co :: ty ~ xi --- --- Then the kind coercion supplied must be of the form: --- --- > kco :: typeKind ty ~ typeKind xi -mkHetReduction :: Reduction -- ^ heterogeneous reduction - -> MCoercion -- ^ kind coercion - -> HetReduction -mkHetReduction redn mco = HetReduction redn mco -{-# INLINE mkHetReduction #-} - --- | Homogenise a heterogeneous reduction. --- --- Given @HetReduction (Reduction co xi) kco@, with --- --- > co :: ty ~ xi --- > kco :: typeKind(ty) ~ typeKind(xi) --- --- this returns the homogeneous reduction: --- --- > hco :: ty ~ ( xi |> sym kco ) -homogeniseHetRedn :: Role -> HetReduction -> Reduction -homogeniseHetRedn role (HetReduction redn kco) - = mkCoherenceRightMRedn role redn (mkSymMCo kco) -{-# INLINE homogeniseHetRedn #-} - --- | Create a 'Reduction' from a pair of a 'Coercion' and a 'Type. --- --- Pre-condition: the RHS type of the coercion matches the provided type --- (perhaps up to zonking). --- --- Use 'coercionRedn' when you only have the coercion. -mkReduction :: Coercion -> Type -> Reduction -mkReduction co ty = Reduction co ty -{-# INLINE mkReduction #-} - -instance Outputable Reduction where - ppr redn = - braces $ vcat - [ text "reductionOriginalType:" <+> ppr (reductionOriginalType redn) - , text " reductionReducedType:" <+> ppr (reductionReducedType redn) - , text " reductionCoercion:" <+> ppr (reductionCoercion redn) - ] - --- | A 'Reduction' in which the 'Coercion' has 'Nominal' role. -type ReductionN = Reduction - --- | A 'Reduction' in which the 'Coercion' has 'Representational' role. -type ReductionR = Reduction - --- | Get the original, unreduced type corresponding to a 'Reduction'. --- --- This is obtained by computing the LHS kind of the stored coercion, --- which may be slow. -reductionOriginalType :: Reduction -> Type -reductionOriginalType = coercionLKind . reductionCoercion -{-# INLINE reductionOriginalType #-} - --- | Turn a 'Coercion' into a 'Reduction' --- by inspecting the RHS type of the coercion. --- --- Prefer using 'mkReduction' when you already know --- the RHS type of the coercion, to avoid computing it anew. -coercionRedn :: Coercion -> Reduction -coercionRedn co = Reduction co (coercionRKind co) -{-# INLINE coercionRedn #-} - --- | Downgrade the role of the coercion stored in the 'Reduction'. -downgradeRedn :: Role -- ^ desired role - -> Role -- ^ current role - -> Reduction - -> Reduction -downgradeRedn new_role old_role redn@(Reduction co _) - = redn { reductionCoercion = downgradeRole new_role old_role co } -{-# INLINE downgradeRedn #-} - --- | Downgrade the role of the coercion stored in the 'Reduction', --- from 'Nominal' to 'Representational'. -mkSubRedn :: Reduction -> Reduction -mkSubRedn redn@(Reduction co _) = redn { reductionCoercion = mkSubCo co } -{-# INLINE mkSubRedn #-} - --- | Compose a reduction with a coercion on the left. --- --- Pre-condition: the provided coercion's RHS type must match the LHS type --- of the coercion that is stored in the reduction. -mkTransRedn :: Coercion -> Reduction -> Reduction -mkTransRedn co1 redn@(Reduction co2 _) - = redn { reductionCoercion = co1 `mkTransCo` co2 } -{-# INLINE mkTransRedn #-} - --- | The reflexive reduction. -mkReflRedn :: Role -> Type -> Reduction -mkReflRedn r ty = mkReduction (mkReflCo r ty) ty - --- | Create a 'Reduction' from a kind cast, in which --- the casted type is the rewritten type. --- --- Given @ty :: k1@, @mco :: k1 ~ k2@, --- produces the 'Reduction' @ty ~res_co~> (ty |> mco)@ --- at the given 'Role'. -mkGReflRightRedn :: Role -> Type -> CoercionN -> Reduction -mkGReflRightRedn role ty co - = mkReduction - (mkGReflRightCo role ty co) - (mkCastTy ty co) -{-# INLINE mkGReflRightRedn #-} - --- | Create a 'Reduction' from a kind cast, in which --- the casted type is the rewritten type. --- --- Given @ty :: k1@, @mco :: k1 ~ k2@, --- produces the 'Reduction' @ty ~res_co~> (ty |> mco)@ --- at the given 'Role'. -mkGReflRightMRedn :: Role -> Type -> MCoercion -> Reduction -mkGReflRightMRedn role ty mco - = mkReduction - (mkGReflRightMCo role ty mco) - (mkCastTyMCo ty mco) -{-# INLINE mkGReflRightMRedn #-} - --- | Create a 'Reduction' from a kind cast, in which --- the casted type is the original (non-rewritten) type. --- --- Given @ty :: k1@, @mco :: k1 ~ k2@, --- produces the 'Reduction' @(ty |> mco) ~res_co~> ty@ --- at the given 'Role'. -mkGReflLeftRedn :: Role -> Type -> CoercionN -> Reduction -mkGReflLeftRedn role ty co - = mkReduction - (mkGReflLeftCo role ty co) - ty -{-# INLINE mkGReflLeftRedn #-} - --- | Create a 'Reduction' from a kind cast, in which --- the casted type is the original (non-rewritten) type. --- --- Given @ty :: k1@, @mco :: k1 ~ k2@, --- produces the 'Reduction' @(ty |> mco) ~res_co~> ty@ --- at the given 'Role'. -mkGReflLeftMRedn :: Role -> Type -> MCoercion -> Reduction -mkGReflLeftMRedn role ty mco - = mkReduction - (mkGReflLeftMCo role ty mco) - ty -{-# INLINE mkGReflLeftMRedn #-} - --- | Apply a cast to the result of a 'Reduction'. --- --- Given a 'Reduction' @ty1 ~co1~> (ty2 :: k2)@ and a kind coercion @kco@ --- with LHS kind @k2@, produce a new 'Reduction' @ty1 ~co2~> ( ty2 |> kco )@ --- of the given 'Role' (which must match the role of the coercion stored --- in the 'Reduction' argument). -mkCoherenceRightRedn :: Role -> Reduction -> CoercionN -> Reduction -mkCoherenceRightRedn r (Reduction co1 ty2) kco - = mkReduction - (mkCoherenceRightCo r ty2 kco co1) - (mkCastTy ty2 kco) -{-# INLINE mkCoherenceRightRedn #-} - --- | Apply a cast to the result of a 'Reduction', using an 'MCoercionN'. --- --- Given a 'Reduction' @ty1 ~co1~> (ty2 :: k2)@ and a kind coercion @mco@ --- with LHS kind @k2@, produce a new 'Reduction' @ty1 ~co2~> ( ty2 |> mco )@ --- of the given 'Role' (which must match the role of the coercion stored --- in the 'Reduction' argument). -mkCoherenceRightMRedn :: Role -> Reduction -> MCoercion -> Reduction -mkCoherenceRightMRedn r (Reduction co1 ty2) kco - = mkReduction - (mkCoherenceRightMCo r ty2 kco co1) - (mkCastTyMCo ty2 kco) -{-# INLINE mkCoherenceRightMRedn #-} - --- | Apply a cast to a 'Reduction', casting both the original and the reduced type. --- --- Given @cast_co@ and 'Reduction' @ty ~co~> xi@, this function returns --- the 'Reduction' @(ty |> cast_co) ~return_co~> (xi |> cast_co)@ --- of the given 'Role' (which must match the role of the coercion stored --- in the 'Reduction' argument). --- --- Pre-condition: the 'Type' passed in is the same as the LHS type --- of the coercion stored in the 'Reduction'. -mkCastRedn1 :: Role - -> Type -- ^ original type - -> CoercionN -- ^ coercion to cast with - -> Reduction -- ^ rewritten type, with rewriting coercion - -> Reduction -mkCastRedn1 r ty cast_co (Reduction co xi) - -- co :: ty ~r ty' - -- return_co :: (ty |> cast_co) ~r (ty' |> cast_co) - = mkReduction - (castCoercionKind1 co r ty xi cast_co) - (mkCastTy xi cast_co) -{-# INLINE mkCastRedn1 #-} - --- | Apply casts on both sides of a 'Reduction' (of the given 'Role'). --- --- Use 'mkCastRedn1' when you want to cast both the original and reduced types --- in a 'Reduction' using the same coercion. --- --- Pre-condition: the 'Type' passed in is the same as the LHS type --- of the coercion stored in the 'Reduction'. -mkCastRedn2 :: Role - -> Type -- ^ original type - -> CoercionN -- ^ coercion to cast with on the left - -> Reduction -- ^ rewritten type, with rewriting coercion - -> CoercionN -- ^ coercion to cast with on the right - -> Reduction -mkCastRedn2 r ty cast_co (Reduction nco nty) cast_co' - = mkReduction - (castCoercionKind2 nco r ty nty cast_co cast_co') - (mkCastTy nty cast_co') -{-# INLINE mkCastRedn2 #-} - --- | Apply one 'Reduction' to another. --- --- Combines 'mkAppCo' and 'mkAppTy`. -mkAppRedn :: Reduction -> Reduction -> Reduction -mkAppRedn (Reduction co1 ty1) (Reduction co2 ty2) - = mkReduction (mkAppCo co1 co2) (mkAppTy ty1 ty2) -{-# INLINE mkAppRedn #-} - --- | Create a function 'Reduction'. --- --- Combines 'mkFunCo' and 'mkFunTy'. -mkFunRedn :: Role -#if MIN_VERSION_ghc(8,10,0) - -> AnonArgFlag -#endif -#if MIN_VERSION_ghc(9,0,0) - -> ReductionN -- ^ multiplicity reduction -#endif - -> Reduction -- ^ argument reduction - -> Reduction -- ^ result reduction - -> Reduction -mkFunRedn r -#if MIN_VERSION_ghc(8,10,0) - vis -#endif -#if MIN_VERSION_ghc(9,0,0) - (Reduction w_co w_ty) -#endif - (Reduction arg_co arg_ty) - (Reduction res_co res_ty) - = mkReduction - ( mkFunCo - r -#if MIN_VERSION_ghc(9,0,0) - w_co -#endif - arg_co - res_co - ) - ( mkFunTy -#if MIN_VERSION_ghc(8,10,0) - vis -#endif -#if MIN_VERSION_ghc(9,0,0) - w_ty -#endif - arg_ty - res_ty - ) -{-# INLINE mkFunRedn #-} - --- | Create a 'Reduction' associated to a Π type, --- from a kind 'Reduction' and a body 'Reduction'. --- --- Combines 'mkForAllCo' and 'mkForAllTy'. -mkForAllRedn :: ArgFlag - -> TyVar - -> ReductionN -- ^ kind reduction - -> Reduction -- ^ body reduction - -> Reduction -mkForAllRedn vis tv1 (Reduction h ki') (Reduction co ty) - = mkReduction - (mkForAllCo tv1 h co) - (mkForAllTy tv2 vis ty) - where - tv2 = setTyVarKind tv1 ki' -{-# INLINE mkForAllRedn #-} - --- | Create a 'Reduction' of a quantified type from a --- 'Reduction' of the body. --- --- Combines 'mkHomoForAllCos' and 'mkForAllTys'. -mkHomoForAllRedn :: [TyVarBinder] -> Reduction -> Reduction -mkHomoForAllRedn bndrs (Reduction co ty) - = mkReduction - (mkHomoForAllCos (binderVars bndrs) co) - (mkForAllTys bndrs ty) -{-# INLINE mkHomoForAllRedn #-} - --- | Create a 'Reduction' from a coercion between coercions. --- --- Combines 'mkProofIrrelCo' and 'mkCoercionTy'. -mkProofIrrelRedn :: Role -- ^ role of the created coercion, "r" - -> CoercionN -- ^ co :: phi1 ~N phi2 - -> Coercion -- ^ g1 :: phi1 - -> Coercion -- ^ g2 :: phi2 - -> Reduction -- ^ res_co :: g1 ~r g2 -mkProofIrrelRedn role co g1 g2 - = mkReduction - (mkProofIrrelCo role co g1 g2) - (mkCoercionTy g2) -{-# INLINE mkProofIrrelRedn #-} - --- | Create a reflexive 'Reduction' whose RHS is the given 'Coercion', --- with the specified 'Role'. -mkReflCoRedn :: Role -> Coercion -> Reduction -mkReflCoRedn role co - = mkReduction - (mkReflCo role co_ty) - co_ty - where - co_ty = mkCoercionTy co -{-# INLINE mkReflCoRedn #-} - --- | A collection of 'Reduction's where the coercions and the types are stored separately. --- --- Use 'unzipRedns' to obtain 'Reductions' from a list of 'Reduction's. --- --- This datatype is used in 'mkAppRedns', 'mkClassPredRedns' and 'mkTyConAppRedn', --- which expect separate types and coercions. --- --- Invariant: the two stored lists are of the same length, --- and the RHS type of each coercion is the corresponding type. -data Reductions = Reductions [Coercion] [Type] - --- | Create 'Reductions' from individual lists of coercions and types. --- --- The lists should be of the same length, and the RHS type of each coercion --- should match the specified type in the other list. -mkReductions :: [Coercion] -> [Type] -> Reductions -mkReductions cos tys = Reductions cos tys -{-# INLINE mkReductions #-} - --- | Combines 'mkAppCos' and 'mkAppTys'. -mkAppRedns :: Reduction -> Reductions -> Reduction -mkAppRedns (Reduction co ty) (Reductions cos tys) - = mkReduction (mkAppCos co cos) (mkAppTys ty tys) -{-# INLINE mkAppRedns #-} - --- | 'TyConAppCo' for 'Reduction's: combines 'mkTyConAppCo' and `mkTyConApp`. -mkTyConAppRedn :: Role -> TyCon -> Reductions -> Reduction -mkTyConAppRedn role tc (Reductions cos tys) - = mkReduction (mkTyConAppCo role tc cos) (mkTyConApp tc tys) -{-# INLINE mkTyConAppRedn #-} - --- | Reduce the arguments of a 'Class' 'TyCon'. -mkClassPredRedn :: Class -> Reductions -> Reduction -mkClassPredRedn cls (Reductions cos tys) - = mkReduction - (mkTyConAppCo Nominal (classTyCon cls) cos) - (mkClassPred cls tys) -{-# INLINE mkClassPredRedn #-} - --- | Obtain 'Reductions' from a list of 'Reduction's by unzipping. -unzipRedns :: [Reduction] -> Reductions -unzipRedns = foldr accRedn (Reductions [] []) - where - accRedn :: Reduction -> Reductions -> Reductions - accRedn (Reduction co xi) (Reductions cos xis) - = Reductions (co:cos) (xi:xis) -{-# INLINE unzipRedns #-} - --------------------------------------------------------------------------------- - -data ArgsReductions = - ArgsReductions - {-# UNPACK #-} !Reductions - !MCoercion - -{-# INLINE simplifyArgsWorker #-} -simplifyArgsWorker :: [TyCoBinder] -> Kind -> TyCoVarSet -> [Role] -> [Reduction] -> ArgsReductions -simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs - orig_roles orig_simplified_args - = go orig_lc - orig_ki_binders orig_inner_ki - orig_roles orig_simplified_args - where - orig_lc = emptyLiftingContext $ mkInScopeSet $ orig_fvs - - go :: LiftingContext -> [TyCoBinder] -> Kind -> [Role] -> [Reduction] -> ArgsReductions - go !lc binders inner_ki _ [] - = ArgsReductions - (mkReductions [] []) - kind_co - where - final_kind = mkPiTys binders inner_ki - kind_co | noFreeVarsOfType final_kind = MRefl - | otherwise = MCo $ liftCoSubst Nominal lc final_kind - - go lc (binder:binders) inner_ki (role:roles) (arg_redn:arg_redns) - = let !kind_co = liftCoSubst Nominal lc (tyCoBinderType binder) - !(Reduction casted_co casted_xi) - = mkCoherenceRightRedn role arg_redn kind_co - -- now, extend the lifting context with the new binding - !new_lc | Just tv <- tyCoBinderVar_maybe binder - = extendLiftingContextAndInScope lc tv casted_co - | otherwise - = lc - !(ArgsReductions (Reductions cos xis) final_kind_co) - = go new_lc binders inner_ki roles arg_redns - in ArgsReductions - (Reductions (casted_co:cos) (casted_xi:xis)) - final_kind_co - - -- See Note [Last case in simplifyArgsWorker] - go lc [] inner_ki roles arg_redns - = let co1 = liftCoSubst Nominal lc inner_ki - co1_kind = coercionKind co1 - unrewritten_tys = map reductionOriginalType arg_redns - (arg_cos, res_co) = decomposePiCos co1 co1_kind unrewritten_tys - casted_args = zipWith3 mkCoherenceRightRedn roles arg_redns arg_cos - zapped_lc = zapLiftingContext lc - Pair rewritten_kind _ = co1_kind - (bndrs, new_inner) = splitPiTys rewritten_kind - - ArgsReductions redns_out res_co_out - = go zapped_lc bndrs new_inner roles casted_args - in - ArgsReductions redns_out (res_co `mkTransMCoR` res_co_out) - - go _ _ _ _ _ = error "simplifyArgsWorker wandered into deeper water than usual" - --------------------------------------------------------------------------------- - --- | Get the reverse of an 'MCoercion' -mkSymMCo :: MCoercion -> MCoercion -mkSymMCo MRefl = MRefl -mkSymMCo (MCo co) = MCo (mkSymCo co) - -mkGReflLeftMCo :: Role -> Type -> MCoercion -> Coercion -mkGReflLeftMCo r ty MRefl = mkReflCo r ty -mkGReflLeftMCo r ty (MCo co) = mkGReflLeftCo r ty co - -mkGReflRightMCo :: Role -> Type -> MCoercion -> Coercion -mkGReflRightMCo r ty MRefl = mkReflCo r ty -mkGReflRightMCo r ty (MCo co) = mkGReflRightCo r ty co - --- | Cast a type by an 'MCoercion' -mkCastTyMCo :: Type -> MCoercion -> Type -mkCastTyMCo ty MRefl = ty -mkCastTyMCo ty (MCo co) = ty `mkCastTy` co - --- | Like 'mkCoherenceRightCo', but with an 'MCoercion' -mkCoherenceRightMCo :: Role -> Type -> MCoercion -> Coercion -> Coercion -mkCoherenceRightMCo _ _ MRefl co2 = co2 -mkCoherenceRightMCo r ty (MCo co) co2 = mkCoherenceRightCo r ty co co2 - -mkTransMCoR :: Coercion -> MCoercion -> MCoercion -mkTransMCoR co1 MRefl = coToMCo co1 -mkTransMCoR co1 (MCo co2) = MCo (mkTransCo co1 co2) - --------------------------------------------------------------------------------- - -#if !MIN_VERSION_ghc(9,0,0) - -coercionLKind, coercionRKind :: Coercion -> Type -coercionLKind co = case coercionKind co of { Pair lco _ -> lco } -coercionRKind co = case coercionKind co of { Pair _ rco -> rco } - --- | Creates a new coercion with both of its types casted by different casts --- @castCoercionKind2 g r t1 t2 h1 h2@, where @g :: t1 ~r t2@, --- has type @(t1 |> h1) ~r (t2 |> h2)@. --- @h1@ and @h2@ must be nominal. -castCoercionKind2 :: Coercion -> Role -> Type -> Type - -> CoercionN -> CoercionN -> Coercion -castCoercionKind2 g r t1 t2 h1 h2 - = mkCoherenceRightCo r t2 h2 (mkCoherenceLeftCo r t1 h1 g) - --- | @castCoercionKind1 g r t1 t2 h@ = @coercionKind g r t1 t2 h h@ --- That is, it's a specialised form of castCoercionKind, where the two --- kind coercions are identical --- @castCoercionKind1 g r t1 t2 h@, where @g :: t1 ~r t2@, --- has type @(t1 |> h) ~r (t2 |> h)@. --- @h@ must be nominal. --- See Note [castCoercionKind1] -castCoercionKind1 :: Coercion -> Role -> Type -> Type - -> CoercionN -> Coercion -castCoercionKind1 g r t1 t2 h - = case g of - Refl {} -> mkNomReflCo (mkCastTy t2 h) - GRefl _ _ mco -> case mco of - MRefl -> mkReflCo r (mkCastTy t2 h) - MCo kind_co -> GRefl r (mkCastTy t1 h) $ - MCo (mkSymCo h `mkTransCo` kind_co `mkTransCo` h) - _ -> castCoercionKind2 g r t1 t2 h h -#endif - -#if !MIN_VERSION_ghc(8,10,0) - -coToMCo :: Coercion -> MCoercion -coToMCo co | isReflCo co = MRefl - | otherwise = MCo co - -#endif +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE CPP #-} + +module GHC.TcPlugin.API.Internal.Shim.Reduction where + +-- base +import Prelude + hiding (Floating(cos)) + +-- ghc +import GHC.Core.Class + ( Class(classTyCon) ) +import GHC.Core.Coercion + ( Coercion, CoercionN, MCoercion(..) + , Role(Nominal), LiftingContext +#if MIN_VERSION_ghc(9,0,0) + , castCoercionKind1, castCoercionKind2 + , coercionLKind, coercionRKind +#else + , mkCoherenceLeftCo, mkNomReflCo +#endif + , coercionKind +#if MIN_VERSION_ghc(8,10,0) + , coToMCo +#else + , isReflCo +#endif + , decomposePiCos, downgradeRole + , liftCoSubst, emptyLiftingContext, extendLiftingContextAndInScope, zapLiftingContext + , mkAppCo, mkAppCos + , mkCoherenceRightCo + , mkForAllCo, mkFunCo + , mkGReflLeftCo, mkGReflRightCo + , mkHomoForAllCos, mkProofIrrelCo + , mkReflCo, mkSubCo, mkSymCo, mkTransCo, mkTyConAppCo + ) +import GHC.Core.Predicate + ( mkClassPred ) +import GHC.Core.TyCo.Rep + ( TyCoBinder, mkFunTy +#if !MIN_VERSION_ghc(9,0,0) + , Coercion(..) +#endif + ) +import GHC.Core.TyCon + ( TyCon ) +import GHC.Core.Type + ( ArgFlag, Kind, Type, TyVar, TyVarBinder +#if MIN_VERSION_ghc(8,10,0) + , AnonArgFlag +#endif + , binderVars + , mkAppTy, mkAppTys, mkCastTy, mkCoercionTy, mkForAllTy, mkForAllTys + , mkTyConApp, mkPiTys + , noFreeVarsOfType + , splitPiTys, tyCoBinderType, tyCoBinderVar_maybe + ) +import GHC.Data.Pair + ( Pair(Pair) ) +import GHC.Types.Var + ( setTyVarKind ) +import GHC.Types.Var.Env + ( mkInScopeSet ) +import GHC.Types.Var.Set + ( TyCoVarSet ) +import GHC.Utils.Outputable + ( Outputable(ppr), (<+>) + , braces, text, vcat + ) + +-------------------------------------------------------------------------------- + + +-- | A 'Reduction' is the result of an operation that rewrites a type @ty_in@. +-- The 'Reduction' includes the rewritten type @ty_out@ and a 'Coercion' @co@ +-- such that @co :: ty_in ~ ty_out@, where the role of the coercion is determined +-- by the context. That is, the LHS type of the coercion is the original type +-- @ty_in@, while its RHS type is the rewritten type @ty_out@. +-- +-- A Reduction is always homogeneous, unless it is wrapped inside a 'HetReduction', +-- which separately stores the kind coercion. +data Reduction = + Reduction + { reductionCoercion :: Coercion + , reductionReducedType :: !Type + } + +-- | Stores a heterogeneous reduction. +-- +-- The stored kind coercion must relate the kinds of the +-- stored reduction. That is, in @HetReduction (Reduction co xi) kco@, +-- we must have: +-- +-- > co :: ty ~ xi +-- > kco :: typeKind ty ~ typeKind xi +data HetReduction = + HetReduction + Reduction + MCoercion + +-- | Create a heterogeneous reduction. +-- +-- Pre-condition: the provided kind coercion (second argument) +-- relates the kinds of the stored reduction. +-- That is, if the coercion stored in the 'Reduction' is of the form +-- +-- > co :: ty ~ xi +-- +-- Then the kind coercion supplied must be of the form: +-- +-- > kco :: typeKind ty ~ typeKind xi +mkHetReduction :: Reduction -- ^ heterogeneous reduction + -> MCoercion -- ^ kind coercion + -> HetReduction +mkHetReduction redn mco = HetReduction redn mco +{-# INLINE mkHetReduction #-} + +-- | Homogenise a heterogeneous reduction. +-- +-- Given @HetReduction (Reduction co xi) kco@, with +-- +-- > co :: ty ~ xi +-- > kco :: typeKind(ty) ~ typeKind(xi) +-- +-- this returns the homogeneous reduction: +-- +-- > hco :: ty ~ ( xi |> sym kco ) +homogeniseHetRedn :: Role -> HetReduction -> Reduction +homogeniseHetRedn role (HetReduction redn kco) + = mkCoherenceRightMRedn role redn (mkSymMCo kco) +{-# INLINE homogeniseHetRedn #-} + +-- | Create a 'Reduction' from a pair of a 'Coercion' and a 'Type. +-- +-- Pre-condition: the RHS type of the coercion matches the provided type +-- (perhaps up to zonking). +-- +-- Use 'coercionRedn' when you only have the coercion. +mkReduction :: Coercion -> Type -> Reduction +mkReduction co ty = Reduction co ty +{-# INLINE mkReduction #-} + +instance Outputable Reduction where + ppr redn = + braces $ vcat + [ text "reductionOriginalType:" <+> ppr (reductionOriginalType redn) + , text " reductionReducedType:" <+> ppr (reductionReducedType redn) + , text " reductionCoercion:" <+> ppr (reductionCoercion redn) + ] + +-- | A 'Reduction' in which the 'Coercion' has 'Nominal' role. +type ReductionN = Reduction + +-- | A 'Reduction' in which the 'Coercion' has 'Representational' role. +type ReductionR = Reduction + +-- | Get the original, unreduced type corresponding to a 'Reduction'. +-- +-- This is obtained by computing the LHS kind of the stored coercion, +-- which may be slow. +reductionOriginalType :: Reduction -> Type +reductionOriginalType = coercionLKind . reductionCoercion +{-# INLINE reductionOriginalType #-} + +-- | Turn a 'Coercion' into a 'Reduction' +-- by inspecting the RHS type of the coercion. +-- +-- Prefer using 'mkReduction' when you already know +-- the RHS type of the coercion, to avoid computing it anew. +coercionRedn :: Coercion -> Reduction +coercionRedn co = Reduction co (coercionRKind co) +{-# INLINE coercionRedn #-} + +-- | Downgrade the role of the coercion stored in the 'Reduction'. +downgradeRedn :: Role -- ^ desired role + -> Role -- ^ current role + -> Reduction + -> Reduction +downgradeRedn new_role old_role redn@(Reduction co _) + = redn { reductionCoercion = downgradeRole new_role old_role co } +{-# INLINE downgradeRedn #-} + +-- | Downgrade the role of the coercion stored in the 'Reduction', +-- from 'Nominal' to 'Representational'. +mkSubRedn :: Reduction -> Reduction +mkSubRedn redn@(Reduction co _) = redn { reductionCoercion = mkSubCo co } +{-# INLINE mkSubRedn #-} + +-- | Compose a reduction with a coercion on the left. +-- +-- Pre-condition: the provided coercion's RHS type must match the LHS type +-- of the coercion that is stored in the reduction. +mkTransRedn :: Coercion -> Reduction -> Reduction +mkTransRedn co1 redn@(Reduction co2 _) + = redn { reductionCoercion = co1 `mkTransCo` co2 } +{-# INLINE mkTransRedn #-} + +-- | The reflexive reduction. +mkReflRedn :: Role -> Type -> Reduction +mkReflRedn r ty = mkReduction (mkReflCo r ty) ty + +-- | Create a 'Reduction' from a kind cast, in which +-- the casted type is the rewritten type. +-- +-- Given @ty :: k1@, @mco :: k1 ~ k2@, +-- produces the 'Reduction' @ty ~res_co~> (ty |> mco)@ +-- at the given 'Role'. +mkGReflRightRedn :: Role -> Type -> CoercionN -> Reduction +mkGReflRightRedn role ty co + = mkReduction + (mkGReflRightCo role ty co) + (mkCastTy ty co) +{-# INLINE mkGReflRightRedn #-} + +-- | Create a 'Reduction' from a kind cast, in which +-- the casted type is the rewritten type. +-- +-- Given @ty :: k1@, @mco :: k1 ~ k2@, +-- produces the 'Reduction' @ty ~res_co~> (ty |> mco)@ +-- at the given 'Role'. +mkGReflRightMRedn :: Role -> Type -> MCoercion -> Reduction +mkGReflRightMRedn role ty mco + = mkReduction + (mkGReflRightMCo role ty mco) + (mkCastTyMCo ty mco) +{-# INLINE mkGReflRightMRedn #-} + +-- | Create a 'Reduction' from a kind cast, in which +-- the casted type is the original (non-rewritten) type. +-- +-- Given @ty :: k1@, @mco :: k1 ~ k2@, +-- produces the 'Reduction' @(ty |> mco) ~res_co~> ty@ +-- at the given 'Role'. +mkGReflLeftRedn :: Role -> Type -> CoercionN -> Reduction +mkGReflLeftRedn role ty co + = mkReduction + (mkGReflLeftCo role ty co) + ty +{-# INLINE mkGReflLeftRedn #-} + +-- | Create a 'Reduction' from a kind cast, in which +-- the casted type is the original (non-rewritten) type. +-- +-- Given @ty :: k1@, @mco :: k1 ~ k2@, +-- produces the 'Reduction' @(ty |> mco) ~res_co~> ty@ +-- at the given 'Role'. +mkGReflLeftMRedn :: Role -> Type -> MCoercion -> Reduction +mkGReflLeftMRedn role ty mco + = mkReduction + (mkGReflLeftMCo role ty mco) + ty +{-# INLINE mkGReflLeftMRedn #-} + +-- | Apply a cast to the result of a 'Reduction'. +-- +-- Given a 'Reduction' @ty1 ~co1~> (ty2 :: k2)@ and a kind coercion @kco@ +-- with LHS kind @k2@, produce a new 'Reduction' @ty1 ~co2~> ( ty2 |> kco )@ +-- of the given 'Role' (which must match the role of the coercion stored +-- in the 'Reduction' argument). +mkCoherenceRightRedn :: Role -> Reduction -> CoercionN -> Reduction +mkCoherenceRightRedn r (Reduction co1 ty2) kco + = mkReduction + (mkCoherenceRightCo r ty2 kco co1) + (mkCastTy ty2 kco) +{-# INLINE mkCoherenceRightRedn #-} + +-- | Apply a cast to the result of a 'Reduction', using an 'MCoercionN'. +-- +-- Given a 'Reduction' @ty1 ~co1~> (ty2 :: k2)@ and a kind coercion @mco@ +-- with LHS kind @k2@, produce a new 'Reduction' @ty1 ~co2~> ( ty2 |> mco )@ +-- of the given 'Role' (which must match the role of the coercion stored +-- in the 'Reduction' argument). +mkCoherenceRightMRedn :: Role -> Reduction -> MCoercion -> Reduction +mkCoherenceRightMRedn r (Reduction co1 ty2) kco + = mkReduction + (mkCoherenceRightMCo r ty2 kco co1) + (mkCastTyMCo ty2 kco) +{-# INLINE mkCoherenceRightMRedn #-} + +-- | Apply a cast to a 'Reduction', casting both the original and the reduced type. +-- +-- Given @cast_co@ and 'Reduction' @ty ~co~> xi@, this function returns +-- the 'Reduction' @(ty |> cast_co) ~return_co~> (xi |> cast_co)@ +-- of the given 'Role' (which must match the role of the coercion stored +-- in the 'Reduction' argument). +-- +-- Pre-condition: the 'Type' passed in is the same as the LHS type +-- of the coercion stored in the 'Reduction'. +mkCastRedn1 :: Role + -> Type -- ^ original type + -> CoercionN -- ^ coercion to cast with + -> Reduction -- ^ rewritten type, with rewriting coercion + -> Reduction +mkCastRedn1 r ty cast_co (Reduction co xi) + -- co :: ty ~r ty' + -- return_co :: (ty |> cast_co) ~r (ty' |> cast_co) + = mkReduction + (castCoercionKind1 co r ty xi cast_co) + (mkCastTy xi cast_co) +{-# INLINE mkCastRedn1 #-} + +-- | Apply casts on both sides of a 'Reduction' (of the given 'Role'). +-- +-- Use 'mkCastRedn1' when you want to cast both the original and reduced types +-- in a 'Reduction' using the same coercion. +-- +-- Pre-condition: the 'Type' passed in is the same as the LHS type +-- of the coercion stored in the 'Reduction'. +mkCastRedn2 :: Role + -> Type -- ^ original type + -> CoercionN -- ^ coercion to cast with on the left + -> Reduction -- ^ rewritten type, with rewriting coercion + -> CoercionN -- ^ coercion to cast with on the right + -> Reduction +mkCastRedn2 r ty cast_co (Reduction nco nty) cast_co' + = mkReduction + (castCoercionKind2 nco r ty nty cast_co cast_co') + (mkCastTy nty cast_co') +{-# INLINE mkCastRedn2 #-} + +-- | Apply one 'Reduction' to another. +-- +-- Combines 'mkAppCo' and 'mkAppTy`. +mkAppRedn :: Reduction -> Reduction -> Reduction +mkAppRedn (Reduction co1 ty1) (Reduction co2 ty2) + = mkReduction (mkAppCo co1 co2) (mkAppTy ty1 ty2) +{-# INLINE mkAppRedn #-} + +-- | Create a function 'Reduction'. +-- +-- Combines 'mkFunCo' and 'mkFunTy'. +mkFunRedn :: Role +#if MIN_VERSION_ghc(8,10,0) + -> AnonArgFlag +#endif +#if MIN_VERSION_ghc(9,0,0) + -> ReductionN -- ^ multiplicity reduction +#endif + -> Reduction -- ^ argument reduction + -> Reduction -- ^ result reduction + -> Reduction +mkFunRedn r +#if MIN_VERSION_ghc(8,10,0) + vis +#endif +#if MIN_VERSION_ghc(9,0,0) + (Reduction w_co w_ty) +#endif + (Reduction arg_co arg_ty) + (Reduction res_co res_ty) + = mkReduction + ( mkFunCo + r +#if MIN_VERSION_ghc(9,0,0) + w_co +#endif + arg_co + res_co + ) + ( mkFunTy +#if MIN_VERSION_ghc(8,10,0) + vis +#endif +#if MIN_VERSION_ghc(9,0,0) + w_ty +#endif + arg_ty + res_ty + ) +{-# INLINE mkFunRedn #-} + +-- | Create a 'Reduction' associated to a Π type, +-- from a kind 'Reduction' and a body 'Reduction'. +-- +-- Combines 'mkForAllCo' and 'mkForAllTy'. +mkForAllRedn :: ArgFlag + -> TyVar + -> ReductionN -- ^ kind reduction + -> Reduction -- ^ body reduction + -> Reduction +mkForAllRedn vis tv1 (Reduction h ki') (Reduction co ty) + = mkReduction + (mkForAllCo tv1 h co) + (mkForAllTy tv2 vis ty) + where + tv2 = setTyVarKind tv1 ki' +{-# INLINE mkForAllRedn #-} + +-- | Create a 'Reduction' of a quantified type from a +-- 'Reduction' of the body. +-- +-- Combines 'mkHomoForAllCos' and 'mkForAllTys'. +mkHomoForAllRedn :: [TyVarBinder] -> Reduction -> Reduction +mkHomoForAllRedn bndrs (Reduction co ty) + = mkReduction + (mkHomoForAllCos (binderVars bndrs) co) + (mkForAllTys bndrs ty) +{-# INLINE mkHomoForAllRedn #-} + +-- | Create a 'Reduction' from a coercion between coercions. +-- +-- Combines 'mkProofIrrelCo' and 'mkCoercionTy'. +mkProofIrrelRedn :: Role -- ^ role of the created coercion, "r" + -> CoercionN -- ^ co :: phi1 ~N phi2 + -> Coercion -- ^ g1 :: phi1 + -> Coercion -- ^ g2 :: phi2 + -> Reduction -- ^ res_co :: g1 ~r g2 +mkProofIrrelRedn role co g1 g2 + = mkReduction + (mkProofIrrelCo role co g1 g2) + (mkCoercionTy g2) +{-# INLINE mkProofIrrelRedn #-} + +-- | Create a reflexive 'Reduction' whose RHS is the given 'Coercion', +-- with the specified 'Role'. +mkReflCoRedn :: Role -> Coercion -> Reduction +mkReflCoRedn role co + = mkReduction + (mkReflCo role co_ty) + co_ty + where + co_ty = mkCoercionTy co +{-# INLINE mkReflCoRedn #-} + +-- | A collection of 'Reduction's where the coercions and the types are stored separately. +-- +-- Use 'unzipRedns' to obtain 'Reductions' from a list of 'Reduction's. +-- +-- This datatype is used in 'mkAppRedns', 'mkClassPredRedns' and 'mkTyConAppRedn', +-- which expect separate types and coercions. +-- +-- Invariant: the two stored lists are of the same length, +-- and the RHS type of each coercion is the corresponding type. +data Reductions = Reductions [Coercion] [Type] + +-- | Create 'Reductions' from individual lists of coercions and types. +-- +-- The lists should be of the same length, and the RHS type of each coercion +-- should match the specified type in the other list. +mkReductions :: [Coercion] -> [Type] -> Reductions +mkReductions cos tys = Reductions cos tys +{-# INLINE mkReductions #-} + +-- | Combines 'mkAppCos' and 'mkAppTys'. +mkAppRedns :: Reduction -> Reductions -> Reduction +mkAppRedns (Reduction co ty) (Reductions cos tys) + = mkReduction (mkAppCos co cos) (mkAppTys ty tys) +{-# INLINE mkAppRedns #-} + +-- | 'TyConAppCo' for 'Reduction's: combines 'mkTyConAppCo' and `mkTyConApp`. +mkTyConAppRedn :: Role -> TyCon -> Reductions -> Reduction +mkTyConAppRedn role tc (Reductions cos tys) + = mkReduction (mkTyConAppCo role tc cos) (mkTyConApp tc tys) +{-# INLINE mkTyConAppRedn #-} + +-- | Reduce the arguments of a 'Class' 'TyCon'. +mkClassPredRedn :: Class -> Reductions -> Reduction +mkClassPredRedn cls (Reductions cos tys) + = mkReduction + (mkTyConAppCo Nominal (classTyCon cls) cos) + (mkClassPred cls tys) +{-# INLINE mkClassPredRedn #-} + +-- | Obtain 'Reductions' from a list of 'Reduction's by unzipping. +unzipRedns :: [Reduction] -> Reductions +unzipRedns = foldr accRedn (Reductions [] []) + where + accRedn :: Reduction -> Reductions -> Reductions + accRedn (Reduction co xi) (Reductions cos xis) + = Reductions (co:cos) (xi:xis) +{-# INLINE unzipRedns #-} + +-------------------------------------------------------------------------------- + +data ArgsReductions = + ArgsReductions + {-# UNPACK #-} !Reductions + !MCoercion + +{-# INLINE simplifyArgsWorker #-} +simplifyArgsWorker :: [TyCoBinder] -> Kind -> TyCoVarSet -> [Role] -> [Reduction] -> ArgsReductions +simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs + orig_roles orig_simplified_args + = go orig_lc + orig_ki_binders orig_inner_ki + orig_roles orig_simplified_args + where + orig_lc = emptyLiftingContext $ mkInScopeSet $ orig_fvs + + go :: LiftingContext -> [TyCoBinder] -> Kind -> [Role] -> [Reduction] -> ArgsReductions + go !lc binders inner_ki _ [] + = ArgsReductions + (mkReductions [] []) + kind_co + where + final_kind = mkPiTys binders inner_ki + kind_co | noFreeVarsOfType final_kind = MRefl + | otherwise = MCo $ liftCoSubst Nominal lc final_kind + + go lc (binder:binders) inner_ki (role:roles) (arg_redn:arg_redns) + = let !kind_co = liftCoSubst Nominal lc (tyCoBinderType binder) + !(Reduction casted_co casted_xi) + = mkCoherenceRightRedn role arg_redn kind_co + -- now, extend the lifting context with the new binding + !new_lc | Just tv <- tyCoBinderVar_maybe binder + = extendLiftingContextAndInScope lc tv casted_co + | otherwise + = lc + !(ArgsReductions (Reductions cos xis) final_kind_co) + = go new_lc binders inner_ki roles arg_redns + in ArgsReductions + (Reductions (casted_co:cos) (casted_xi:xis)) + final_kind_co + + -- See Note [Last case in simplifyArgsWorker] + go lc [] inner_ki roles arg_redns + = let co1 = liftCoSubst Nominal lc inner_ki + co1_kind = coercionKind co1 + unrewritten_tys = map reductionOriginalType arg_redns + (arg_cos, res_co) = decomposePiCos co1 co1_kind unrewritten_tys + casted_args = zipWith3 mkCoherenceRightRedn roles arg_redns arg_cos + zapped_lc = zapLiftingContext lc + Pair rewritten_kind _ = co1_kind + (bndrs, new_inner) = splitPiTys rewritten_kind + + ArgsReductions redns_out res_co_out + = go zapped_lc bndrs new_inner roles casted_args + in + ArgsReductions redns_out (res_co `mkTransMCoR` res_co_out) + + go _ _ _ _ _ = error "simplifyArgsWorker wandered into deeper water than usual" + +-------------------------------------------------------------------------------- + +-- | Get the reverse of an 'MCoercion' +mkSymMCo :: MCoercion -> MCoercion +mkSymMCo MRefl = MRefl +mkSymMCo (MCo co) = MCo (mkSymCo co) + +mkGReflLeftMCo :: Role -> Type -> MCoercion -> Coercion +mkGReflLeftMCo r ty MRefl = mkReflCo r ty +mkGReflLeftMCo r ty (MCo co) = mkGReflLeftCo r ty co + +mkGReflRightMCo :: Role -> Type -> MCoercion -> Coercion +mkGReflRightMCo r ty MRefl = mkReflCo r ty +mkGReflRightMCo r ty (MCo co) = mkGReflRightCo r ty co + +-- | Cast a type by an 'MCoercion' +mkCastTyMCo :: Type -> MCoercion -> Type +mkCastTyMCo ty MRefl = ty +mkCastTyMCo ty (MCo co) = ty `mkCastTy` co + +-- | Like 'mkCoherenceRightCo', but with an 'MCoercion' +mkCoherenceRightMCo :: Role -> Type -> MCoercion -> Coercion -> Coercion +mkCoherenceRightMCo _ _ MRefl co2 = co2 +mkCoherenceRightMCo r ty (MCo co) co2 = mkCoherenceRightCo r ty co co2 + +mkTransMCoR :: Coercion -> MCoercion -> MCoercion +mkTransMCoR co1 MRefl = coToMCo co1 +mkTransMCoR co1 (MCo co2) = MCo (mkTransCo co1 co2) + +-------------------------------------------------------------------------------- + +#if !MIN_VERSION_ghc(9,0,0) + +coercionLKind, coercionRKind :: Coercion -> Type +coercionLKind co = case coercionKind co of { Pair lco _ -> lco } +coercionRKind co = case coercionKind co of { Pair _ rco -> rco } + +-- | Creates a new coercion with both of its types casted by different casts +-- @castCoercionKind2 g r t1 t2 h1 h2@, where @g :: t1 ~r t2@, +-- has type @(t1 |> h1) ~r (t2 |> h2)@. +-- @h1@ and @h2@ must be nominal. +castCoercionKind2 :: Coercion -> Role -> Type -> Type + -> CoercionN -> CoercionN -> Coercion +castCoercionKind2 g r t1 t2 h1 h2 + = mkCoherenceRightCo r t2 h2 (mkCoherenceLeftCo r t1 h1 g) + +-- | @castCoercionKind1 g r t1 t2 h@ = @coercionKind g r t1 t2 h h@ +-- That is, it's a specialised form of castCoercionKind, where the two +-- kind coercions are identical +-- @castCoercionKind1 g r t1 t2 h@, where @g :: t1 ~r t2@, +-- has type @(t1 |> h) ~r (t2 |> h)@. +-- @h@ must be nominal. +-- See Note [castCoercionKind1] +castCoercionKind1 :: Coercion -> Role -> Type -> Type + -> CoercionN -> Coercion +castCoercionKind1 g r t1 t2 h + = case g of + Refl {} -> mkNomReflCo (mkCastTy t2 h) + GRefl _ _ mco -> case mco of + MRefl -> mkReflCo r (mkCastTy t2 h) + MCo kind_co -> GRefl r (mkCastTy t1 h) $ + MCo (mkSymCo h `mkTransCo` kind_co `mkTransCo` h) + _ -> castCoercionKind2 g r t1 t2 h h +#endif + +#if !MIN_VERSION_ghc(8,10,0) + +coToMCo :: Coercion -> MCoercion +coToMCo co | isReflCo co = MRefl + | otherwise = MCo co + +#endif diff --git a/src/GHC/TcPlugin/API/Names.hs b/src/GHC/TcPlugin/API/Names.hs --- a/src/GHC/TcPlugin/API/Names.hs +++ b/src/GHC/TcPlugin/API/Names.hs @@ -1,494 +1,494 @@ -{-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE CPP #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE GeneralisedNewtypeDeriving #-} -{-# LANGUAGE InstanceSigs #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE QuantifiedConstraints #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE UndecidableInstances #-} - -#if MIN_VERSION_ghc(9,0,0) -{-# LANGUAGE StandaloneKindSignatures #-} -#endif - -{-| -Module: GHC.TcPlugin.API.Names - -This module provides an /optional/ framework that facilitates name lookup -in type-checking plugins, using constrained traversals (similar to the -). - -See the 'ResolveNames' typeclass. - -Before: - -> data PluginDefs = -> PluginDefs -> { myTyCon :: TyCon -> , myClass :: Class -> , myPromotedDataCon :: TyCon -> } -> -> findMyModule :: MonadTcPlugin m => m Module -> findMyModule = do -> findResult <- findImportedModule ( mkModuleName "MyModule" ) Nothing -> case findResult of -> Found _ res -> pure res -> _ -> error $ "MyPlugin: could not find any module named MyModule." -> -> pluginInit :: TcPluginM Init PluginDefs -> pluginInit = do -> myModule <- findMyModule -> myTyCon <- tcLookupTyCon =<< lookupOrig myModule ( mkTcOcc "MyTyCon" ) -> myClass <- tcLookupClass =<< lookupOrig myModule ( mkClsOcc "MyClass" ) -> myPromotedDataCon <- fmap promoteDataCon . tcLookupDataCon =<< lookupOrig myModule ( mkDataOcc "MyDataCon" ) -> pure ( PluginDefs { .. } ) - -After: - -> data PluginDefsHKD n = -> PluginDefs -> { myTyCon :: Wear n TyCon -> , myClass :: Wear n Class -> , myPromotedDataCon :: Wear n ( Promoted DataCon ) -> } -> deriving stock Generic -> deriving ResolveNames -> via Generically1 PluginDefsHKD -> -> type PluginDefs = PluginDefsHKD Resolved -> -> pluginInit :: TcPluginM Init PluginDefs -> pluginInit = resolveNames pluginNames -> where -> pluginNames :: PluginDefsHKD Named -> pluginNames = -> PluginDefs -> { myTyCon = mkQualified "MyTyCon" -> , myClass = mkQualified "MyClass" -> , myPromotedDataCon = mkQualified "MyDataCon" -> } -> mkQualified :: String -> QualifiedName thing -> mkQualified str = -> Qualified -> { name = str -> , module' = mkModuleName "MyModule" -> , package = Nothing -> } - --} - -module GHC.TcPlugin.API.Names - ( ResolveNames, resolveNames - , Wear, QualifiedName(..), NameResolution(..) - , Promoted - , Lookupable(..) - - -- * Re-export Generically1 for compatibility. - , Generically1(..) - ) where - --- base -import Prelude - hiding ( lookup ) -import Data.Coerce - ( Coercible, coerce ) -import Data.Kind - ( Type, Constraint ) -import GHC.Generics - ( Generic(..) -#if MIN_VERSION_base(4,17,0) - , Generically1(..) -#endif - , (:+:)(..), (:*:)(..) - , K1(K1), M1(M1), U1(..), V1, Rec0 - ) -import GHC.TypeLits - ( TypeError, ErrorMessage(..) ) - --- transformers -import Control.Monad.Trans.State.Strict - ( StateT, evalStateT, get, put ) -import Control.Monad.Trans.Class - ( MonadTrans(lift) ) - --- ghc -#if MIN_VERSION_ghc(9,3,0) -import GHC.Iface.Errors - ( cannotFindModule ) -#elif MIN_VERSION_ghc(9,2,0) -import GHC.Iface.Load - ( cannotFindModule ) -#else -import GHC.Driver.Types - ( hsc_dflags ) -import GHC.Driver.Finder - ( cannotFindModule ) -import GHC.Driver.Session - ( DynFlags ) -#endif -#if MIN_VERSION_ghc(9,5,0) -import Language.Haskell.Syntax.Module.Name - ( moduleNameString ) -#else -import GHC.Unit.Module.Name - ( moduleNameString ) -#endif -import GHC.Unit.Types - ( unitIdString ) -import GHC.Utils.Panic - ( pgmErrorDoc ) -import GHC.Tc.Plugin - ( getTopEnv ) -import GHC.Types.Unique.FM - ( addToUFM, addToUFM_C, lookupUFM, plusUFM, unitUFM ) - --- ghc-tcplugin-api -import GHC.TcPlugin.API - hiding ( Type ) -import GHC.TcPlugin.API.Internal - ( MonadTcPlugin(liftTcPluginM) ) - --------------------------------------------------------------------------------- - --- | A 'QualifiedName' is the name of something, --- together with the names of the module and package it comes from. -data QualifiedName (thing :: Type) - = Qualified - { -- | Name of the thing (e.g. name of the 'TyCon' or 'Class'). - name :: String - -- | Name of the module in which the thing can be found. - , module' :: ModuleName - -- | Name of the package in which the module can be found. - , package :: PkgQual - } - --- | Type-level parameter to 'Wear' type family, for higher-kinded data. --- --- @Wear Named thing@ is the identifier data passed in as an argument. --- @Wear Resolved thing@ is the result of name resolving the thing. --- --- This allows users to pass a record of names, of type @MyData Named@, --- and obtain a record of looked-up things, of type @MyData Resolved@. --- --- Refer to 'ResolveNames' for a worked example. -data NameResolution = Named | Resolved - --- | Use this to refer to a @Promoted DataCon@. -data Promoted (thing :: k) :: Type - --- | Type-family used for higher-kinded data pattern. --- --- This allows the same record to be re-used, --- as explained in the worked example for 'ResolveNames'. --- --- For instance, if one defines: --- --- > data MyData n --- > = MyData --- > { myClass :: !( Wear n Class ) --- > , myTyCon :: !( Wear n TyCon ) --- > } --- --- then a record of type @MyData Named@ is simply a record of textual names --- (a typeclass name and a type-constructor name, with associated module & packages), --- whereas a record of type @MyData Resolved@ contains a typeclass's @Class@ --- as well as a type-constructor's @TyCon@. -#if MIN_VERSION_ghc(9,0,0) -type Wear :: forall k. NameResolution -> k -> Type -#endif -type family Wear (n :: NameResolution) (thing :: k) :: Type where -#if MIN_VERSION_ghc(9,0,0) - Wear @Type Named thing = QualifiedName thing -#else - Wear Named thing = QualifiedName thing -#endif - Wear Resolved (Promoted DataCon) = TyCon - Wear Resolved (Promoted a) - = TypeError - ( Text "Cannot promote " :<>: ShowType a :<>: Text "." - :$$: Text "Can only promote 'DataCon's." - ) - Wear Resolved thing = thing - --- | Retrieve the underlying thing being referred to by inspecting --- the type parameter of 'QualifiedName'. -type family UnwearNamed (loc :: Type) :: Type where - UnwearNamed (QualifiedName thing) = thing - --- | Type-class overloading things that can be looked up by name: --- --- * classes, --- * data constructors (as well as their promotion), --- * type-constructors. -#if MIN_VERSION_ghc(9,0,0) -type Lookupable :: forall {k}. k -> Constraint -#endif -class Lookupable (a :: k) where - mkOccName :: String -> OccName - lookup :: MonadTcPlugin m => Name -> m (Wear Resolved a) - -instance Lookupable TyCon where - mkOccName = mkTcOcc - lookup = tcLookupTyCon -instance Lookupable DataCon where - mkOccName = mkDataOcc - lookup = tcLookupDataCon -instance Lookupable Class where - mkOccName = mkClsOcc - lookup = tcLookupClass -instance Lookupable (Promoted DataCon) where - mkOccName = mkDataOcc - lookup = fmap promoteDataCon . tcLookupDataCon - --- | This class exposes the method 'resolveNames' which will --- perform name resolution for all the fields in a datatype. --- --- Example usage: we define a record that will hold --- the things we want to look up, using the 'Wear' type family. --- --- For example: --- --- > data MyData n --- > = MyData --- > { myClass :: !( Wear n Class ) --- > , myTyCon :: !( Wear n TyCon ) --- > , myDataCon :: !( Wear n DataCon ) --- > , myPromDataCon :: !( Wear n (Promoted DataCon) ) --- > } --- > deriving stock Generic --- > deriving ResolveNames --- > via Generically1 MyData --- --- Now we can specify the names of the things which we want to look up, --- together with the modules and packages in which they belong: --- --- > myNames :: MyData Named --- > myNames = MyData --- > { myClass = QualifiedName "MyClass" "My.Module" ( Just "my-pkg-name" ) --- > , ... --- > } --- --- Then we can call 'resolveNames': --- --- > resolvedNames :: MonadTcPlugin m => m (MyData Resolved) --- > resolvedNames = resolveNames myNames --- --- This returns a record containing the looked up things we want, --- e.g. @myClass :: Class@, @myPromDataCon :: TyCon@, etc. -class ResolveNames (f :: NameResolution -> Type) where - resolve_names :: ( Coercible res ( f Resolved ), MonadTcPlugin m ) - => f Named -> m res - -- Workaround: the result is anything coercible to "f Resolved" rather than just "f Resolved", - -- because otherwise GHC complains when using DerivingVia that we don't know the role - -- of the parameter to m, despite the quantified constraint superclass to MonadTcPlugin. - -- - -- This unfortunately worsens type-inference, so we export - -- 'resolveNames' separately. - --- | Resolve a collection of names. --- --- See 'ResolveNames' for further details. -resolveNames :: ( MonadTcPlugin m, ResolveNames f ) - => f Named -> m ( f Resolved ) -resolveNames = resolve_names - -instance ( Generic (f Named) - , Generic (f Resolved) - , GTraversableC ResolveName (Rep (f Named)) (Rep (f Resolved)) - ) - => ResolveNames (Generically1 f) where - resolve_names - :: forall -#if MIN_VERSION_ghc(9,0,0) - {m} -#else - m -#endif - res - . ( Coercible res ( Generically1 f Resolved ), MonadTcPlugin m ) - => Generically1 f Named -> m res - resolve_names ( Generically1 dat ) - = ( `evalStateT` emptyModules ) - $ coerce . to @(f Resolved) - <$> gtraverseC @ResolveName resolveName ( from dat ) - --- | Type-class dispatch for looking up names. --- --- Every instance is of the form: --- --- > ResolveName (Wear Named thing) (Wear Resolved thing) --- --- which allows one to write 'resolveName': --- --- > resolveName :: ... => Wear Named thing -> m ( Wear Resolved thing ) -class ( a ~ Wear Named ( UnwearNamed a ) - , b ~ Wear Resolved ( UnwearNamed a ) - , Lookupable ( UnwearNamed a ) - ) - => ResolveName (a :: Type) (b :: Type) -instance ( a ~ Wear Named ( UnwearNamed a ) - , b ~ Wear Resolved ( UnwearNamed a ) - , Lookupable ( UnwearNamed a ) - ) - => ResolveName a b - -resolveName :: forall (thing :: Type) m - . ResolveName ( Wear Named thing ) ( Wear Resolved thing ) - => MonadTcPlugin m - => Wear Named thing - -> StateT ImportedModules m ( Wear Resolved thing ) -resolveName (Qualified str mod_name pkg) = do - md <- lookupModule pkg mod_name - nm <- lift $ lookupOrig md - (mkOccName -#if !MIN_VERSION_ghc(9,0,0) - @_ -#endif - @thing - str - ) - lift $ lookup -#if !MIN_VERSION_ghc(9,0,0) - @_ -#endif - @thing nm - --------------------------------------------------------------------------------- --- Caching of found modules. - -data ImportedModules - = ImportedModules - { home_modules :: UniqFM ModuleName Module - , this_pkg_modules :: UniqFM UnitId ( UniqFM ModuleName Module ) - , other_pkg_modules :: UniqFM UnitId ( UniqFM ModuleName Module ) - } - -emptyModules :: ImportedModules -emptyModules = - ImportedModules - { home_modules = emptyUFM - , this_pkg_modules = emptyUFM - , other_pkg_modules = emptyUFM - } - -lookupCachedModule :: Monad m => PkgQual -> ModuleName -> StateT ImportedModules m (Maybe Module) -lookupCachedModule NoPkgQual mod_name - = ( `lookupUFM` mod_name ) - . home_modules - <$> get -lookupCachedModule (ThisPkg pkg) mod_name - = ( ( `lookupUFM` mod_name ) =<< ) - . ( `lookupUFM` pkg ) - . this_pkg_modules - <$> get -lookupCachedModule (OtherPkg pkg) mod_name - = ( ( `lookupUFM` mod_name ) =<< ) - . ( `lookupUFM` pkg ) - . other_pkg_modules - <$> get - -insertCachedModule :: Monad m => PkgQual -> ModuleName -> Module -> StateT ImportedModules m () -insertCachedModule NoPkgQual mod_name md = do - mods@( ImportedModules { home_modules = prev } ) <- get - put $ mods { home_modules = addToUFM prev mod_name md } -insertCachedModule (ThisPkg pkg) mod_name md = do - mods@( ImportedModules { this_pkg_modules = prev } ) <- get - put $ mods { this_pkg_modules = addToUFM_C plusUFM prev pkg (unitUFM mod_name md) } -insertCachedModule (OtherPkg pkg) mod_name md = do - mods@( ImportedModules { other_pkg_modules = prev } ) <- get - put $ mods { other_pkg_modules = addToUFM_C plusUFM prev pkg (unitUFM mod_name md) } - -lookupModule :: MonadTcPlugin m => PkgQual -> ModuleName -> StateT ImportedModules m Module -lookupModule pkg mod_name = do - cachedResult <- lookupCachedModule pkg mod_name - case cachedResult of - Just res -> do - insertCachedModule pkg mod_name res - pure res - Nothing -> do - findResult <- lift $ findImportedModule mod_name pkg - case findResult of - Found _ res - -> pure res - other -> do - hsc_env <- lift . liftTcPluginM $ getTopEnv - let - err_doc :: SDoc -#if MIN_VERSION_ghc(9,2,0) - err_doc = cannotFindModule hsc_env mod_name other -#else - err_doc = cannotFindModule dflags mod_name other - dflags :: DynFlags - dflags = hsc_dflags hsc_env -#endif - pgmErrorDoc - ( "GHC.TcPlugin.API: could not find module " <> mod_str <> " in " <> pkg_name ) - err_doc - where - pkg_name, mod_str :: String - pkg_name = case pkg of - NoPkgQual -> "home package" - ThisPkg unit -> "home-unit package " <> unitIdString unit - OtherPkg unit -> "other unit package" <> unitIdString unit - mod_str = moduleNameString mod_name - --------------------------------------------------------------------------------- --- Constrained traversals. - -type TraversalC (c :: Type -> Type -> Constraint) (s :: Type) (t :: Type) - = forall f. ( Applicative f ) - => ( forall a b. c a b => a -> f b ) -> s -> f t - -class GTraversableC (c :: Type -> Type -> Constraint) (s :: Type -> Type) (t :: Type -> Type) where - gtraverseC :: TraversalC c (s x) (t x) - -instance - ( GTraversableC c l l' - , GTraversableC c r r' - ) => GTraversableC c (l :*: r) (l' :*: r') where - gtraverseC f (l :*: r) - = (:*:) <$> gtraverseC @c f l <*> gtraverseC @c f r - -instance - ( GTraversableC c l l' - , GTraversableC c r r' - ) => GTraversableC c (l :+: r) (l' :+: r') where - gtraverseC f (L1 l) = L1 <$> gtraverseC @c f l - gtraverseC f (R1 r) = R1 <$> gtraverseC @c f r - -instance GTraversableC c s t - => GTraversableC c (M1 i m s) (M1 i m t) where - gtraverseC f (M1 x) = M1 <$> gtraverseC @c f x - -instance GTraversableC c U1 U1 where - gtraverseC _ _ = pure U1 - -instance GTraversableC c V1 V1 where - gtraverseC _ = pure - -instance c a b => GTraversableC c (Rec0 a) (Rec0 b) where - gtraverseC f (K1 a) = K1 <$> f a - --------------------------------------------------------------------------------- --- Generically and Generically1 wrappers for DerivingVia. - -#if !MIN_VERSION_base(4,17,0) --- | A type whose instances are defined generically, using the --- 'Generic1' representation. 'Generically1' is a higher-kinded --- version of 'Generically' that uses 'Generic'. --- --- Generic instances can be derived for type constructors via --- @'Generically1' F@ using @-XDerivingVia@. -newtype Generically1 (f :: k -> Type) (a :: k) = Generically1 ( f a ) -#endif +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GeneralisedNewtypeDeriving #-} +{-# LANGUAGE InstanceSigs #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +#if MIN_VERSION_ghc(9,0,0) +{-# LANGUAGE StandaloneKindSignatures #-} +#endif + +{-| +Module: GHC.TcPlugin.API.Names + +This module provides an /optional/ framework that facilitates name lookup +in type-checking plugins, using constrained traversals (similar to the +). + +See the 'ResolveNames' typeclass. + +Before: + +> data PluginDefs = +> PluginDefs +> { myTyCon :: TyCon +> , myClass :: Class +> , myPromotedDataCon :: TyCon +> } +> +> findMyModule :: MonadTcPlugin m => m Module +> findMyModule = do +> findResult <- findImportedModule ( mkModuleName "MyModule" ) Nothing +> case findResult of +> Found _ res -> pure res +> _ -> error $ "MyPlugin: could not find any module named MyModule." +> +> pluginInit :: TcPluginM Init PluginDefs +> pluginInit = do +> myModule <- findMyModule +> myTyCon <- tcLookupTyCon =<< lookupOrig myModule ( mkTcOcc "MyTyCon" ) +> myClass <- tcLookupClass =<< lookupOrig myModule ( mkClsOcc "MyClass" ) +> myPromotedDataCon <- fmap promoteDataCon . tcLookupDataCon =<< lookupOrig myModule ( mkDataOcc "MyDataCon" ) +> pure ( PluginDefs { .. } ) + +After: + +> data PluginDefsHKD n = +> PluginDefs +> { myTyCon :: Wear n TyCon +> , myClass :: Wear n Class +> , myPromotedDataCon :: Wear n ( Promoted DataCon ) +> } +> deriving stock Generic +> deriving ResolveNames +> via Generically1 PluginDefsHKD +> +> type PluginDefs = PluginDefsHKD Resolved +> +> pluginInit :: TcPluginM Init PluginDefs +> pluginInit = resolveNames pluginNames +> where +> pluginNames :: PluginDefsHKD Named +> pluginNames = +> PluginDefs +> { myTyCon = mkQualified "MyTyCon" +> , myClass = mkQualified "MyClass" +> , myPromotedDataCon = mkQualified "MyDataCon" +> } +> mkQualified :: String -> QualifiedName thing +> mkQualified str = +> Qualified +> { name = str +> , module' = mkModuleName "MyModule" +> , package = Nothing +> } + +-} + +module GHC.TcPlugin.API.Names + ( ResolveNames, resolveNames + , Wear, QualifiedName(..), NameResolution(..) + , Promoted + , Lookupable(..) + + -- * Re-export Generically1 for compatibility. + , Generically1(..) + ) where + +-- base +import Prelude + hiding ( lookup ) +import Data.Coerce + ( Coercible, coerce ) +import Data.Kind + ( Type, Constraint ) +import GHC.Generics + ( Generic(..) +#if MIN_VERSION_base(4,17,0) + , Generically1(..) +#endif + , (:+:)(..), (:*:)(..) + , K1(K1), M1(M1), U1(..), V1, Rec0 + ) +import GHC.TypeLits + ( TypeError, ErrorMessage(..) ) + +-- transformers +import Control.Monad.Trans.State.Strict + ( StateT, evalStateT, get, put ) +import Control.Monad.Trans.Class + ( MonadTrans(lift) ) + +-- ghc +#if MIN_VERSION_ghc(9,3,0) +import GHC.Iface.Errors + ( cannotFindModule ) +#elif MIN_VERSION_ghc(9,2,0) +import GHC.Iface.Load + ( cannotFindModule ) +#else +import GHC.Driver.Types + ( hsc_dflags ) +import GHC.Driver.Finder + ( cannotFindModule ) +import GHC.Driver.Session + ( DynFlags ) +#endif +#if MIN_VERSION_ghc(9,5,0) +import Language.Haskell.Syntax.Module.Name + ( moduleNameString ) +#else +import GHC.Unit.Module.Name + ( moduleNameString ) +#endif +import GHC.Unit.Types + ( unitIdString ) +import GHC.Utils.Panic + ( pgmErrorDoc ) +import GHC.Tc.Plugin + ( getTopEnv ) +import GHC.Types.Unique.FM + ( addToUFM, addToUFM_C, lookupUFM, plusUFM, unitUFM ) + +-- ghc-tcplugin-api +import GHC.TcPlugin.API + hiding ( Type ) +import GHC.TcPlugin.API.Internal + ( MonadTcPlugin(liftTcPluginM) ) + +-------------------------------------------------------------------------------- + +-- | A 'QualifiedName' is the name of something, +-- together with the names of the module and package it comes from. +data QualifiedName (thing :: Type) + = Qualified + { -- | Name of the thing (e.g. name of the 'TyCon' or 'Class'). + name :: String + -- | Name of the module in which the thing can be found. + , module' :: ModuleName + -- | Name of the package in which the module can be found. + , package :: PkgQual + } + +-- | Type-level parameter to 'Wear' type family, for higher-kinded data. +-- +-- @Wear Named thing@ is the identifier data passed in as an argument. +-- @Wear Resolved thing@ is the result of name resolving the thing. +-- +-- This allows users to pass a record of names, of type @MyData Named@, +-- and obtain a record of looked-up things, of type @MyData Resolved@. +-- +-- Refer to 'ResolveNames' for a worked example. +data NameResolution = Named | Resolved + +-- | Use this to refer to a @Promoted DataCon@. +data Promoted (thing :: k) :: Type + +-- | Type-family used for higher-kinded data pattern. +-- +-- This allows the same record to be re-used, +-- as explained in the worked example for 'ResolveNames'. +-- +-- For instance, if one defines: +-- +-- > data MyData n +-- > = MyData +-- > { myClass :: !( Wear n Class ) +-- > , myTyCon :: !( Wear n TyCon ) +-- > } +-- +-- then a record of type @MyData Named@ is simply a record of textual names +-- (a typeclass name and a type-constructor name, with associated module & packages), +-- whereas a record of type @MyData Resolved@ contains a typeclass's @Class@ +-- as well as a type-constructor's @TyCon@. +#if MIN_VERSION_ghc(9,0,0) +type Wear :: forall k. NameResolution -> k -> Type +#endif +type family Wear (n :: NameResolution) (thing :: k) :: Type where +#if MIN_VERSION_ghc(9,0,0) + Wear @Type Named thing = QualifiedName thing +#else + Wear Named thing = QualifiedName thing +#endif + Wear Resolved (Promoted DataCon) = TyCon + Wear Resolved (Promoted a) + = TypeError + ( Text "Cannot promote " :<>: ShowType a :<>: Text "." + :$$: Text "Can only promote 'DataCon's." + ) + Wear Resolved thing = thing + +-- | Retrieve the underlying thing being referred to by inspecting +-- the type parameter of 'QualifiedName'. +type family UnwearNamed (loc :: Type) :: Type where + UnwearNamed (QualifiedName thing) = thing + +-- | Type-class overloading things that can be looked up by name: +-- +-- * classes, +-- * data constructors (as well as their promotion), +-- * type-constructors. +#if MIN_VERSION_ghc(9,0,0) +type Lookupable :: forall {k}. k -> Constraint +#endif +class Lookupable (a :: k) where + mkOccName :: String -> OccName + lookup :: MonadTcPlugin m => Name -> m (Wear Resolved a) + +instance Lookupable TyCon where + mkOccName = mkTcOcc + lookup = tcLookupTyCon +instance Lookupable DataCon where + mkOccName = mkDataOcc + lookup = tcLookupDataCon +instance Lookupable Class where + mkOccName = mkClsOcc + lookup = tcLookupClass +instance Lookupable (Promoted DataCon) where + mkOccName = mkDataOcc + lookup = fmap promoteDataCon . tcLookupDataCon + +-- | This class exposes the method 'resolveNames' which will +-- perform name resolution for all the fields in a datatype. +-- +-- Example usage: we define a record that will hold +-- the things we want to look up, using the 'Wear' type family. +-- +-- For example: +-- +-- > data MyData n +-- > = MyData +-- > { myClass :: !( Wear n Class ) +-- > , myTyCon :: !( Wear n TyCon ) +-- > , myDataCon :: !( Wear n DataCon ) +-- > , myPromDataCon :: !( Wear n (Promoted DataCon) ) +-- > } +-- > deriving stock Generic +-- > deriving ResolveNames +-- > via Generically1 MyData +-- +-- Now we can specify the names of the things which we want to look up, +-- together with the modules and packages in which they belong: +-- +-- > myNames :: MyData Named +-- > myNames = MyData +-- > { myClass = QualifiedName "MyClass" "My.Module" ( Just "my-pkg-name" ) +-- > , ... +-- > } +-- +-- Then we can call 'resolveNames': +-- +-- > resolvedNames :: MonadTcPlugin m => m (MyData Resolved) +-- > resolvedNames = resolveNames myNames +-- +-- This returns a record containing the looked up things we want, +-- e.g. @myClass :: Class@, @myPromDataCon :: TyCon@, etc. +class ResolveNames (f :: NameResolution -> Type) where + resolve_names :: ( Coercible res ( f Resolved ), MonadTcPlugin m ) + => f Named -> m res + -- Workaround: the result is anything coercible to "f Resolved" rather than just "f Resolved", + -- because otherwise GHC complains when using DerivingVia that we don't know the role + -- of the parameter to m, despite the quantified constraint superclass to MonadTcPlugin. + -- + -- This unfortunately worsens type-inference, so we export + -- 'resolveNames' separately. + +-- | Resolve a collection of names. +-- +-- See 'ResolveNames' for further details. +resolveNames :: ( MonadTcPlugin m, ResolveNames f ) + => f Named -> m ( f Resolved ) +resolveNames = resolve_names + +instance ( Generic (f Named) + , Generic (f Resolved) + , GTraversableC ResolveName (Rep (f Named)) (Rep (f Resolved)) + ) + => ResolveNames (Generically1 f) where + resolve_names + :: forall +#if MIN_VERSION_ghc(9,0,0) + {m} +#else + m +#endif + res + . ( Coercible res ( Generically1 f Resolved ), MonadTcPlugin m ) + => Generically1 f Named -> m res + resolve_names ( Generically1 dat ) + = ( `evalStateT` emptyModules ) + $ coerce . to @(f Resolved) + <$> gtraverseC @ResolveName resolveName ( from dat ) + +-- | Type-class dispatch for looking up names. +-- +-- Every instance is of the form: +-- +-- > ResolveName (Wear Named thing) (Wear Resolved thing) +-- +-- which allows one to write 'resolveName': +-- +-- > resolveName :: ... => Wear Named thing -> m ( Wear Resolved thing ) +class ( a ~ Wear Named ( UnwearNamed a ) + , b ~ Wear Resolved ( UnwearNamed a ) + , Lookupable ( UnwearNamed a ) + ) + => ResolveName (a :: Type) (b :: Type) +instance ( a ~ Wear Named ( UnwearNamed a ) + , b ~ Wear Resolved ( UnwearNamed a ) + , Lookupable ( UnwearNamed a ) + ) + => ResolveName a b + +resolveName :: forall (thing :: Type) m + . ResolveName ( Wear Named thing ) ( Wear Resolved thing ) + => MonadTcPlugin m + => Wear Named thing + -> StateT ImportedModules m ( Wear Resolved thing ) +resolveName (Qualified str mod_name pkg) = do + md <- lookupModule pkg mod_name + nm <- lift $ lookupOrig md + (mkOccName +#if !MIN_VERSION_ghc(9,0,0) + @_ +#endif + @thing + str + ) + lift $ lookup +#if !MIN_VERSION_ghc(9,0,0) + @_ +#endif + @thing nm + +-------------------------------------------------------------------------------- +-- Caching of found modules. + +data ImportedModules + = ImportedModules + { home_modules :: UniqFM ModuleName Module + , this_pkg_modules :: UniqFM UnitId ( UniqFM ModuleName Module ) + , other_pkg_modules :: UniqFM UnitId ( UniqFM ModuleName Module ) + } + +emptyModules :: ImportedModules +emptyModules = + ImportedModules + { home_modules = emptyUFM + , this_pkg_modules = emptyUFM + , other_pkg_modules = emptyUFM + } + +lookupCachedModule :: Monad m => PkgQual -> ModuleName -> StateT ImportedModules m (Maybe Module) +lookupCachedModule NoPkgQual mod_name + = ( `lookupUFM` mod_name ) + . home_modules + <$> get +lookupCachedModule (ThisPkg pkg) mod_name + = ( ( `lookupUFM` mod_name ) =<< ) + . ( `lookupUFM` pkg ) + . this_pkg_modules + <$> get +lookupCachedModule (OtherPkg pkg) mod_name + = ( ( `lookupUFM` mod_name ) =<< ) + . ( `lookupUFM` pkg ) + . other_pkg_modules + <$> get + +insertCachedModule :: Monad m => PkgQual -> ModuleName -> Module -> StateT ImportedModules m () +insertCachedModule NoPkgQual mod_name md = do + mods@( ImportedModules { home_modules = prev } ) <- get + put $ mods { home_modules = addToUFM prev mod_name md } +insertCachedModule (ThisPkg pkg) mod_name md = do + mods@( ImportedModules { this_pkg_modules = prev } ) <- get + put $ mods { this_pkg_modules = addToUFM_C plusUFM prev pkg (unitUFM mod_name md) } +insertCachedModule (OtherPkg pkg) mod_name md = do + mods@( ImportedModules { other_pkg_modules = prev } ) <- get + put $ mods { other_pkg_modules = addToUFM_C plusUFM prev pkg (unitUFM mod_name md) } + +lookupModule :: MonadTcPlugin m => PkgQual -> ModuleName -> StateT ImportedModules m Module +lookupModule pkg mod_name = do + cachedResult <- lookupCachedModule pkg mod_name + case cachedResult of + Just res -> do + insertCachedModule pkg mod_name res + pure res + Nothing -> do + findResult <- lift $ findImportedModule mod_name pkg + case findResult of + Found _ res + -> pure res + other -> do + hsc_env <- lift . liftTcPluginM $ getTopEnv + let + err_doc :: SDoc +#if MIN_VERSION_ghc(9,2,0) + err_doc = cannotFindModule hsc_env mod_name other +#else + err_doc = cannotFindModule dflags mod_name other + dflags :: DynFlags + dflags = hsc_dflags hsc_env +#endif + pgmErrorDoc + ( "GHC.TcPlugin.API: could not find module " <> mod_str <> " in " <> pkg_name ) + err_doc + where + pkg_name, mod_str :: String + pkg_name = case pkg of + NoPkgQual -> "home package" + ThisPkg unit -> "home-unit package " <> unitIdString unit + OtherPkg unit -> "other unit package" <> unitIdString unit + mod_str = moduleNameString mod_name + +-------------------------------------------------------------------------------- +-- Constrained traversals. + +type TraversalC (c :: Type -> Type -> Constraint) (s :: Type) (t :: Type) + = forall f. ( Applicative f ) + => ( forall a b. c a b => a -> f b ) -> s -> f t + +class GTraversableC (c :: Type -> Type -> Constraint) (s :: Type -> Type) (t :: Type -> Type) where + gtraverseC :: TraversalC c (s x) (t x) + +instance + ( GTraversableC c l l' + , GTraversableC c r r' + ) => GTraversableC c (l :*: r) (l' :*: r') where + gtraverseC f (l :*: r) + = (:*:) <$> gtraverseC @c f l <*> gtraverseC @c f r + +instance + ( GTraversableC c l l' + , GTraversableC c r r' + ) => GTraversableC c (l :+: r) (l' :+: r') where + gtraverseC f (L1 l) = L1 <$> gtraverseC @c f l + gtraverseC f (R1 r) = R1 <$> gtraverseC @c f r + +instance GTraversableC c s t + => GTraversableC c (M1 i m s) (M1 i m t) where + gtraverseC f (M1 x) = M1 <$> gtraverseC @c f x + +instance GTraversableC c U1 U1 where + gtraverseC _ _ = pure U1 + +instance GTraversableC c V1 V1 where + gtraverseC _ = pure + +instance c a b => GTraversableC c (Rec0 a) (Rec0 b) where + gtraverseC f (K1 a) = K1 <$> f a + +-------------------------------------------------------------------------------- +-- Generically and Generically1 wrappers for DerivingVia. + +#if !MIN_VERSION_base(4,17,0) +-- | A type whose instances are defined generically, using the +-- 'Generic1' representation. 'Generically1' is a higher-kinded +-- version of 'Generically' that uses 'Generic'. +-- +-- Generic instances can be derived for type constructors via +-- @'Generically1' F@ using @-XDerivingVia@. +newtype Generically1 (f :: k -> Type) (a :: k) = Generically1 ( f a ) +#endif