diff --git a/changelog.md b/changelog.md --- a/changelog.md +++ b/changelog.md @@ -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: diff --git a/ghc-tcplugin-api.cabal b/ghc-tcplugin-api.cabal --- a/ghc-tcplugin-api.cabal +++ b/ghc-tcplugin-api.cabal @@ -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 ) diff --git a/src/GHC/Builtins.hs b/src/GHC/Builtins.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Builtins.hs @@ -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 diff --git a/src/GHC/TcPlugin/API.hs b/src/GHC/TcPlugin/API.hs --- a/src/GHC/TcPlugin/API.hs +++ b/src/GHC/TcPlugin/API.hs @@ -1,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 + +-------------------------------------------------------------------------------- diff --git a/src/GHC/TcPlugin/API/Internal.hs b/src/GHC/TcPlugin/API/Internal.hs --- a/src/GHC/TcPlugin/API/Internal.hs +++ b/src/GHC/TcPlugin/API/Internal.hs @@ -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 ) = diff --git a/src/GHC/TcPlugin/API/Internal/Shim.hs b/src/GHC/TcPlugin/API/Internal/Shim.hs --- a/src/GHC/TcPlugin/API/Internal/Shim.hs +++ b/src/GHC/TcPlugin/API/Internal/Shim.hs @@ -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 diff --git a/src/GHC/TcPlugin/API/Names.hs b/src/GHC/TcPlugin/API/Names.hs --- a/src/GHC/TcPlugin/API/Names.hs +++ b/src/GHC/TcPlugin/API/Names.hs @@ -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. diff --git a/src/GHC/TcPlugin/API/TyConSubst.hs b/src/GHC/TcPlugin/API/TyConSubst.hs new file mode 100644 --- /dev/null +++ b/src/GHC/TcPlugin/API/TyConSubst.hs @@ -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 + ? +-------------------------------------------------------------------------------} + +-- | 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