ghc-tcplugin-api 0.8.3.0 → 0.20.1.1
raw patch · 8 files changed
Files
- changelog.md +203/−0
- ghc-tcplugin-api.cabal +35/−11
- src/GHC/Builtins.hs +130/−0
- src/GHC/TcPlugin/API.hs +625/−143
- src/GHC/TcPlugin/API/Internal.hs +186/−73
- src/GHC/TcPlugin/API/Internal/Shim.hs +142/−19
- src/GHC/TcPlugin/API/Names.hs +36/−58
- src/GHC/TcPlugin/API/TyConSubst.hs +537/−0
changelog.md view
@@ -1,3 +1,206 @@+# Version 0.20.1.1 (2026-11-03)++- Adapt to GHC HEAD `ModuleName` change (GHC commit 575c4bc6cb).++# Version 0.20.1.0 (2026-09-01)++- Add `cTupleTyConName` and `isCTupleTyConName` to the export list of+ `GHC.Builtins`.++# Version 0.20.0.0 (2026-09-01)++- Preliminary support for GHC 10.2 (with the known-entities refactor).++- The re-exports of `GHC.Builtin.Names`, `GHC.Builtin.Types` and+ `GHC.Builtin.Types.Prim` have been replaced by a single umbrella helper+ module, `GHC.Builtins`. Remarks:++ - GHC 10.2 no longer defines static `Name`s for known-key entities. Instead,+ these need to be resolved at runtime. Accordingly, `GHC.Builtins`+ exports `KnownKey` uniques such as `errorMessageTypeErrorFamKey` on+ GHC >= 10.2, instead of `Name`s such as `errorMessageTypeErrorFamName`.++ - The `MonadThings` class has been removed. Use `tcLookupTyCon`,+ `tcLookupDataCon` etc instead.++# Version 0.19.0.0 (2026-05-12)++- Starting from GHC 10.0, typechecker plugins are kept running during the+ desugaring phase, in order to improve the accuracy of pattern-match warnings.++ For this reason, the `tcPluginStop` function has been split into two:+ - `tcPluginPostTc`, for actions to run at the end of typechecking.+ - `tcPluginShutdown`, to shut down the plugin. This action runs in `IO`+ instead of a `TcM`-like monad.++ On GHC versions prior to 10.0, both of these actions will run at the end of+ typechecking, and typechecker plugins aren't invoked during pattern-match+ checking.++# Version 0.18.2.1 (2026-04-28)++- Add preliminary support for GHC 10.0.++# Version 0.18.2.0 (2025-01-14)++- Add a new function `ctsSubst` which computes a fix-point substitution from+ a collection of constraints which define a terminating generalised+ substitution. Mainly for use with the set of inert Given constraints.++- Re-export several functions to deal with substitutions: `substTy`,+ `substTys`, `extendTvSubst` and `mkTvSubstPrs`. Also re-export the `Subst`+ type (alias for `TCvSubst` on GHC <= 9.6).++# Version 0.18.1.0 (2025-10-09)++- Bugfix for v0.18.0.0: deal with constraints generated by unflattening+ in `splitTyConApp_upTo`. Fixes #19.++# Version 0.18.0.0 (2025-09-15)++- On GHC 9.0 and below, `ghc-tcplugin-api` will now automatically unflatten all+ Given constraints. That is, all flattening skolems `[G] fsk ~ F tys` will be+ substituted away, both in Givens and in Wanteds/Deriveds.++ No change for GHC 9.2 and above, as GHC stopped producing flattening variables+ from 9.2 onwards.++# Version 0.17.2.0 (2025-09-08)++- Fix the package failing to build on GHC 9.6.1 through 9.6.6 and+ on GHC 9.8.1 through 9.8.3. GHC versions 9.6.7 and 9.8.4 are unaffected.++# Version 0.17.1.0 (2025-08-27)++- Fix a regression, introduced in `0.17.0.0`, in which `splitTyConApp_upTo` would+ fail to take into account equalities of the form `tv1 ~ tv2`.++# Version 0.17.0.0 (2025-08-25)++- `splitTyConApp_upTo` now additionally returns a `[Coercion]` for tracking+ Given dependencies (which should be passed to functions such as `mkPluginUnivCo`,+ `mkPluginUnivEvTerm` and `mkTyFamAppReduction`).++# Version 0.16.2.0 (2025-08-22)++- `splitTyConApp_upTo` now correctly splits apart type families. This ensures+ it is a valid drop-in replacement for `splitTyConApp_maybe` (fixes issue #13).++# Version 0.16.1.0 (2025-07-18)++- Correctness fix for the `GHC.TcPlugin.API.TyConSubst` module: ensure that+ the `TyConSubst` does not mistake representational Given equalities for+ nominal equalities. For the time being, the `splitTyConApp_upTo` functionality+ only works at nominal role.++# Version 0.16.0.0 (2025-07-18)++- Re-export `tyConDataCons`, `tyConSingleDataCon_maybe`,+ `tyConSingleDataCon`, `dataConTyCon`, `isNewTyCon` and `isNewDataCon`+ from GHC.++- The `isWanted` function now correctly returns `False` for derived+ constraints. This is only relevant for GHC 9.2 and below.++- Add `GHC.TcPlugin.API.TyConSubst` module, which implements logic for+ recognising when a type is a `TyConApp` up to Given constraints.++# Version 0.15.0.0 (2025-06-03)++- Remove `tcPluginIO` in favour of new `MonadIO` instance. + To migrate, use `liftIO` instead of `tcPluginIO`.++- Add `lookupTHName` function, which allows looking up Template Haskell names+ in typechecker plugins. Useful in conjunction with `TemplateHaskellQuotes`.++- Helper functions to construct evidence terms have been adjusted to return+ values of type `EvExpr`, rather than `EvTerm`. This makes the functions more+ composable, and allows typechecker plugin to provide evidence for quantified+ constraints more easily.++ Affected functions: `evDFunApp`, `evDataConApp`, `evCast`.++ To migrate, you will need to manually wrap evidence terms with the+ `EvExpr` constructor in places that expect an `EvTerm`.++- Added `natKind`, `symbolKind` and `charKind` for the kinds of type-level+ `Nat`, `Symbol` and `Char`.++- Added several re-exports from the `ghc` library:+ - `isGiven` & `isWanted`.+ - `ctEvPred`, `ctEvId`, `ctEvExpr` and `ctEvLoc`.+ - `className` & `tyConName`.+ - `isEqPred` (unboxed equality) and `isEqClassPred` (boxed equality).+ - `evId` & `ctEvId`.+ - `typeKind`.+ - `nonDetCmpType`.++- Removed re-exports of `ctev_pred`, `ctev_loc`, `ctev_evar`, and `ctev_dest`.++ Migration: use `ctEvPred` instead of `ctev_pred` and `ctEvLoc` instead of `ctev_loc`.+ Uses of `ctev_evar` and `ctev_dest` should be covered by `ctEvEvId` and/or+ `ctEvExpr`.++# Version 0.14.0.0 (2024-11-28)++- Rename `mkPrimEqPredRole` to `mkEqPredRole`. This is a re-exported function+ from GHC, and the renaming adapts to the renaming in GHC-9.13.++# Version 0.13.0.0 (2024-10-30)++- Update to changes in the type of GHC's `mkUnivCo`+ in order to (properly) add support for GHC 9.12.++- Change `mkPluginUnivCo`, `mkPluginUnivEvTerm` and `mkTyFamAppReduction`+ to take a `[Coercion]` rather than a `DVarSet` for specifying dependencies.++- Stop re-exporting `DVarSet`, `emptyDVarSet`, `extendDVarSet`, `unionDVarSet`,+ `unitDVarSet`, and `mkDVarSet`.++- Update documentation to suggest using `ctEvCoercion`+ rather than `ctEvId` to specify coercions that a `UnivCo` depends on.++- Re-export `ctEvCoercion`, and stop re-exporting `ctEvId`.++# Version 0.12.0.0 (2024-10-22)++- Add preliminary support for GHC 9.12.++- `mkPluginUnivCo`, `mkPluginUnivEvTerm` and `mkTyFamAppReduction` now all take+ an additional `DVarSet` argument which allows specifying evidence that we+ depend on. This stops evidence terms being floated out past used enclosing+ Givens (see [GHC issue #23923](https://gitlab.haskell.org/ghc/ghc/-/issues/23923)).++- Re-export `DVarSet`, `emptyDVarSet`, `extendDVarSet`, `unionDVarSet`,+ `unitDVarSet`, and `mkDVarSet`, as well as `ctEvId`, in order to facilitate+ construction and manipulation of `DVarSet`s.++- Re-export `GHC.Types.Unique.Set`, `GHC.Types.Unique.DSet`.++# Version 0.11.0.0 (2023-08-29)++- Add support for GHC 9.8.++- Re-export functionality relating to GHC's constraint solving `TcS` monad,+ such as `{get,set}InertSet`, `{get,set}TcEvBindsMap`.++- Re-export `readTcRef` and `writeTcRef`.++# Version 0.10.0.0 (2023-02-28)++- Introduce `resolveImport`, and make `PkgQual` opaque.++- Rename `tcRewriterWanteds` to `tcRewriterNewWanteds`+ (bringing it in line with nomenclature in GHC 9.4).++# Version 0.9.0.0 (2023-01-24)++- Add support for GHC 9.6 and `transformers` 0.6.++- The `One` and `Many` pattern synonyms are now `OneTy` and `ManyTy`.++- Use `mkInvisFunTy`/`mkInvisFunTys` instead of `mkInvisFunTyMany`/`mkInvisFunTysMany`.+ # Version 0.8.3.0 (2022-10-05) - Bugfix for the GHC 9.0 rewriter plugin compatibility shim:
ghc-tcplugin-api.cabal view
@@ -1,12 +1,12 @@ cabal-version: 3.0 name: ghc-tcplugin-api-version: 0.8.3.0+version: 0.20.1.1 synopsis: An API for type-checker plugins. license: BSD-3-Clause build-type: Simple author: Sam Derbyshire maintainer: Sam Derbyshire-copyright: 2021 Sam Derbyshire+copyright: 2021-2025 Sam Derbyshire homepage: https://github.com/sheaf/ghc-tcplugin-api category: Type System, GHC, Plugin description:@@ -15,7 +15,7 @@ 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+ post-tc) 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.@@ -33,11 +33,17 @@ build-depends: base- >= 4.13.0 && < 4.19,+ >= 4.13.0 && < 5,+ array+ >= 0.5.3.0 && < 0.6,+ containers+ >= 0.6 && < 0.9, ghc- >= 8.8 && < 9.7,+ >= 8.8 && < 10.3, transformers- >= 0.5 && < 0.6,+ >= 0.5 && < 0.7,+ template-haskell+ >= 2.15 && < 3, default-language: Haskell2010@@ -56,18 +62,26 @@ exposed-modules: GHC.TcPlugin.API, GHC.TcPlugin.API.Names,- GHC.TcPlugin.API.Internal+ GHC.TcPlugin.API.TyConSubst, + GHC.TcPlugin.API.Internal,++ GHC.Builtins+ reexported-modules:- GHC.Builtin.Names- , GHC.Builtin.Types- , GHC.Builtin.Types.Prim- , GHC.Core.Make+ GHC.Core.Make , GHC.Plugins , GHC.Types.Unique.DFM , GHC.Types.Unique.FM+ , GHC.Types.Unique.Set+ , GHC.Types.Unique.DSet , GHC.Utils.Outputable + if impl(ghc >= 9.13.0)+ -- Don't warn on exports of the form "pattern ClassPred".+ -- We can migrate to using "data" when that becomes necessary.+ ghc-options: -Wno-pattern-namespace-specifier+ if impl(ghc >= 9.3.0) cpp-options: -DHAS_REWRITING else@@ -85,6 +99,7 @@ , PrelNames as GHC.Builtin.Names , TysWiredIn as GHC.Builtin.Types+ , TcTypeNats as GHC.Builtin.Types.Literals , TysPrim as GHC.Builtin.Types.Prim , CoreSyn as GHC.Core@@ -106,6 +121,8 @@ , DynFlags as GHC.Driver.Session , HscTypes as GHC.Driver.Types + , IfaceEnv as GHC.Iface.Env+ , GhcPlugins as GHC.Plugins , TcPluginM as GHC.Tc.Plugin@@ -121,10 +138,13 @@ , Literal as GHC.Types.Literal , Name as GHC.Types.Name , OccName as GHC.Types.Name.Occurrence+ , RdrName as GHC.Types.Name.Reader , SrcLoc as GHC.Types.SrcLoc , Unique as GHC.Types.Unique , UniqDFM as GHC.Types.Unique.DFM+ , UniqDSet as GHC.Types.Unique.DSet , UniqFM as GHC.Types.Unique.FM+ , UniqSet as GHC.Types.Unique.Set , Var as GHC.Types.Var , VarEnv as GHC.Types.Var.Env , VarSet as GHC.Types.Var.Set@@ -133,6 +153,7 @@ , Module as GHC.Unit.Module.Name , Module as GHC.Unit.Types + , FV as GHC.Utils.FV , Util as GHC.Utils.Misc , TcRnMonad as GHC.Utils.Monad , Outputable as GHC.Utils.Outputable@@ -146,6 +167,8 @@ ( Predicate as GHC.Core.Predicate , Constraint as GHC.Tc.Types.Constraint , TcOrigin as GHC.Tc.Types.Origin+ , GHC.ThToHs as GHC.ThToHs+ -- I forget what this last line does, but it is needed on GHC 9.10 ) else@@ -155,4 +178,5 @@ ( Type as GHC.Core.Predicate , TcRnTypes as GHC.Tc.Types.Constraint , TcRnTypes as GHC.Tc.Types.Origin+ , Convert as GHC.ThToHs )
+ src/GHC/Builtins.hs view
@@ -0,0 +1,130 @@+{-# LANGUAGE CPP #-}++-- | Helper umbrella re-exports of various known entities to GHC: known-key+-- uniques, wired-in types.+module GHC.Builtins+ ( -- * Known-key uniques+ hasKey+ , eqTyConKey, heqTyConKey, coercibleTyConKey+ , eqPrimTyConKey, eqReprPrimTyConKey, eqPhantPrimTyConKey++ -- * Custom type errors (prefer using 'GHC.TcPlugin.API.mkTcPluginErrorTy')+#if MIN_VERSION_ghc(10,1,0)+ , errorMessageTypeErrorFamKey+ , typeErrorTextDataConKey, typeErrorShowTypeDataConKey+ , typeErrorAppendDataConKey, typeErrorVAppendDataConKey+#else+ , errorMessageTypeErrorFamName+ , typeErrorTextDataConName, typeErrorShowTypeDataConName+ , typeErrorAppendDataConName, typeErrorVAppendDataConName+#endif++ -- * Equality and coercions+ , eqTyCon, heqTyCon, coercibleTyCon+ , eqPrimTyCon, eqReprPrimTyCon, eqPhantPrimTyCon+ , eqClass, heqClass, coercibleClass+ , eqDataCon, heqDataCon, coercibleDataCon+#if MIN_VERSION_ghc(8,10,0)+ , equalityTyCon+#endif++ -- * Kinds+ , liftedTypeKind, constraintKind, typeSymbolKind+ , unboxedTupleKind, unboxedSumKind+ , liftedTypeKindTyCon, constraintKindTyCon, tYPETyCon+ , anyTy, anyTyCon, anyTypeOfKind+#if MIN_VERSION_ghc(8,10,0)+ , typeToTypeKind+#endif+#if MIN_VERSION_ghc(9,1,0)+ , unliftedTypeKind+#endif+#if MIN_VERSION_ghc(9,3,0)+ , zeroBitTypeKind+#endif+#if MIN_VERSION_ghc(9,5,0)+ , tYPEKind, cONSTRAINTKind, cONSTRAINTTyCon, fUNTyCon+#endif++ -- * Runtime representations, levities and multiplicities+ , runtimeRepTy, runtimeRepTyCon, liftedRepTy+#if MIN_VERSION_ghc(9,0,0)+ , multiplicityTy, multiplicityTyCon+ , manyDataCon, oneDataCon, manyDataConTy, oneDataConTy+#endif+#if MIN_VERSION_ghc(9,1,0)+ , unliftedRepTy, boxedRepDataConTyCon, levityTyCon+ , liftedDataConTy, unliftedDataConTy+ , liftedDataConTyCon, unliftedDataConTyCon+#endif+#if MIN_VERSION_ghc(9,3,0)+ , levityTy, zeroBitRepTy+#endif++ -- * Wired-in types+ , unitTy, unitTyCon, unitDataCon, unitDataConId+ , boolTy, boolTyCon, trueDataCon, falseDataCon+ , promotedTrueDataCon, promotedFalseDataCon+ , orderingTyCon, promotedLTDataCon, promotedEQDataCon, promotedGTDataCon+ , charTy, charTyCon, charDataCon+ , intTy, intTyCon, intDataCon+ , wordTy, wordTyCon, wordDataCon+ , floatTy, floatTyCon, doubleTy, doubleTyCon+ , stringTy+ , listTyCon, nilDataCon, consDataCon+ , promotedNilDataCon, promotedConsDataCon+ , maybeTyCon, justDataCon, nothingDataCon+ , promotedJustDataCon, promotedNothingDataCon+#if MIN_VERSION_ghc(9,0,0)+ , integerTy, integerTyCon, naturalTy, naturalTyCon+#endif+#if !MIN_VERSION_ghc(9,1,0)+ , typeNatKind+#endif++ -- * Tuples and sums+ , tupleTyCon, tupleDataCon, promotedTupleDataCon+ , sumTyCon, sumDataCon+ , cTupleTyConName, isCTupleTyConName+ , mkTupleTy, mkBoxedTupleTy, mkSumTy+ , mkListTy, mkPromotedListTy+#if MIN_VERSION_ghc(8,10,0)+ , mkTupleTy1+#endif+#if MIN_VERSION_ghc(9,1,0)+ , cTupleTyCon, cTupleDataCon+ , mkMaybeTy, mkPromotedMaybeTy, mkPromotedPairTy+#endif+#if MIN_VERSION_ghc(9,5,0)+ , mkConstraintTupleTy+#endif++ -- * Type-level literals+ , typeNatTyCons, typeNatCoAxiomRules+ , typeNatAddTyCon, typeNatSubTyCon, typeNatMulTyCon, typeNatExpTyCon+ , typeNatDivTyCon, typeNatModTyCon, typeNatLogTyCon, typeNatCmpTyCon+ , typeSymbolCmpTyCon, typeSymbolAppendTyCon, typeSymbolKindCon+#if MIN_VERSION_ghc(9,1,0)+ , typeConsSymbolTyCon, typeUnconsSymbolTyCon+ , typeCharCmpTyCon, typeCharToNatTyCon, typeNatToCharTyCon+#endif++ -- * Primitive types+ , intPrimTy, wordPrimTy, charPrimTy, floatPrimTy, doublePrimTy+ , realWorldTy, realWorldTyCon, realWorldStatePrimTy+ , mkStatePrimTy, mkProxyPrimTy, proxyPrimTyCon+ )+ where++-- ghc+#if MIN_VERSION_ghc(10,1,0)+import GHC.Builtin.KnownKeys+import GHC.Builtin.WiredIn.Prim+import GHC.Builtin.WiredIn.TypeLits+import GHC.Builtin.WiredIn.Types+#else+import GHC.Builtin.Names+import GHC.Builtin.Types+import GHC.Builtin.Types.Literals+import GHC.Builtin.Types.Prim+#endif
src/GHC/TcPlugin/API.hs view
@@ -1,12 +1,20 @@ {-# LANGUAGE CPP #-}++{-# LANGUAGE BangPatterns #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE DuplicateRecordFields #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE UndecidableInstances #-} +#if !MIN_VERSION_ghc(8,11,0)+{-# OPTIONS_GHC -Wno-orphans #-}+#endif+ {-| Module: GHC.TcPlugin.API @@ -63,7 +71,6 @@ -- typeclass providing overloading (for operations that work in all stages). , TcPluginStage(..), MonadTcPlugin , TcPluginM- , tcPluginIO -- *** Emitting new work, and throwing type-errors @@ -79,11 +86,27 @@ -- | 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@:+ -- The most convenient way to look up a Name is to bring the name into scope+ -- in the module defining the plugin, and use @TemplateHaskellQuotes@+ -- in conjunction with the 'lookupTHName' function. --- -- > lookupMyModule :: MonadTcPlugin m => m Module- -- > lookupMyModule = do- -- > findResult <- findImportedModule ( mkModuleName "MyModule" ) ( Just $ fsLit "my-pkg" )+ -- > import Data.Maybe+ -- >+ -- > lookupMaybeTyCon :: MonadTcPluginM m => m TyCon+ -- > lookupMaybeTyCon = lookupTHName ''Maybe >>= tcLookupTyCon+ --+ -- This is recommended over manually looking up the package and module+ -- name, because the manual method does not robustly deal with re-exports;+ -- one must specify the exact package/module which defines the identifier.+ -- For instance, to manually lookup the type family @MyFam@ in module+ -- @MyModule@ in package @my-pkg@:+ --+ -- > lookupMyFam :: MonadTcPluginM m => m Name+ -- > lookupMyFam = do+ -- > let modlName = mkModuleName "MyModule"+ -- > pkgName = Just $ fsLit "my-pkg"+ -- > pkgQual <- resolveImport modlName pkgName+ -- > findResult <- findImportedModule modlName pkgQual -- > case findResult of -- > Found _ myModule -> pure myModule -- > _ -> error "MyPlugin couldn't find MyModule in my-pkg"@@ -95,31 +118,38 @@ -- 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+ -- ** Name resolution: TH method + -- | Look up a Name from a Template Haskell Name (e.g. a Name constructed+ -- using TemplateHaskellQuotes).+ , lookupTHName++ -- ** Name resolution: manual method+ -- *** 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(..)+ , findImportedModule, resolveImport, fsLit, unpackFS, mkModuleName+ , unitIdFS, stringToUnitId, pkgQualToPkgName+ , Module, ModuleName, FindResult(..), UnitId, PkgQual - -- ** Names+ -- *** Names - -- *** Occurence 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+ -- **** 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+ -- ** Name resolution: resolving the Name to a '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@@ -237,10 +267,15 @@ , isSkolemTyVar , isMetaTyVar, isFilledMetaTyVar_maybe , writeMetaTyVar+ , readTcRef, writeTcRef -- | == Some further functions for inspecting constraints- , eqType+ , eqType, nonDetCmpType , ctLoc, ctEvidence, ctFlavour, ctEqRel, ctOrigin+ , ctEvPred, ctEvId, ctEvExpr, ctEvLoc+ , isGiven, isWanted+ , isEqPred, isEqClassPred+ , className, tyConName -- ** Constraint evidence @@ -254,6 +289,20 @@ , mkReflCo, mkSymCo, mkTransCo, mkUnivCo , mkCoercionTy, isCoercionTy, isCoercionTy_maybe + -- *** Depending on outer Givens++ -- | When a plugin returns a coercion that depends on outer Given constraints,+ -- it should declare this dependency using the '[Coercion]' argument to+ -- functions such as 'mkPluginUnivCo', 'mkPluginUnivEvTerm' and 'mkTyFamAppReduction'+ -- in order to avoid this coercion getting floated out past such enclosing+ -- Givens.+ --+ -- You can use 'ctEvCoercion' to obtain the coercion underlying an equality+ -- constraint (whether Given or Wanted). It is not possible to declare+ -- a dependency on non-equality constraints, and calling 'ctEvCoercion'+ -- on a non-equality constraint will cause a crash.+ , ctEvCoercion+ -- *** Evidence terms -- | Typeclass constraints have a different notion of evidence: evidence terms.@@ -263,13 +312,11 @@ -- by combining evidence that is already available. , mkPluginUnivEvTerm- , evDataConApp+ , evDFunApp, evDataConApp , newEvVar, setEvBind- , evCoercion, evCast- , ctEvExpr+ , evId, evCoercion, evCast , askEvBinds, lookupEvBind, eb_lhs, eb_rhs , newName, mkLocalId, mkTyVar- , ctev_pred, ctev_evar, ctev_loc, ctev_dest -- *** Class dictionaries @@ -303,7 +350,7 @@ -- | The following functions allow plugins to create constraints -- for typeclasses and type equalities.- , mkClassPred, mkPrimEqPredRole+ , mkClassPred, mkEqPredRole -- | === Deriveds @@ -376,23 +423,39 @@ -- ** Type literals (natural numbers, type-level strings) , mkNumLitTy, isNumLitTy , mkStrLitTy, isStrLitTy+ , natKind, symbolKind, charKind -- ** Creating and decomposing applications , mkTyConTy, mkTyConApp, mkAppTy, mkAppTys , splitTyConApp_maybe , tyConAppTyConPicky_maybe, tyConAppTyCon_maybe , splitAppTy_maybe, splitAppTys+ , isNewTyCon, dataConTyCon + -- ** Data constructors+ , tyConDataCons, tyConSingleDataCon_maybe, tyConSingleDataCon+ , isNewDataCon+ -- ** Function types , mkVisFunTyMany, mkVisFunTysMany- , mkInvisFunTyMany, mkInvisFunTysMany+ , mkInvisFunTy, mkInvisFunTys , mkForAllTy, mkForAllTys , mkPiTy, mkPiTys + -- ** Kinds+ , typeKind+ #if MIN_VERSION_ghc(9,0,0)- , Mult, pattern One, pattern Many+ , Mult+ , pattern OneTy, pattern ManyTy #endif + -- ** Substitution+ , Subst+ , substTy, substTys+ , mkTvSubstPrs, extendTvSubst+ , ctsSubst+ -- ** Zonking -- | Zonking is the operation in which GHC actually switches out mutable unification variables@@ -422,6 +485,11 @@ -- * The type-checking environment , getEnvs + -- * Interacting with GHC's constraint solver+ , TcS+ , InertSet, getInertSet, setInertSet+ , getTcEvBindsMap, setTcEvBindsMap+ -- * Built-in types -- | This module also re-exports the built-in types that GHC already knows about.@@ -443,7 +511,6 @@ -- | == Names , Name, OccName, TyThing, TcTyThing- , MonadThings(..) , Class(classTyCon), DataCon, TyCon, Id , FastString @@ -474,23 +541,31 @@ ) where +-- base+import Prelude+ hiding ( cos )+#if !MIN_VERSION_base(4,20,0)+import Data.Foldable+ ( foldl' )+#endif+#if !MIN_VERSION_ghc(8,11,0)+import Data.List.NonEmpty+ ( NonEmpty(..) )+#endif+import Data.Maybe+ ( mapMaybe )+ -- 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(..) )+ ( CoreBndr, CoreExpr, Expr(..), mkTyApps, mkApps ) import GHC.Core.Class ( Class(..), FunDep ) import GHC.Core.Coercion ( mkReflCo, mkSymCo, mkTransCo- , mkUnivCo-#if MIN_VERSION_ghc(8,10,0)+ , mkUnivCo, isReflCo+#if !MIN_VERSION_ghc(9,13,0) && MIN_VERSION_ghc(8,10,0) , mkPrimEqPredRole #endif )@@ -498,7 +573,11 @@ ( Role(..) ) import GHC.Core.DataCon ( DataCon- , classDataCon, promoteDataCon+ , classDataCon, promoteDataCon, dataConWrapId+ , dataConTyCon+#if MIN_VERSION_ghc(9,1,0)+ , isNewDataCon+#endif ) import GHC.Core.FamInstEnv ( FamInstEnv )@@ -510,6 +589,9 @@ #endif import GHC.Core.Predicate ( EqRel(..)+#if MIN_VERSION_ghc(9,13,0)+ , mkEqPredRole+#endif #if MIN_VERSION_ghc(8,10,0) , Pred(..) #else@@ -523,7 +605,14 @@ ( Reduction(..) ) #endif import GHC.Core.TyCon- ( TyCon(..) )+ ( TyCon(..), tyConClass_maybe+ , tyConDataCons, tyConSingleDataCon_maybe, tyConSingleDataCon+ , isNewTyCon+ )+#if MIN_VERSION_ghc(9,6,0)+import GHC.Core.TyCo.Compare+ ( eqType )+#endif import GHC.Core.TyCo.Rep ( Type, PredType, Kind , Coercion(..), CoercionHole(..)@@ -531,7 +620,11 @@ #if MIN_VERSION_ghc(9,0,0) , Mult , mkVisFunTyMany, mkVisFunTysMany+#if MIN_VERSION_ghc(9,6,0)+ , mkInvisFunTy, mkInvisFunTys+#else , mkInvisFunTyMany, mkInvisFunTysMany+#endif #elif MIN_VERSION_ghc(8,10,0) , mkVisFunTy, mkVisFunTys , mkInvisFunTy, mkInvisFunTys@@ -546,20 +639,70 @@ , mkForAllTy, mkForAllTys ) import GHC.Core.Type- ( eqType, mkTyConTy, mkTyConApp, splitTyConApp_maybe+ ( 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)+ , typeKind+#if !MIN_VERSION_ghc(9,6,0)+ , eqType+#endif+#if MIN_VERSION_ghc(9,6,0)+ , pattern OneTy, pattern ManyTy+#elif MIN_VERSION_ghc(9,0,0) , pattern One, pattern Many #endif+ , TvSubstEnv+#if MIN_VERSION_ghc(9,6,0)+ , Subst+#else+ , TCvSubst+#endif ) import GHC.Data.FastString ( FastString, fsLit, unpackFS )+#if MIN_VERSION_ghc(9,5,0)+import GHC.Plugins+ ( thNameToGhcNameIO )+#else+import Data.Maybe+ ( listToMaybe )+#if MIN_VERSION_ghc(9,3,0)+import GHC.Iface.Env+ ( lookupNameCache )+#else+import GHC.Iface.Env+ ( lookupOrigIO )+#endif+import GHC.ThToHs+ ( thRdrNameGuesses )+import GHC.Types.Name+ ( isExternalName )+import GHC.Types.Name.Reader+ ( isExact_maybe, isOrig_maybe )+import GHC.Utils.Monad+ ( mapMaybeM )+#endif import qualified GHC.Tc.Plugin as GHC+#if MIN_VERSION_ghc(9,4,0)+import GHC.Tc.Solver.InertSet+ ( InertSet )+#endif+import GHC.Tc.Solver.Monad+ ( TcS+#if !MIN_VERSION_ghc(9,4,0)+ , InertSet+#endif+#if MIN_VERSION_ghc(9,8,0)+ , getInertSet, updInertSet+#else+ , getTcSInerts, setTcSInerts+#endif+ , getTcEvBindsMap, setTcEvBindsMap+ ) import GHC.Tc.Types ( TcTyThing(..), TcGblEnv(..), TcLclEnv(..) #if HAS_REWRITING@@ -567,28 +710,51 @@ , RewriteEnv(..) #endif )+#if MIN_VERSION_ghc(9,11,0)+import GHC.Tc.Types.CtLoc+ ( CtLoc(..), bumpCtLocDepth )+#else import GHC.Tc.Types.Constraint- ( Ct(..), CtLoc(..), CtEvidence(..), CtFlavour(..)+ ( CtLoc(..), bumpCtLocDepth )+#endif+#if MIN_VERSION_ghc(9,13,0)+import GHC.Tc.Types.Constraint+ ( GivenCtEvidence(..) )+#endif+import GHC.Tc.Types.Constraint+ ( Ct(..), CtEvidence(..), CtFlavour(..) , QCInst(..), TcEvDest(..) , ctPred, ctLoc, ctEvidence, ctEvExpr+ , ctEvCoercion , ctFlavour, ctEqRel, ctOrigin- , bumpCtLocDepth- , mkNonCanonical+ , ctEvFlavour, ctEvPred, ctEvLoc+ , mkNonCanonical, ctEvId ) import GHC.Tc.Types.Evidence ( EvBind(..), EvTerm(..), EvExpr, EvBindsVar(..)- , evCoercion, evCast, lookupEvBind, evDataConApp+ , evCoercion, lookupEvBind+ , mkGivenEvBind, evId ) import GHC.Tc.Types.Origin ( CtOrigin(..) ) import GHC.Tc.Utils.Monad- ( newName )+ ( newName, readTcRef, writeTcRef ) import qualified GHC.Tc.Utils.Monad as GHC ( traceTc, setCtLocM ) import GHC.Tc.Utils.TcType ( TcType, TcLevel, MetaDetails, MetaInfo , isSkolemTyVar, isMetaTyVar+ , nonDetCmpType+ , mkTvSubst, extendTvSubst+ , substTy, substTys, mkTvSubstPrs+ , tyCoVarsOfTypes+ , scopedSort+#if MIN_VERSION_ghc(9,15,0)+ , tyCoVarsOfTypes+#else+ , tyCoFVsOfTypes+#endif ) import GHC.Tc.Utils.TcMType ( isFilledMetaTyVar_maybe, writeMetaTyVar )@@ -608,9 +774,25 @@ ( OccName(..) , mkVarOcc, mkDataOcc, mkTyVarOcc, mkTcOcc, mkClsOcc )+#if MIN_VERSION_ghc(9,1,0)+import GHC.Driver.Env.Types+ ( HscEnv )+#else+import GHC.Driver.Types+ ( HscEnv )+#endif #if MIN_VERSION_ghc(9,3,0)+import GHC.Driver.Env.Types+ ( hsc_unit_env, hsc_NC ) import GHC.Types.PkgQual ( PkgQual(..) )+import GHC.Rename.Names+ ( renamePkgQual )+import GHC.Unit.Module+ ( unitIdString )+#elif MIN_VERSION_ghc(9,1,0)+import GHC.Data.FastString+ ( NonDetFastString(NonDetFastString) ) #endif import GHC.Types.SrcLoc ( GenLocated(..), Located, RealLocated@@ -618,33 +800,39 @@ ) import GHC.Types.Unique ( Unique )+-- UniqFM didn't have the first argument in GHC < 9.0.+-- This adds a little compatibility shim for that. #if MIN_VERSION_ghc(9,0,0) import GHC.Types.Unique.FM as UniqFM- ( UniqFM, emptyUFM, listToUFM )+ ( UniqFM ) #else import qualified GHC.Types.Unique.FM as GHC ( UniqFM )-import GHC.Types.Unique.FM as UniqFM- ( emptyUFM, listToUFM ) #endif+import GHC.Types.Unique.FM+ ( emptyUFM, listToUFM, nonDetEltsUFM ) import GHC.Types.Unique.DFM ( UniqDFM, lookupUDFM, lookupUDFM_Directly, elemUDFM ) import GHC.Types.Var ( TyVar, CoVar, TcTyVar, EvVar- , mkTyVar+ , mkTyVar, DFunId, isTyVar, updateTyVarKind )-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+import GHC.Types.Var.Env+ ( InScopeSet, mkInScopeSet, mapVarEnv, elemVarEnv )+import GHC.Types.Var.Set+ ( mkVarSet, unionVarSet+#if MIN_VERSION_ghc(9,15,0)+ , nonDetVarSetElems #endif )+import GHC.Utils.Outputable+ ( Outputable(..), SDoc, text ) #if MIN_VERSION_ghc(9,2,0) import GHC.Utils.Panic ( panic, pprPanic )+#else+import GHC.Utils.Outputable+ ( panic, pprPanic ) #endif #if MIN_VERSION_ghc(9,2,0) import GHC.Unit.Finder@@ -654,33 +842,52 @@ ( 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+ ( ModuleName, mkModuleName+ , UnitId, unitIdFS, stringToUnitId+ ) import GHC.Unit.Types ( Module )---- transformers-import Control.Monad.IO.Class- ( MonadIO ( liftIO ) )+#if MIN_VERSION_ghc(9,0,0) && !MIN_VERSION_ghc(9,5,0)+import GHC.Utils.Misc+ ( HasDebugCallStack )+#endif+#if MIN_VERSION_ghc(9,15,0)+#else+import GHC.Utils.FV+ ( fvVarList )+#endif+import GHC.Utils.Misc+ ( filterOut ) -- ghc-tcplugin-api+import GHC.Builtins+ ( hasKey+ , eqPrimTyConKey, eqReprPrimTyConKey+ , heqTyConKey, eqTyConKey, coercibleTyConKey+ , typeSymbolKind, charTy+#if MIN_VERSION_ghc(9,1,0)+ , naturalTy+#else+ , typeNatKind+#endif+#if !MIN_VERSION_ghc(9,0,0)+ , intDataCon, intPrimTy+#endif+ ) import GHC.TcPlugin.API.Internal #ifndef HAS_REWRITING import GHC.TcPlugin.API.Internal.Shim #endif ---------------------------------------------------------------------------------+-- template-haskell+import qualified Language.Haskell.TH as TH --- | Run an 'IO' computation within the plugin.-tcPluginIO :: MonadTcPlugin m => IO a -> m a-tcPluginIO = unsafeLiftTcM . liftIO+-- transformers+import Control.Monad.IO.Class+ ( MonadIO ( liftIO ) ) +--------------------------------------------------------------------------------+ -- | Output some debugging information within the plugin. tcPluginTrace :: MonadTcPlugin m => String -- ^ Text at the top of the debug message.@@ -690,54 +897,86 @@ -------------------------------------------------------------------------------- -#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 )+#if MIN_VERSION_ghc(9,0,0) && !MIN_VERSION_ghc(9,5,0)+pattern OneTy, ManyTy :: Mult+pattern OneTy = One+pattern ManyTy = Many -instance Outputable PkgQual where- ppr = \case- NoPkgQual -> empty- ThisPkg u -> doubleQuotes (ppr u)- OtherPkg u -> doubleQuotes (ppr u)+mkInvisFunTy :: HasDebugCallStack => Type -> Type -> Type+mkInvisFunTy = mkInvisFunTyMany++mkInvisFunTys :: HasDebugCallStack => [Type] -> Type -> Type+mkInvisFunTys = mkInvisFunTysMany #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++-- Use PkgQual from ghc itself++#elif MIN_VERSION_ghc(9,1,0)++newtype PkgQual = PkgQual (Maybe NonDetFastString)+ deriving stock ( Eq, Ord )+ deriving newtype ( Outputable )++-- | INTERNAL: Unwrap 'PkgQual'+getPkgQual :: PkgQual -> Maybe FastString+getPkgQual (PkgQual Nothing) = Nothing+getPkgQual (PkgQual (Just (NonDetFastString pkg))) = Just pkg+ #else- -> Maybe FastString++newtype PkgQual = PkgQual (Maybe FastString)+ deriving stock ( Eq, Ord )+ deriving newtype ( Outputable )++-- | INTERNAL: Unwrap 'PkgQual'+getPkgQual :: PkgQual -> Maybe FastString+getPkgQual (PkgQual mPkg) = mPkg+ #endif-pkgQual_pkg pkg =++-- | Get package name from package qualifier+pkgQualToPkgName :: PkgQual -> Maybe String #if MIN_VERSION_ghc(9,3,0)- pkg+pkgQualToPkgName NoPkgQual = Nothing+pkgQualToPkgName (ThisPkg unit) = Just $ unitIdString unit+pkgQualToPkgName (OtherPkg unit) = Just $ unitIdString unit #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+pkgQualToPkgName = fmap unpackFS . getPkgQual #endif --- | Lookup a Haskell module from the given package.+-- | Resolve import+resolveImport :: MonadTcPlugin m+ => ModuleName -- ^ Module name to import from+ -> Maybe FastString -- ^ Optional package qualifier+ -> m PkgQual+#if MIN_VERSION_ghc(9,3,0)+resolveImport mod_name mPkg = do+ hscEnv <- getTopEnv+ return $ renamePkgQual (hsc_unit_env hscEnv) mod_name mPkg+#elif MIN_VERSION_ghc(9,1,0)+resolveImport _mod_name mPkg = do+ return $ PkgQual (NonDetFastString <$> mPkg)+#else+resolveImport _mod_name mPkg = do+ return $ PkgQual mPkg+#endif++-- | Lookup a Haskell module, with an optional package qualifier. findImportedModule :: MonadTcPlugin m- => ModuleName -- ^ Module name, e.g. @"Data.List"@.- -> PkgQual -- ^ Package name, e.g. @Just "base"@.- -- Use @Nothing@ for the current home package+ => ModuleName -- ^ Module name, e.g. @"Data.List"@+ -> PkgQual -- ^ Package qualifier. See 'resolveImport' -> m FindResult-findImportedModule mod_name pkg- = liftTcPluginM- $ GHC.findImportedModule mod_name (pkgQual_pkg pkg)+#if MIN_VERSION_ghc(9,3,0)+findImportedModule mod_name pkg = liftTcPluginM $+ GHC.findImportedModule mod_name pkg+#else+findImportedModule mod_name pkg = liftTcPluginM $+ GHC.findImportedModule mod_name (getPkgQual pkg)+#endif -- | Obtain the full internal 'Name' (with its unique identifier, etc) from its 'OccName'. --@@ -778,10 +1017,68 @@ -------------------------------------------------------------------------------- -{-+#if !MIN_VERSION_ghc(9,6,0)+type Subst = TCvSubst+#endif++-- | Compute an idempotent substitution from a collection of constraints, in+-- particular from inert Givens.+--+-- NB: don't pass any set of constraints to this function; they should form a+-- terminating generalised substitution as in Note [inert_eqs: the inert equalities]+-- in GHC.Tc.Solver.InertSet.+ctsSubst :: [Ct] -> Subst+ctsSubst cts = niFixSubst inScope $ listToUFM prs+ where+ toSubstPair ct =+ case classifyPredType (ctEvPred (ctEvidence ct)) of+ EqPred NomEq t1 t2+ | Just tv <- getTyVar_maybe t1+ -- NB: deliberately don't re-orient constraints: we are only+ -- guaranteed a terminating substitution by keeping the orientation.+ -> Just (tv, t2)+ _ -> Nothing+ prs = mapMaybe toSubstPair cts+ inScope =+ mkInScopeSet $+ mkVarSet (map fst prs)+ `unionVarSet`+ tyCoVarsOfTypes (map snd prs)++-- NB: copied from GHC, as GHC doesn't export this function.+niFixSubst :: InScopeSet -> TvSubstEnv -> Subst+niFixSubst in_scope tenv+ | not_fixpoint = niFixSubst in_scope (mapVarEnv (substTy subst) tenv)+ | otherwise = tenv_subst+ where+ tenv_subst = mkTvSubst in_scope tenv++ range_tvs :: [TyVar]+ range_tvs =+#if MIN_VERSION_ghc(9,15,0)+ nonDetVarSetElems $ tyCoVarsOfTypes+#else+ fvVarList $ tyCoFVsOfTypes+#endif+ $ nonDetEltsUFM tenv++ not_fixpoint = any in_domain range_tvs+ in_domain tv = tv `elemVarEnv` tenv++ free_tvs = scopedSort (filterOut in_domain range_tvs)++ subst = foldl' add_free_tv tenv_subst free_tvs++ add_free_tv subst0 tv+ | isTyVar tv = extendTvSubst subst0 tv (mkTyVarTy tv')+ | otherwise = subst0+ where+ tv' = updateTyVarKind (substTy subst0) tv++--------------------------------------------------------------------------------+ getTopEnv :: MonadTcPlugin m => m HscEnv getTopEnv = liftTcPluginM GHC.getTopEnv--} -- | Obtain the current global and local type-checking environments. getEnvs :: MonadTcPlugin m => m ( TcGblEnv, TcLclEnv )@@ -841,6 +1138,20 @@ -------------------------------------------------------------------------------- +-- | Is this a "Given" constraint?+isGiven :: CtEvidence -> Bool+isGiven ev = case ctEvFlavour ev of+ Given {} -> True+ _ -> False++-- | Is this a "Wanted" constraint?+isWanted :: CtEvidence -> Bool+isWanted ev = case ctEvFlavour ev of+ Wanted {} -> True+ _ -> False++--------------------------------------------------------------------------------+ -- | Create a new Wanted constraint. -- -- Requires a location (so that error messages can say where the constraint came from,@@ -858,15 +1169,19 @@ -- | Create a new Given constraint. -- -- Unlike 'newWanted', we need to supply evidence for this constraint.-newGiven :: CtLoc -> PredType -> EvExpr -> TcPluginM Solve CtEvidence+newGiven :: CtLoc -> PredType -> EvTerm -> 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+ new_ev <- newEvVar pty+ setEvBind $ mkGivenEvBind new_ev evtm+ return $+ CtGiven+#if MIN_VERSION_ghc(9,13,0)+ $ GivenCt #endif-+ { ctev_pred = pty+ , ctev_evar = new_ev+ , ctev_loc = loc+ } -- | Obtain the 'CtLoc' from a 'RewriteEnv'. --@@ -922,12 +1237,21 @@ -- 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)+ :: String -- ^ Name of equality (for the plugin's internal use, or for debugging) -> Role- -> TcType -- ^ LHS- -> TcType -- ^ RHS+ -> [Coercion] -- ^ Evidence that this proof term depends on (use 'ctEvCoercion')+ -> TcType -- ^ LHS+ -> TcType -- ^ RHS -> Coercion-mkPluginUnivCo str role lhs rhs = mkUnivCo ( PluginProv str ) role lhs rhs+mkPluginUnivCo str role _deps lhs rhs =+ mkUnivCo+ ( PluginProv str )+#if MIN_VERSION_ghc(9,12,0)+ _deps+#endif+ role+ lhs+ rhs -- | Conjure up an evidence term for an equality between two types -- at the given 'Role' ('Nominal' or 'Representational').@@ -937,12 +1261,14 @@ -- 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)+ :: String -- ^ Name of equality (for the plugin's internal use, or for debugging) -> Role- -> TcType -- ^ LHS- -> TcType -- ^ RHS+ -> [Coercion] -- ^ Evidence that this proof term depends on (use 'ctEvCoercion')+ -> TcType -- ^ LHS+ -> TcType -- ^ RHS -> EvTerm-mkPluginUnivEvTerm str role lhs rhs = evCoercion $ mkPluginUnivCo str role lhs rhs+mkPluginUnivEvTerm str role deps lhs rhs =+ evCoercion $ mkPluginUnivCo str role deps lhs rhs -- | Provide a rewriting of a saturated type family application -- at the given 'Role' ('Nominal' or 'Representational').@@ -950,14 +1276,17 @@ -- 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+ :: String -- ^ Name of reduction (for debugging)+ -> Role -- ^ Role of reduction ('Nominal' or 'Representational')+ -> [Coercion] -- ^ Evidence that this reduction depends on (use 'ctEvCoercion')+ -> 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+mkTyFamAppReduction str role deps tc args ty =+ Reduction+ ( mkPluginUnivCo str role deps ( mkTyConApp tc args ) ty )+ ty -------------------------------------------------------------------------------- @@ -972,34 +1301,187 @@ #if MIN_VERSION_ghc(8,10,0) -mkInvisFunTyMany, mkVisFunTyMany :: Type -> Type -> Type-mkInvisFunTyMany = mkInvisFunTy-mkVisFunTyMany = mkVisFunTy+mkVisFunTyMany :: Type -> Type -> Type+mkVisFunTyMany = mkVisFunTy -mkInvisFunTysMany, mkVisFunTysMany :: [Type] -> Type -> Type-mkInvisFunTysMany = mkInvisFunTys-mkVisFunTysMany = mkVisFunTys+mkVisFunTysMany :: [Type] -> Type -> Type+mkVisFunTysMany = mkVisFunTys #else type Pred = PredTree -mkInvisFunTyMany, mkVisFunTyMany :: Type -> Type -> Type-mkInvisFunTyMany = mkFunTy-mkVisFunTyMany = mkFunTy+mkInvisFunTy, mkVisFunTyMany :: Type -> Type -> Type+mkInvisFunTy = mkFunTy+mkVisFunTyMany = mkFunTy -mkInvisFunTysMany, mkVisFunTysMany :: [Type] -> Type -> Type-mkInvisFunTysMany = mkFunTys+mkInvisFunTys, mkVisFunTysMany :: [Type] -> Type -> Type+mkInvisFunTys = 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 +--------------------------------------------------------------------------------++#if !MIN_VERSION_ghc(9,13,0)+-- | Makes an unlifted equality predicate at the given role+-- (either 'Nominal' or 'Representational').+mkEqPredRole :: Role -> Type -> Type -> PredType+#if MIN_VERSION_ghc(8,10,0)+mkEqPredRole = mkPrimEqPredRole+#else+mkEqPredRole Nominal = mkPrimEqPred+mkEqPredRole Representational = mkReprPrimEqPred+mkEqPredRole Phantom = panic "mkPrimEqPredRole phantom" #endif #endif++--------------------------------------------------------------------------------++#if !MIN_VERSION_ghc(9,1,0)+isNewDataCon :: DataCon -> Bool+isNewDataCon dc = isNewTyCon (dataConTyCon dc)+#endif++#if !MIN_VERSION_ghc(8,11,0)+instance Outputable a => Outputable (NonEmpty a) where+ ppr (x :| xs) = ppr (x : xs)+#endif++--------------------------------------------------------------------------------++#if MIN_VERSION_ghc(9,8,0)+setInertSet :: InertSet -> TcS ()+setInertSet inerts = updInertSet ( const inerts )+ -- workaround for setInertSet not being exported++#elif !MIN_VERSION_ghc(9,8,0)+getInertSet :: TcS InertSet+getInertSet = getTcSInerts++setInertSet :: InertSet -> TcS ()+setInertSet = setTcSInerts+#endif++--------------------------------------------------------------------------------++-- | Resolve a @template-haskell@ 'TH.Name' to a GHC 'Name'.+--+-- Especially useful in conjunction with @TemplateHaskellQuotes@, e.g. to+-- look up the 'Name' of the @Maybe@ type constructor, you can do:+--+-- > lookupName ''Maybe+--+-- @since 0.15.0.0+lookupTHName :: ( Monad (TcPluginM s), MonadTcPlugin (TcPluginM s) )+ => TH.Name -> TcPluginM s Name+lookupTHName thNm = do+ hscEnv <- getTopEnv+ mbNm <-+ liftIO $+ thNameToGhcNameIO+#if MIN_VERSION_ghc(9,6,0)+ (hsc_NC hscEnv)+#else+ hscEnv+#endif+ thNm+ case mbNm of+ Just nm ->+ return nm+ Nothing ->+ pprPanic "lookupTHName: lookup failed" (text $ show thNm)++--------------------------------------------------------------------------------++-- | Apply an instance dictionary function to type and value arguments.+--+-- NB: different from @evDFunApp@ defined in GHC, as this function returns+-- an @EvExpr@ rather than an @EvTerm@.+evDFunApp :: DFunId -> [Type] -> [EvExpr] -> EvExpr+evDFunApp df tys ets = Var df `mkTyApps` tys `mkApps` ets++-- | Apply a data constructor to type and value arguments.+--+-- NB: different from @evDataConApp@ defined in GHC, as this function returns+-- an @EvExpr@ rather than an @EvTerm@.+evDataConApp :: DataCon -> [Type] -> [EvExpr] -> EvExpr+evDataConApp dc tys ets = evDFunApp (dataConWrapId dc) tys ets++-- | Cast an evidence expression by a coercion.+--+-- NB: different from @evCast@ defined in GHC, as this function returns+-- an @EvExpr@ rather than an @EvTerm@.+evCast :: EvExpr -> Coercion -> EvExpr+evCast et co | isReflCo co = et+ | otherwise = Cast et co++--------------------------------------------------------------------------------++natKind, symbolKind, charKind :: Type+natKind =+#if MIN_VERSION_ghc(9,1,0)+ naturalTy+#else+ typeNatKind+#endif+symbolKind = typeSymbolKind+charKind = charTy++--------------------------------------------------------------------------------++-- | Is this a primitive (unboxed) equality type, i.e. one of:+--+-- - @~#@ (heterogeneous nominal unboxed equality),+-- - @~R#@ (heterogeneous representational unboxed equality).+--+-- NB: returns @False@ for **boxed** equalities such as @(~)@, @(~~)@ and @Coercible@.+-- If you want to detect those, use 'isEqClassPred'.+isEqPred :: PredType -> Bool+isEqPred pty+ | Just tc <- tyConAppTyCon_maybe pty+ = tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey+ | otherwise+ = False++-- | Is this a boxed equality type, i.e. one of:+--+-- - @(~)@ (homogeneous nominal boxed equality),+-- - @(~~)@ (heterogeneous nominal boxed equality),+-- - @Coercible@ (homogeneous boxed representational equality).+isEqClassPred :: PredType -> Bool+isEqClassPred pty+ | Just tc <- tyConAppTyCon_maybe pty+ , Just cls <- tyConClass_maybe tc+ = cls `hasKey` heqTyConKey+ || cls `hasKey` eqTyConKey+ || cls `hasKey` coercibleTyConKey+ | otherwise+ = False++--------------------------------------------------------------------------------++#if !MIN_VERSION_ghc(9,6,0)+thNameToGhcNameIO :: HscEnv -> TH.Name -> IO (Maybe Name)+thNameToGhcNameIO hscEnv th_name+ = do { names <- mapMaybeM do_lookup (thRdrNameGuesses th_name)+ ; return (listToMaybe names) }+ where+ do_lookup rdr_name+ | Just n <- isExact_maybe rdr_name+ = return $ if isExternalName n then Just n else Nothing+ | Just (rdr_mod, rdr_occ) <- isOrig_maybe rdr_name+#if MIN_VERSION_ghc(9,3,0)+ = Just <$> lookupNameCache (hsc_NC hscEnv) rdr_mod rdr_occ+#else+ = Just <$> lookupOrigIO hscEnv rdr_mod rdr_occ+#endif+ | otherwise+ = return Nothing+#endif++--------------------------------------------------------------------------------
src/GHC/TcPlugin/API/Internal.hs view
@@ -51,7 +51,6 @@ , TcPluginM(..) , TcPluginErrorMessage(..) , TcPluginRewriter- , MonadThings(..) , askRewriteEnv , askDeriveds , askEvBinds@@ -69,21 +68,12 @@ ( TypeError, ErrorMessage(..) ) -- transformers+import Control.Monad.IO.Class+ ( MonadIO ( liftIO ) ) 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 )@@ -95,17 +85,25 @@ ( PredType, Type(..), TyLit(..) ) import qualified GHC.Core.Type as GHC- ( mkTyConApp, tcTypeKind )+ ( mkTyConApp, typeKind ) import qualified GHC.Data.FastString as GHC ( fsLit ) import qualified GHC.Tc.Plugin as GHC ( tcLookupDataCon, tcLookupTyCon )+#if MIN_VERSION_ghc(10,1,0)+import qualified GHC.Tc.Utils.Env+ as GHC+ ( rnLookupKnownKeyName )+#endif import qualified GHC.Tc.Types as GHC ( TcM, TcPlugin(..), TcPluginM , TcPluginSolver+#if !MIN_VERSION_ghc(9,1,0)+ , TcPluginResult(..)+#endif #ifdef HAS_REWRITING , TcPluginRewriter #else@@ -129,20 +127,45 @@ 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(..) )+#if !MIN_VERSION_ghc(9,1,0)+import GHC.Tc.Types.Constraint+ ( ctEvidence, ctEvId, isDerived )+import GHC.Types.Var.Env+ ( lookupVarEnv, mkVarEnv )+import GHC.Utils.Outputable+import GHC.Tc.Plugin+ ( tcPluginTrace ) #endif -- ghc-tcplugin-api+import qualified GHC.Builtins+ as GHC+ ( constraintKind )+import qualified GHC.Builtins+ as GHC.TypeError+#if MIN_VERSION_ghc(10,1,0)+ ( errorMessageTypeErrorFamKey+ , typeErrorTextDataConKey+ , typeErrorAppendDataConKey+ , typeErrorVAppendDataConKey+ , typeErrorShowTypeDataConKey+ )+#else+ ( errorMessageTypeErrorFamName+ , typeErrorTextDataConName+ , typeErrorAppendDataConName+ , typeErrorVAppendDataConName+ , typeErrorShowTypeDataConName+ )+#endif #ifndef HAS_REWRITING import GHC.TcPlugin.API.Internal.Shim ( TcPluginSolveResult, TcPluginRewriteResult(..) , RewriteEnv , shimRewriter+#if !MIN_VERSION_ghc(9,1,0)+ , unflattenCts+#endif ) #endif @@ -151,10 +174,14 @@ -- | Stage of a type-checking plugin, used as a data kind. data TcPluginStage+ -- | Plugin initialisation = Init+ -- | Solve constraints | Solve+ -- | Rewrite type-families | Rewrite- | Stop+ -- | End of typechecking+ | PostTc -- | The @solve@ function of a type-checking plugin takes in Given and Wanted -- constraints, and should return a 'GHC.Tc.Types.TcPluginSolveResult'@@ -198,22 +225,22 @@ -- > myTcPlugin args = ... data TcPlugin = forall s. TcPlugin { tcPluginInit :: TcPluginM Init s- -- ^ Initialise plugin, when entering type-checker.+ -- ^ Initialize plugin (once per module), when starting the 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.+ -- process: once to simplify 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.+ -- and possibly emit additional constraints. These returned constraints+ -- must be Givens in the first case, and Wanteds in the second. --- -- Use @ \\ _ _ _ -> pure $ TcPluginOK [] [] @ if your plugin- -- does not provide this functionality.+ -- Use @ \\ _ _ _ _ -> pure $ TcPluginOk [] [] @ if your plugin , tcPluginRewrite :: s -> GHC.UniqFM@@ -232,8 +259,18 @@ -- -- 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.+ , tcPluginPostTc :: s -> TcPluginM PostTc ()+ -- ^ Action to run at the end of typechecking a module, e.g. to intercept+ -- the final 'TcGblEnv'/'TcLclEnv' at the end of typechecking, possibly+ -- modifying mutable fields.+ --+ -- Should not terminate the plugin, as the plugin may continue to be invoked+ -- when desugaring the module (as the pattern-match checker may invoke the+ -- constraint solver).++ , tcPluginShutdown :: s -> IO ()+ -- ^ Clean up after the plugin, when GHC is done processing the given+ -- module (e.g. after desugaring). } -- | The monad used for a type-checker plugin, parametrised by@@ -257,8 +294,8 @@ 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 }+newtype instance TcPluginM PostTc a =+ TcPluginPostTcM { tcPluginPostTcM :: GHC.TcPluginM a } deriving newtype ( Functor, Applicative, Monad ) -- | Ask for the evidence currently gathered by the type-checker.@@ -369,14 +406,14 @@ #endif . ( \ f -> f builtinDefs rewriteEnv ) . tcPluginRewriteM )-instance MonadTcPlugin ( TcPluginM Stop ) where- liftTcPluginM = TcPluginStopM+instance MonadTcPlugin ( TcPluginM PostTc ) where+ liftTcPluginM = TcPluginPostTcM unsafeWithRunInTcM runInTcM = unsafeLiftTcM $ runInTcM #ifdef HAS_REWRITING- ( GHC.runTcPluginM . tcPluginStopM )+ ( GHC.runTcPluginM . tcPluginPostTcM ) #else- ( ( `GHC.runTcPluginM` ( error "tcPluginStop: cannot access EvBindsVar" ) ) . tcPluginStopM )+ ( ( `GHC.runTcPluginM` ( error "tcPluginPostTc: cannot access EvBindsVar" ) ) . tcPluginPostTcM ) #endif -- | Take a function whose argument and result types are both within the 'GHC.Tc.TcM' monad,@@ -394,19 +431,26 @@ { tcPluginInit = tcPluginInit :: TcPluginM Init userDefs , tcPluginSolve , tcPluginRewrite- , tcPluginStop+ , tcPluginPostTc+ , tcPluginShutdown } ) = GHC.TcPlugin- { GHC.tcPluginInit = adaptUserInit tcPluginInit+ { GHC.tcPluginInit = adaptUserInit tcPluginInit #ifdef HAS_REWRITING- , GHC.tcPluginSolve = adaptUserSolve tcPluginSolve- , GHC.tcPluginRewrite = adaptUserRewrite tcPluginRewrite+ , GHC.tcPluginSolve = adaptUserSolve tcPluginSolve+ , GHC.tcPluginRewrite = adaptUserRewrite tcPluginRewrite #else- , GHC.tcPluginSolve = adaptUserSolveAndRewrite- tcPluginSolve tcPluginRewrite+ , GHC.tcPluginSolve = adaptUserSolveAndRewrite+ tcPluginSolve tcPluginRewrite #endif- , GHC.tcPluginStop = adaptUserStop tcPluginStop+#if MIN_VERSION_ghc(10,0,0)+ , GHC.tcPluginPostTc = adaptUserPostTc tcPluginPostTc+ , GHC.tcPluginShutdown = adaptUserShutdown tcPluginShutdown+#else+ , GHC.tcPluginStop = adaptUserStop+ tcPluginPostTc tcPluginShutdown+#endif } where adaptUserInit :: TcPluginM Init userDefs -> GHC.TcPluginM ( TcPluginDefs userDefs )@@ -444,33 +488,92 @@ -> TcPluginDefs userDefs -> GHC.TcPluginSolver adaptUserSolveAndRewrite userSolve userRewrite ( TcPluginDefs { tcPluginUserDefs, tcPluginBuiltinDefs } )- = \ givens deriveds wanteds -> do+ = \ givens0 deriveds0 wanteds0 -> do+#if MIN_VERSION_ghc(9,1,0)+ let givens = givens0+ deriveds = deriveds0+ wanteds = wanteds0+#else+ let ( givens, deriveds, wanteds ) = unflattenCts givens0 deriveds0 wanteds0+ tcPluginTrace "ghc-tcplugin-api: unflattening" $+ vcat [ text "givens:" <+> ppr givens0+ , text "deriveds:" <+> ppr deriveds0+ , text "wanteds:" <+> ppr wanteds0+ , text (replicate 80 '=')+ , text "givens:" <+> ppr givens+ , text "deriveds:" <+> ppr deriveds+ , text "wanteds:" <+> ppr wanteds+ ]+#endif 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- )+ res <-+ 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+ )+#if MIN_VERSION_ghc(9,1,0)+ return res+#else+ let origCts =+ mkVarEnv+ [ ( ctEvId ct, ct )+ | ct <- givens0 ++ wanteds0 ]+ case res of+ GHC.TcPluginOk solved new -> do+ -- If we are solving a constraint that has been flattened, make+ -- sure to solve the original constraint instead of the flattened+ -- constraint, otherwise GHC gets very confused.+ let+ lookupOrigCt ct+ | isDerived (ctEvidence ct)+ = ct+ | Just ct' <- lookupVarEnv origCts ( ctEvId ct )+ = ct'+ | otherwise+ = ct+ solved' = map ( \ ( ev, ct ) -> ( ev, lookupOrigCt ct ) ) solved+ return $ GHC.TcPluginOk solved' new+ GHC.TcPluginContradiction {} ->+ return res #endif+#endif - adaptUserStop :: ( userDefs -> TcPluginM Stop () ) -> TcPluginDefs userDefs -> GHC.TcPluginM ()- adaptUserStop userStop ( TcPluginDefs { tcPluginUserDefs } ) =- tcPluginStopM $ userStop tcPluginUserDefs+#if MIN_VERSION_ghc(10,0,0)+ adaptUserPostTc :: ( userDefs -> TcPluginM PostTc () ) -> TcPluginDefs userDefs -> GHC.TcPluginM ()+ adaptUserPostTc userPostTc ( TcPluginDefs { tcPluginUserDefs } ) =+ tcPluginPostTcM $ userPostTc tcPluginUserDefs+ adaptUserShutdown :: ( userDefs -> IO () ) -> TcPluginDefs userDefs -> IO ()+ adaptUserShutdown userShutdown ( TcPluginDefs { tcPluginUserDefs } ) =+ userShutdown tcPluginUserDefs+#else+ -- Prior to GHC 10.0, run the "post-tc" and "shutdown" actions in sequence,+ -- at the end of typechecking. Typechecker plugins do not persist to desugaring.+ adaptUserStop :: ( userDefs -> TcPluginM PostTc () ) -> ( userDefs -> IO () ) -> TcPluginDefs userDefs -> GHC.TcPluginM ()+ adaptUserStop userPostTc userShutdown ( TcPluginDefs { tcPluginUserDefs } ) = do+ tcPluginPostTcM $ userPostTc tcPluginUserDefs+ GHC.unsafeTcPluginTcM . liftIO $ userShutdown tcPluginUserDefs+#endif ++-- | @since 0.15.0.0+instance ( Monad ( TcPluginM s ), MonadTcPlugin ( TcPluginM s ) ) => MonadIO ( TcPluginM s ) where+ liftIO = unsafeLiftTcM . liftIO+ -- | 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'.+-- throw type errors in 'tcPluginInit' or 'tcPluginPostTc'. -- -- See 'mkTcPluginErrorTy' and 'GHC.TcPlugin.API.emitWork' for functions -- which require this typeclass.@@ -492,9 +595,9 @@ 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'."+instance TypeError ( 'Text "Cannot emit new work in 'tcPluginPostTc'." )+ => MonadTcPluginWork ( TcPluginM PostTc ) where+ askBuiltins = error "Cannot emit new work in 'tcPluginPostTc'." -- | 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,@@ -527,10 +630,6 @@ 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.@@ -552,11 +651,25 @@ 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+#if MIN_VERSION_ghc(10,1,0)+ let lookupBuiltin = GHC.unsafeTcPluginTcM . GHC.rnLookupKnownKeyName+ typeErrorName <- lookupBuiltin GHC.TypeError.errorMessageTypeErrorFamKey+ textName <- lookupBuiltin GHC.TypeError.typeErrorTextDataConKey+ showTypeName <- lookupBuiltin GHC.TypeError.typeErrorShowTypeDataConKey+ concatName <- lookupBuiltin GHC.TypeError.typeErrorAppendDataConKey+ vcatName <- lookupBuiltin GHC.TypeError.typeErrorVAppendDataConKey+#else+ let typeErrorName = GHC.TypeError.errorMessageTypeErrorFamName+ textName = GHC.TypeError.typeErrorTextDataConName+ showTypeName = GHC.TypeError.typeErrorShowTypeDataConName+ concatName = GHC.TypeError.typeErrorAppendDataConName+ vcatName = GHC.TypeError.typeErrorVAppendDataConName+#endif+ typeErrorTyCon <- GHC.tcLookupTyCon typeErrorName+ textTyCon <- GHC.promoteDataCon <$> GHC.tcLookupDataCon textName+ showTypeTyCon <- GHC.promoteDataCon <$> GHC.tcLookupDataCon showTypeName+ concatTyCon <- GHC.promoteDataCon <$> GHC.tcLookupDataCon concatName+ vcatTyCon <- GHC.promoteDataCon <$> GHC.tcLookupDataCon vcatName pure ( BuiltinDefs { .. } ) interpretErrorMessage :: BuiltinDefs -> TcPluginErrorMessage -> GHC.PredType@@ -566,7 +679,7 @@ go ( Txt str ) = GHC.mkTyConApp textTyCon [ GHC.LitTy . GHC.StrTyLit . GHC.fsLit $ str ] go ( PrintType ty ) =- GHC.mkTyConApp showTypeTyCon [ GHC.tcTypeKind ty, ty ]+ GHC.mkTyConApp showTypeTyCon [ GHC.typeKind 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 ) =
src/GHC/TcPlugin/API/Internal/Shim.hs view
@@ -21,6 +21,9 @@ , TcPluginSolveResult(TcPluginContradiction, TcPluginOk, ..), TcPluginRewriteResult(..) , RewriteEnv(..) , shimRewriter+#if !MIN_VERSION_ghc(9,1,0)+ , unflattenCts+#endif ) where @@ -31,11 +34,11 @@ ( forM, unless, when ) import Data.Foldable ( traverse_-#if !MIN_VERSION_ghc(9,2,0)+#if !MIN_VERSION_ghc(9,1,0) , foldlM #endif )-#if MIN_VERSION_ghc(9,2,0)+#if MIN_VERSION_ghc(9,1,0) import Data.List.NonEmpty ( NonEmpty((:|)) ) #endif@@ -55,6 +58,9 @@ , mkAppCos, mkNomReflCo, mkSubCo , mkTyConAppCo, tyConRolesX , tyConRolesRepresentational+#if !MIN_VERSION_ghc(9,1,0)+ , CoercionHole(..), setCoHoleCoVar, coHoleCoVar+#endif ) import GHC.Core.Predicate ( EqRel(..), eqRelRole )@@ -64,7 +70,7 @@ ) import GHC.Core.TyCon ( TyCon(..), TyConBinder, TyConBndrVis(..)-#if MIN_VERSION_ghc(9,2,0)+#if MIN_VERSION_ghc(9,1,0) , isForgetfulSynTyCon #endif , isFamFreeTyCon, isTypeSynonymTyCon@@ -80,7 +86,7 @@ #endif , coreView, tyVarKind )-#if MIN_VERSION_ghc(9,2,0)+#if MIN_VERSION_ghc(9,1,0) import GHC.Data.Maybe ( firstJustsM ) #endif@@ -96,7 +102,7 @@ , runTcPluginTcS, runTcSWithEvBinds , traceTcS , setWantedEvTerm-#if MIN_VERSION_ghc(9,2,0)+#if MIN_VERSION_ghc(9,1,0) , lookupFamAppCache, lookupFamAppInert, extendFamAppCache , pattern EqualCtList #else@@ -112,8 +118,10 @@ import GHC.Tc.Types.Constraint ( Ct(..), CtEvidence(..) , CtLoc, CtFlavour(..), CtFlavourRole, ShadowInfo(..)-#if MIN_VERSION_ghc(9,2,0)+#if MIN_VERSION_ghc(9,1,0) , CanEqLHS(..)+#else+ , QCInst(..), TcEvDest(..) #endif , ctLoc, ctFlavour, ctEvidence, ctEqRel, ctEvPred , ctEvExpr, ctEvCoercion, ctEvFlavour@@ -125,10 +133,14 @@ ) import GHC.Tc.Utils.TcType ( TcTyCoVarSet-#if MIN_VERSION_ghc(9,2,0)+#if MIN_VERSION_ghc(9,1,0) , tcSplitForAllTyVarBinders #else , tcSplitForAllVarBndrs++ -- Unflattening+ , TCvSubst(..), substTy, substTys, extendTvSubst+ , emptyTCvSubst, lookupTyVar #endif , tcSplitTyConApp_maybe , tcTypeKind@@ -138,8 +150,10 @@ ( UniqFM, lookupUFM, isNullUFM ) import GHC.Types.Var ( TcTyVar, VarBndr(..)-#if !MIN_VERSION_ghc(9,2,0)+#if !MIN_VERSION_ghc(9,1,0) , TyVarBinder+ , updateTyVarKind+ , setVarType #endif , updateTyVarKindM )@@ -152,7 +166,7 @@ import GHC.Utils.Monad ( zipWith3M ) import GHC.Utils.Outputable- ( Outputable(..), SDoc, empty )+ hiding ( (<>) ) -- ghc-tcplugin-api import GHC.TcPlugin.API.Internal.Shim.Reduction@@ -252,8 +266,8 @@ -- -- The plugin can also emit additional wanted constraints. | TcPluginRewriteTo- { tcPluginReduction :: !Reduction- , tcRewriterWanteds :: [Ct]+ { tcPluginReduction :: !Reduction+ , tcRewriterNewWanteds :: [Ct] } type Rewriter = RewriteEnv -> [Ct] -> [Type] -> TcPluginM TcPluginRewriteResult@@ -532,7 +546,7 @@ liftTcS $ extendFamAppCache tc tys ( mkSymCoOnGHC92 final_co, final_xi )-#if !MIN_VERSION_ghc(9,2,0)+#if !MIN_VERSION_ghc(9,1,0) flavour #endif return final_redn@@ -545,7 +559,7 @@ -- (Recall: this module is only used for GHC 9.2 and below.) mkSymCoOnGHC92 :: Coercion -> Coercion mkSymCoOnGHC92 co =-#if MIN_VERSION_ghc(9,2,0)+#if MIN_VERSION_ghc(9,1,0) mkSymCo co #else co@@ -591,8 +605,8 @@ pure ( res, s ) case rewriteResult of TcPluginRewriteTo- { tcPluginReduction = redn- , tcRewriterWanteds = wanteds+ { tcPluginReduction = redn+ , tcRewriterNewWanteds = wanteds } -> addRewriting ( Just redn ) wanteds TcPluginNoRewrite { } -> addRewriting Nothing []@@ -615,7 +629,7 @@ rewriterView :: Type -> Maybe Type rewriterView ty@(TyConApp tc _) | ( isTypeSynonymTyCon tc && not (isFamFreeTyCon tc) )-#if MIN_VERSION_ghc(9,2,0)+#if MIN_VERSION_ghc(9,1,0) || isForgetfulSynTyCon tc #endif = tcView ty@@ -651,7 +665,7 @@ rewrite_tyvar2 tv fr@(_, eq_rel) = do ieqs <- liftTcS $ getInertEqs case lookupDVarEnv ieqs tv of-#if MIN_VERSION_ghc(9,2,0)+#if MIN_VERSION_ghc(9,1,0) Just (EqualCtList (ct :| _)) | CEqCan { cc_ev = ctev, cc_lhs = TyVarLHS {} , cc_rhs = rhs_ty, cc_eq_rel = ct_eq_rel } <- ct@@ -668,7 +682,7 @@ (ReprEq, _rel) -> rewriting_co1 (NomEq, NomEq) -> rewriting_co1 (NomEq, ReprEq) -> mkSubCo rewriting_co1- return $ RTRFollowed $ mkReduction rewriting_co rhs_ty + return $ RTRFollowed $ mkReduction rewriting_co rhs_ty _other -> return RTRNotFollowed rewrite_vector :: Kind@@ -942,7 +956,7 @@ !env' = env { rewriteEnv = renv' } thing_inside env' s -#if !MIN_VERSION_ghc(9,2,0)+#if !MIN_VERSION_ghc(9,1,0) -------------------------------------------------------------------------------- -- GHC 9.0 compatibility. @@ -971,5 +985,114 @@ tcSplitForAllTyVarBinders :: Type -> ([TyVarBinder], Type) tcSplitForAllTyVarBinders = tcSplitForAllVarBndrs++#endif++--------------------------------------------------------------------------------+-- Unflattening constraints++#if !MIN_VERSION_ghc(9,1,0)+unflattenCts :: [ Ct ] -> [ Ct ] -> [ Ct ] -> ( [ Ct ], [ Ct ], [ Ct ] )+unflattenCts givens0 deriveds0 wanteds0 =+ -- NB: on all GHC versions we support (GHC >= 8.8),+ -- GHC passes zonked constraints to typechecker plugins.+ -- So there's no need for us to zonk anything.+ let ( subst, givens ) = add_fsks emptyTCvSubst [] givens0+ deriveds = substCts subst deriveds0+ wanteds = substCts subst wanteds0++ in+ ( givens, deriveds, wanteds )++-- Construct an unflattening substitution from Givens of the form+--+-- [G] fsk ~ rhs+--+-- and filter them out.+add_fsks :: TCvSubst -> [ Ct ] -> [ Ct ] -> ( TCvSubst, [ Ct ] )+add_fsks subst rev_acc [] = ( subst, substCts subst $ reverse rev_acc )+add_fsks subst rev_acc ( ct : cts ) =+ case ct of+ CFunEqCan { cc_fsk, cc_fun, cc_tyargs } ->+ let subst' = extendSubst subst cc_fsk $ mkTyConApp cc_fun cc_tyargs+ in add_fsks subst' rev_acc cts+ _ -> add_fsks subst ( ct : rev_acc ) cts++extendSubst :: TCvSubst -> TyVar -> Type -> TCvSubst+extendSubst subst@( TCvSubst in_scope tv_env cv_env ) tv ty =+ -- Keep the substitution idempotent+ let ty' = substTy subst ty+ tv_subst = extendTvSubst emptyTCvSubst tv ty'+ subst' = TCvSubst in_scope ( fmap ( substTy tv_subst ) tv_env ) cv_env+ in extendTvSubst subst' tv ty'++substCts :: TCvSubst -> [ Ct ] -> [ Ct ]+substCts subst = map $ substCt subst++substCt :: TCvSubst -> Ct -> Ct+substCt subst ct =+ case ct of+ CIrredCan { cc_ev } ->+ ct { cc_ev = substCtEv subst cc_ev }+ CNonCanonical { cc_ev } ->+ ct { cc_ev = substCtEv subst cc_ev }+ CDictCan { cc_ev, cc_tyargs } ->+ ct { cc_ev = substCtEv subst cc_ev+ , cc_tyargs = substTys subst cc_tyargs+ }+ CFunEqCan {} ->+ pprPanic "substCt: CFunEqCan" (ppr ct)+ CTyEqCan { cc_ev, cc_tyvar, cc_rhs } ->+ let ev' = substCtEv subst cc_ev+ rhs' = substTy subst cc_rhs+ in+ case lookupTyVar subst cc_tyvar of+ Nothing ->+ ct { cc_ev = ev'+ , cc_tyvar = updateTyVarKind ( substTy subst ) cc_tyvar+ , cc_rhs = rhs'+ }+ Just ty' ->+ case ty' of+ TyVarTy tv' ->+ ct { cc_ev = ev'+ , cc_tyvar = tv'+ , cc_rhs = rhs'+ }+ _ ->+ CNonCanonical { cc_ev = ev' }+ CQuantCan qci@( QCI { qci_ev, qci_tvs, qci_pred } ) ->+ CQuantCan $+ qci { qci_ev = substCtEv subst qci_ev+ , qci_tvs = map ( updateTyVarKind $ substTy subst ) qci_tvs+ , qci_pred = substTy subst qci_pred+ }+#if !MIN_VERSION_ghc(8,11,0)+ CHoleCan { cc_ev } ->+ let ev' = substCtEv subst cc_ev+ in ct { cc_ev = ev' }+#endif++substCtEv :: TCvSubst -> CtEvidence -> CtEvidence+substCtEv subst ctev =+ setCtEvPredType ctev ( substTy subst ( ctev_pred ctev ) )++setCtEvPredType :: CtEvidence -> Type -> CtEvidence+setCtEvPredType old_ev@(CtGiven { ctev_evar = ev }) new_pred+ = old_ev { ctev_pred = new_pred+ , ctev_evar = setVarType ev new_pred }++setCtEvPredType old_ev@(CtWanted { ctev_dest = dest }) new_pred+ = old_ev { ctev_pred = new_pred+ , ctev_dest = new_dest }+ where+ new_dest = case dest of+ EvVarDest ev -> EvVarDest (setVarType ev new_pred)+ HoleDest h -> HoleDest (setCoHoleType h new_pred)+setCtEvPredType old_ev@( CtDerived {} ) new_pred+ = old_ev { ctev_pred = new_pred }++setCoHoleType :: CoercionHole -> Type -> CoercionHole+setCoHoleType h t = setCoHoleCoVar h (setVarType (coHoleCoVar h) t) #endif
src/GHC/TcPlugin/API/Names.hs view
@@ -41,7 +41,9 @@ > > findMyModule :: MonadTcPlugin m => m Module > findMyModule = do-> findResult <- findImportedModule ( mkModuleName "MyModule" ) Nothing+> let modlName = mkModuleName "MyModule"+> pkgQual <- resolveImport modlName Nothing+> findResult <- findImportedModule modlName pkgQual > case findResult of > Found _ res -> pure res > _ -> error $ "MyPlugin: could not find any module named MyModule."@@ -116,13 +118,22 @@ import GHC.TypeLits ( TypeError, ErrorMessage(..) ) +-- containers+import Data.Map+ ( Map )+import qualified Data.Map as Map+ -- transformers import Control.Monad.Trans.State.Strict- ( StateT, evalStateT, get, put )+ ( StateT, evalStateT, get, modify ) import Control.Monad.Trans.Class ( MonadTrans(lift) ) -- ghc+#if MIN_VERSION_ghc(9,8,0)+import GHC.Iface.Errors.Ppr+ ( missingInterfaceErrorDiagnostic )+#endif #if MIN_VERSION_ghc(9,3,0) import GHC.Iface.Errors ( cannotFindModule )@@ -134,24 +145,17 @@ ( 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+import GHC.Unit.Module ( 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 )+#if MIN_VERSION_ghc(9,8,0)+import GHC.Types.Error+ ( HasDefaultDiagnosticOpts(defaultOpts) )+#endif -- ghc-tcplugin-api import GHC.TcPlugin.API@@ -367,47 +371,21 @@ -------------------------------------------------------------------------------- -- Caching of found modules. -data ImportedModules+newtype ImportedModules = ImportedModules- { home_modules :: UniqFM ModuleName Module- , this_pkg_modules :: UniqFM UnitId ( UniqFM ModuleName Module )- , other_pkg_modules :: UniqFM UnitId ( UniqFM ModuleName Module )+ { imported_modules :: Map (PkgQual, ModuleName) Module } emptyModules :: ImportedModules emptyModules =- ImportedModules- { home_modules = emptyUFM- , this_pkg_modules = emptyUFM- , other_pkg_modules = emptyUFM- }+ ImportedModules Map.empty 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+lookupCachedModule pkg modl = Map.lookup (pkg, modl) . imported_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) }+insertCachedModule pkg modl md = modify $ \mods ->+ mods{ imported_modules = Map.insert (pkg, modl) md (imported_modules mods) } lookupModule :: MonadTcPlugin m => PkgQual -> ModuleName -> StateT ImportedModules m Module lookupModule pkg mod_name = do@@ -425,23 +403,23 @@ hsc_env <- lift . liftTcPluginM $ getTopEnv let err_doc :: SDoc+ err_doc =+#if MIN_VERSION_ghc(9,8,0)+ missingInterfaceErrorDiagnostic defaultOpts $+#endif #if MIN_VERSION_ghc(9,2,0)- err_doc = cannotFindModule hsc_env mod_name other+ cannotFindModule hsc_env mod_name other #else- err_doc = cannotFindModule dflags mod_name other- dflags :: DynFlags- dflags = hsc_dflags hsc_env+ cannotFindModule (hsc_dflags hsc_env) mod_name other #endif pgmErrorDoc- ( "GHC.TcPlugin.API: could not find module " <> mod_str <> " in " <> pkg_name )+ ( "GHC.TcPlugin.API: could not find module "+ <> moduleNameString mod_name+ <> case pkgQualToPkgName pkg of+ Just p -> " in package " <> p+ Nothing -> mempty+ ) 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.
+ src/GHC/TcPlugin/API/TyConSubst.hs view
@@ -0,0 +1,537 @@+{-# LANGUAGE CPP #-}++{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiWayIf #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE ViewPatterns #-}++{-|+Module: GHC.TcPlugin.API.TyConSubst++This module provides functionality for recognising whether a type is a+'TyConApp' while taking into account Given nominal equalities.++In particular, this allows dealing with flattening variables on older GHC versions+(9.0 and below). For example, instead of @[W] m + n ~ n + m@, older GHCs might+produce @[G] u ~ m + n, [G] v ~ n + m, [W] u ~ v@. In this case, one needs to+use the Givens to recognise that @u ~ v@ can be solved using the laws of natural+number arithmetic.++Usage:++ - Use 'mkTyConSubst' to create a 'TyConSubst' from Givens.+ - Use 'splitTyConApp_upTo' to compute whether a type is a 'TyConApp', taking+ into account Given constraints (in the form of the 'TyConSubst').++Notes:++ - 'splitTyConApp_upTo' will also look through type synonyms,+ - 'splitTyConApp_upTo' only takes into account nominal equalities.+ Please open a ticket if you have a need for rewriting modulo representational+ equalities.++-}+module GHC.TcPlugin.API.TyConSubst (+ TyConSubst -- opaque+ , mkTyConSubst+ , splitTyConApp_upTo+ ) where++-- Word64Map is available:+--+-- - from 9.10.1 onwards+-- - in 9.8.4+-- - in 9.6.7+--+-- This is unusual: whether a module is exposed depends on the MINOR version+#define HAS_WORD64MAP \+ (MIN_VERSION_ghc(9,9,0) || \+ (MIN_VERSION_ghc(9,8,4) && !(MIN_VERSION_ghc(9,9,0))) || \+ (MIN_VERSION_ghc(9,6,7) && !(MIN_VERSION_ghc(9,7,0))))++-- base+import Data.Bifunctor+ ( Bifunctor(first, second) )+import Data.Either+ ( partitionEithers )+import Data.Foldable+ ( toList, asum )+import Data.List.NonEmpty+ ( NonEmpty(..) )+import Data.Maybe+ ( fromJust )+#if !MIN_VERSION_ghc(8,11,0)+import Unsafe.Coerce+ ( unsafeCoerce )+#endif++-- containers+import Data.Sequence+ ( Seq )+import qualified Data.Sequence as Seq++-- ghc+#if HAS_WORD64MAP+import qualified GHC.Data.Word64Map.Strict as Word64Map+#else+import qualified Data.IntMap.Strict as IntMap+#endif+import GHC.Types.Unique+ ( Uniquable, getUnique )+import qualified GHC.Types.Unique.FM as UFM+import GHC.Types.Unique.Set+ ( UniqSet )+import qualified GHC.Types.Unique.Set as UniqSet+import GHC.Utils.Outputable+ hiding ( (<>) )++-- ghc-tcplugin-api+import GHC.TcPlugin.API+import GHC.Tc.Types.Constraint++{-------------------------------------------------------------------------------+ The main type++ TODO: maybe this could be sped up with+ <https://hackage.haskell.org/package/union-find>?+-------------------------------------------------------------------------------}++-- | Substitution for recognizing 'TyCon' applications modulo nominal equalities.+data TyConSubst = TyConSubst {+ tyConSubstMap :: UniqFM TcTyVar (NonEmpty (TyCon, [Type], [Coercion]))+ , tyConSubstCanon :: UniqFM TcTyVar (TcTyVar, [Coercion])+ }+-- During constraint solving the set of Given constraints includes so-called+-- "canonical equalities": equalities of the form+--+-- > var ~ typ (CTyEqCan)+-- > var ~ TyCon arg1 .. argN (CFunEqCan, the TyCon will be a type family)+--+-- The problem we want to solve is recognizing if some type τ is of the form+--+-- > TyCon arg1 arg2 .. argN (0 <= N)+--+-- modulo those canonical equalities. We limit the scope of what we try to do:+--+-- o We are only interested in recognizing types of the form above+-- (as opposed to general parsing-modulo-equalities).+-- o We will only use the canonical equalities as-is: we will not attempt to+-- derive any additional equalities from them (i.e. if, say, we know that+-- @x ~ T1@ and @x ~ T2@, we will not attempt to use the fact that this means+-- that @T1 ~ T2@, nor any derived conclusions thereof). We /will/ however+-- try to apply the canonical equalities as often as is necessary (e.g.,+-- first applying @x ~ T y@, then applying @y ~ T2@).+--+-- We solve this problem by constructing a 'TyConSubst': a possibly+-- non-deterministic substitution mapping type variables to types of the form+-- above (that is, a type constructor applied to some arguments).+--+-- We detail the construction of this substitution below (see documentation of+-- 'Classified' and 'process'), but once we have this substitution, the+-- recognition problem becomes easy:+--+-- 1. Without loss of generality, let τ be of the form @t arg1 arg2 .. argN@+-- 2. If @t@ is a 'TyCon', we're done.+-- 3. Otherwise, if @t@ is a variable @x@, lookup @x@ in the substitution; if+-- there is one (or more) mappings for @x@, then we have successfully+-- recognized τ to be of the form above. There is no need to apply the+-- substitution repeatedly.+--+-- The substitution is non-deterministic because there might be multiple+-- matches. For example, if we have+--+-- > type family Foo where+-- > Foo = Int+--+-- then we might well have equalities @x ~ Int, x ~ Foo@ in scope, and so a type+-- @x@ would match two different 'TyCon's. What we do know, however, is that if+-- τ matches both @t arg1 .. argN@ and @t' arg1' .. argM'@ (possibly @N /= M@),+-- then+--+-- > t arg1 .. argN ~ t' arg1' .. argM'+--+-- If @t == t'@, we can conclude that the arguments are equal only if @t@ is+-- injective.++{-------------------------------------------------------------------------------+ Basic functionality for working with 'TyConSubst'+-------------------------------------------------------------------------------}++-- | Empty substitution+--+-- The canonical variables map is established once when the initial substitution+-- is generated and not updated thereafter.+tyConSubstEmpty :: UniqFM TcTyVar (TcTyVar, [Coercion]) -> TyConSubst+tyConSubstEmpty canon = TyConSubst {+ tyConSubstMap = UFM.emptyUFM+ , tyConSubstCanon = canon+ }++-- | Lookup a variable in the substitution+tyConSubstLookup :: TcTyVar -> TyConSubst -> Maybe (NonEmpty (TyCon, [Type], [Coercion]))+tyConSubstLookup var TyConSubst{..} =+ fmap ( \ (tc, tys, deps) -> (tc, tys, deps ++ deps')) <$> UFM.lookupUFM tyConSubstMap var'+ where+ var' :: TcTyVar+ deps' :: [Coercion]+ (var', deps') = canonicalize tyConSubstCanon var++-- | Extend substitution with new bindings+tyConSubstExtend ::+ [(TcTyVar, (TyCon, [Type]), [Coercion])]+ -> TyConSubst -> TyConSubst+tyConSubstExtend new subst@TyConSubst{..} = subst {+ tyConSubstMap = UFM.plusUFM_C (<>)+ (UFM.listToUFM $ map aux new)+ tyConSubstMap+ }+ where+ aux :: (TcTyVar, (TyCon, [Type]), [Coercion])+ -> (TcTyVar, NonEmpty (TyCon, [Type] , [Coercion]))+ aux (var, (tc, args), deps) =+ let (var', deps') = canonicalize tyConSubstCanon var+ in (var', (tc, args, deps ++ deps') :| [])++{-------------------------------------------------------------------------------+ Classification+-------------------------------------------------------------------------------}++-- | Classified canonical nominal equality constraints.+--+-- The first step in the construction of the 'TyConSubst' is to classify the+-- available canonical equalities as one of three categories, defined below.+data Classified = Classified {+ -- | " Obviously " productive mappings+ --+ -- An equality @var := TyCon args@ is productive, because as soon as we+ -- apply it, we are done: we have successfully recognized a type as being+ -- an application of a concrete type constructor (note that we only ever+ -- apply the substitution to the head @t@ of a type @t args@, never to the+ -- arguments).+ classifiedProductive :: [(TcTyVar, (TyCon, [Type]), [Coercion])]++ -- | Extend equivalence class of variables+ --+ -- An equality @var1 := var2@ we will regard as extending the equivalence+ -- classes of variables (see 'constructEquivClasses').+ , classifiedExtendEquivClass :: [(TcTyVar, TcTyVar, [Coercion])]++ -- | Substitutions we need to reconsider later+ --+ -- An equality @var1 := var2 args@ (with @args@ a non-empty list of+ -- arguments) is most problematic. Applying it /may/ allow us to make+ -- progress, but it may not (consider for example @var := var arg@). We+ -- will reconsider such equalities at the end (see 'process').+ , classifiedReconsider :: [(TcTyVar, (TcTyVar, NonEmpty Type), [Coercion])]+ }++instance Semigroup Classified where+ c1 <> c2 = Classified {+ classifiedProductive = combine classifiedProductive+ , classifiedExtendEquivClass = combine classifiedExtendEquivClass+ , classifiedReconsider = combine classifiedReconsider+ }+ where+ combine :: (Classified -> [a]) -> [a]+ combine f = f c1 ++ f c2++instance Monoid Classified where+ mempty = Classified [] [] []++productive :: TcTyVar -> (TyCon, [Type]) -> [Coercion] -> Classified+productive var app deps = mempty {+ classifiedProductive = [(var, app, deps)]+ }++extendEquivClass :: TcTyVar -> TcTyVar -> [Coercion] -> Classified+extendEquivClass var var' deps = mempty {+ classifiedExtendEquivClass = [(var, var', deps)]+ }++reconsider :: TcTyVar -> (TcTyVar, NonEmpty Type) -> [Coercion] -> Classified+reconsider var (var', args) deps = mempty {+ classifiedReconsider = [(var, (var', args), deps)]+ }++-- | Classify a set of Given constraints.+--+-- See 'Classified' for details.+classify :: [Ct] -> Classified+classify = go mempty+ where+ go :: Classified -> [Ct] -> Classified+ go acc [] = acc+ go acc (c:cs) =+ let deps = [ctEvCoercion (ctEvidence c)] in+ case isCanonicalVarEq c of+ Just (var, splitAppTys -> (fn, args), NomEq)+ | Just (tyCon, inner) <- splitTyConApp_maybe fn ->+ go (productive var (tyCon, inner ++ args) deps <> acc) cs+ | Just var' <- getTyVar_maybe fn, null args ->+ go (extendEquivClass var var' deps <> acc) cs+ | Just var' <- getTyVar_maybe fn, x:xs <- args ->+ go (reconsider var (var', x :| xs) deps <> acc) cs+ _otherwise ->+ go acc cs++{-------------------------------------------------------------------------------+ Processing+-------------------------------------------------------------------------------}++-- | Construct 'TyCon' substitution from classified nominal equality constraints.+--+-- The difficult part in constructing this substitution are the equalities of+-- the form @var1 ~ var2 args@, which we ear-marked as "to reconsider" during+-- classification.+--+-- We will do this iteratively:+--+-- o We first construct a set of variable equivalence classes based on+-- 'classifiedExtendEquivClass' (using 'constructEquivClasses'), and use that+-- along with the "obviously productive" equalities ('classifiedProductive')+-- as the initial value of the accumulator (a 'TyConSubst').+-- o We then repeatedly consider the remaining equalities. Whenever there is+-- a substitution available in the accumulator for @var2@ which turns it into+-- a type of the form @TyCon args'@, we add @var1 := TyCon args' args@ to the+-- accumulator.+-- o We keep doing this until we can make no more progress.+--+-- The functions for working with 'TyConSubst' take the variable equivalence+-- classes into account, so we do not need to do that here.+--+-- Two observations:+--+-- o This process must terminate: there are a finite number of constraints+-- to consider, and whenever we apply a substitution from the accumulator,+-- we get an "obviously productive" substitution: we do not create new work+-- in the loop.+-- o We may end up ignoring some substitutions: if there is a substitution+-- @var1 := var2 args@ and we don't have any (productive) substitutions for+-- @var2@, we will just ignore it.+--+-- A note on recursive bindings: a direct or indirect recursive binding+--+-- > x := x args1 x := y args1+-- > y := x args2+--+-- where @args1, args2@ are non-empty lists of arguments, /cannot/ be relevant:+-- if they were, that would imply that there is some type constructor (regular+-- datatype or type family) which can be applied to an arbitrary number of+-- arguments. Such datatypes or type families cannot be defined in Haskell.+-- We therefore take no special care in handling recursive bindings, other than+-- to note (as we did above) that the process must terminate.+process :: Classified -> TyConSubst+process Classified{..} =+ go initSubst classifiedReconsider+ where+ initSubst :: TyConSubst+ initSubst =+ tyConSubstExtend classifiedProductive+ $ tyConSubstEmpty (constructEquivClasses classifiedExtendEquivClass)++ go :: TyConSubst+ -> [(TcTyVar, (TcTyVar, NonEmpty Type), [Coercion])]+ -> TyConSubst+ go acc rs =+ let (prod, rest) = tryApply makeProductive rs in+ if null prod+ then acc -- No other equations can be made productive+ else go (tyConSubstExtend prod acc) rest+ where+ makeProductive ::+ (TcTyVar, (TcTyVar, NonEmpty Type), [Coercion])+ -> Maybe (NonEmpty (TcTyVar, (TyCon, [Type]), [Coercion]))+ makeProductive (var, (var', args), deps) = do+ tcApp <- tyConSubstLookup var' acc+ return $ fmap aux tcApp+ where+ aux :: (TyCon, [Type], [Coercion]) -> (TcTyVar, (TyCon, [Type]), [Coercion])+ aux (tyCon, args', deps') =+ (var, (tyCon, args' ++ toList args), deps ++ deps')++-- | Construct a 'TyConSubst' from a collection of Given constraints.+mkTyConSubst :: [Ct] -> TyConSubst+mkTyConSubst = process . classify++{-------------------------------------------------------------------------------+ Using+-------------------------------------------------------------------------------}++-- | Like 'splitTyConApp_maybe', but taking Given constraints into account.+--+-- Alongside the @TyCon@ and its arguments, also returns a list of coercions+-- that embody the Givens that we depended on.+--+-- Looks through type synonyms, just like 'splitTyConApp_maybe' does.+splitTyConApp_upTo :: TyConSubst -> Type -> Maybe (NonEmpty (TyCon, [Type], [Coercion]))+splitTyConApp_upTo subst typ = asum [+ -- Direct match+ do (tyCon, inner) <- splitTyConApp_maybe fn+ return ((tyCon, inner ++ args, []) :| [])++ -- Indirect match+ , do var <- getTyVar_maybe fn+ tcApps <- tyConSubstLookup var subst+ return $+ fmap (\ (tc, inner, deps) -> (tc, inner ++ args, deps)) tcApps+ ]+ where+ (fn, args) = splitAppTys typ++{-------------------------------------------------------------------------------+ Outputable+-------------------------------------------------------------------------------}++instance Outputable TyConSubst where+ ppr TyConSubst{..} = parens $+ text "TyConSubst"+ <+> ppr tyConSubstMap+ <+> ppr tyConSubstCanon++{-------------------------------------------------------------------------------+ Canonical equalities+-------------------------------------------------------------------------------}++isCanonicalVarEq :: Ct -> Maybe (TcTyVar, Type, EqRel)+isCanonicalVarEq = \case+#if __GLASGOW_HASKELL__ < 902+ CTyEqCan { cc_tyvar, cc_rhs, cc_eq_rel } ->+ Just (cc_tyvar, cc_rhs, cc_eq_rel)+ CFunEqCan { cc_fsk, cc_fun, cc_tyargs } ->+ Just (cc_fsk, mkTyConApp cc_fun cc_tyargs, NomEq)+#elif __GLASGOW_HASKELL__ < 907+ CEqCan { cc_lhs, cc_rhs, cc_eq_rel }+ | TyVarLHS var <- cc_lhs+ -> Just (var, cc_rhs, cc_eq_rel)+ | TyFamLHS tyCon args <- cc_lhs+ , Just var <- getTyVar_maybe cc_rhs+ -> Just (var, mkTyConApp tyCon args, NomEq)+#else+ CEqCan eqCt+ | TyVarLHS var <- lhs+ -> Just (var, rhs, rel)+ | TyFamLHS tyCon args <- lhs+ , Just var <- getTyVar_maybe rhs+ -> Just (var, mkTyConApp tyCon args, rel)+ where+ lhs = eq_lhs eqCt+ rhs = eq_rhs eqCt+ rel = eq_eq_rel eqCt+#endif+ -- Deal with CNonCanonical, which are produced by ghc-tcplugin-api+ -- in GHC 9.0 and below due to 'unflattenCts'.+ ct@(CNonCanonical {})+ | EqPred rel lhs rhs <- classifyPredType (ctPred ct)+ -> if | Just tv <- getTyVar_maybe lhs+ -> Just (tv, rhs, rel)+ | Just tv <- getTyVar_maybe rhs+ -> Just (tv, lhs, rel)+ | otherwise+ -> Nothing+ _ -> Nothing++{-------------------------------------------------------------------------------+ Internal auxiliary+-------------------------------------------------------------------------------}++-- | Attempt to apply a non-deterministic function to a list of values+--+-- Returns the successful results as well as the inputs on which the function+-- failed.+tryApply :: forall a b. (a -> Maybe (NonEmpty b)) -> [a] -> ([b], [a])+tryApply f = first (concat . map toList) . partitionEithers . map f'+ where+ f' :: a -> Either (NonEmpty b) a+ f' a = maybe (Right a) Left $ f a++{-------------------------------------------------------------------------------+ Equivalence classes+-------------------------------------------------------------------------------}++-- | Given a set of labelled equivalent pairs, map every value to a canonical+-- value in the same equivalence class, with the shortest path (as a list of+-- labels) connecting the value to the canonical value.+--+-- Example with two equivalence classes:+--+-- >>> constructEquivClasses [(1, 2, ["12"]), (4, 5, ["45"]), (2, 3, ["23"])]+-- fromList [(1,(1,[])),(2,(1,["12"])),(3,(1,["23","12"])),(4,(4,[])),(5,(4,["45"]))]+--+-- Adding one element that connects both equivalence classes:+--+-- >>> constructEquivClasses [(1, 2, ["12"]), (4, 5, ["45"]), (2, 3, ["23"]), (3, 4, ["34"])]+-- fromList [(1,(1,[])),(2,(1,["12"])),(3,(1,["23","12"])),(4,(1,["34","23","12"])),(5,(1,["45","34","23","12"]))]+constructEquivClasses :: forall a l. (Uniquable a, Monoid l) => [(a, a, l)] -> UniqFM a (a, l)+constructEquivClasses equivs = canonicals+ where+ neighbours :: UniqFM a (UniqFM a l)+ neighbours = neighboursMap equivs++ allValues :: UniqSet a+ allValues = UniqSet.mkUniqSet $ concat [ [x,y] | (x,y,_) <- equivs ]++ canonicals :: UniqFM a (a, l)+ canonicals = go UFM.emptyUFM allValues+ where+ go :: UniqFM a (a, l) -> UniqSet a -> UniqFM a (a, l)+ go acc vs =+ case minViewUniqSet vs of+ Nothing -> acc+ Just (v, vs') ->+ let+ !comp = doComp+ ( UFM.unitUFM v mempty )+ ( Seq.singleton $ getUnique v )+ in+ go+ ( UFM.plusUFM acc ( ( v , ) <$> comp ) )+ ( vs' `UniqSet.uniqSetMinusUFM` comp )++ doComp :: UniqFM a l -> Seq Unique -> UniqFM a l+ doComp !ds Seq.Empty = ds+ doComp ds (v Seq.:<| vs) =+ let+ -- unvisited neighbours+ !us = ( fromJust $ UFM.lookupUFM_Directly neighbours v ) `UFM.minusUFM` ds+ !d = fromJust $ UFM.lookupUFM_Directly ds v++ !ds' = UFM.plusUFM ds ( UFM.mapUFM (<> d) us )+ !vs' = vs Seq.>< Seq.fromList ( UFM.nonDetKeysUFM us )+ in+ doComp ds' vs'++minViewUniqSet :: forall a. UniqSet a -> Maybe (a, UniqSet a)+minViewUniqSet s =+ let m = UFM.ufmToIntMap $ UniqSet.getUniqSet s+ in second+ ( UniqSet.unsafeUFMToUniqSet+ .+#if MIN_VERSION_ghc(8,11,0)+ UFM.unsafeIntMapToUFM+#else+ ( unsafeCoerce :: IntMap.IntMap a -> UniqFM a a )+#endif+ ) <$>+#if HAS_WORD64MAP+ Word64Map.minView+#else+ IntMap.minView+#endif+ m++neighboursMap :: forall a l. Uniquable a => [(a, a, l)] -> UniqFM a (UniqFM a l)+neighboursMap edges = foldr addEdge UFM.emptyUFM edges+ where+ addEdge :: (a, a, l) -> UniqFM a (UniqFM a l) -> UniqFM a (UniqFM a l)+ addEdge (u, v, l) m+ = UFM.addToUFM_C UFM.plusUFM+ (UFM.addToUFM_C UFM.plusUFM m v (UFM.unitUFM u l))+ u (UFM.unitUFM v l)++canonicalize :: (Uniquable a, Monoid l) => UniqFM a (a, l) -> a -> (a, l)+canonicalize canon x = UFM.lookupWithDefaultUFM canon (x, mempty) x