ghc-tcplugin-api 0.8.0.0 → 0.8.1.0

raw patch · 7 files changed

+3904/−3900 lines, 7 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• changelog.md +106/−102
• ghc-tcplugin-api.cabal +158/−158
• src/GHC/TcPlugin/API.hs +1005/−1005
• src/GHC/TcPlugin/API/Internal.hs +575/−575
• src/GHC/TcPlugin/API/Internal/Shim.hs +962/−962
• src/GHC/TcPlugin/API/Internal/Shim/Reduction.hs +604/−604
• src/GHC/TcPlugin/API/Names.hs +494/−494

@@ -1,102 +1,106 @@-
-# Version 0.8.0.0 (2022-07-07)
-
-- Compatibility for GHC 9.4.
-
-- Change API for `lookupImportedModule` to use `PkgQual` and `UnitId`
-  instead of `Maybe FastString`, with back-compatibility function `pkgQual_pkg`
-  for use with older module lookup functions.
-
-- Re-export `splitAppTys` and `unpackFS`.
-
-# Version 0.7.1.0 (2022-01-04)
-
-- `newWanted` now always uses the `CtLoc` information that it is provided with,
-  as opposed to obtaining some information from the monadic environment.
-  This means you no longer need to wrap calls to `newWanted` in `setCtLocM`
-  to ensure that GHC reports the correct source span when reporting unsolved
-  Wanteds in error messages.
-
-- Remove the `newDerived` function, as Derived constraints are going to be
-  removed from GHC.
-
-# Version 0.7.0.0 (2021-12-31)
-
-- Re-export functions for dealing with type-level literals,
-  such as `mkNumLitTy` and `isStrLitTy`.
-
-- Re-export functions for splitting apart type applications, such as
-  `splitAppTy_maybe` and `tyConAppTyCon_maybe`.
-
-- Redefine and re-export `mkUncheckedIntExpr` for GHC versions prior to 9.0.
-
-- Re-export some basic types from `GHC.Types.Basic` such as `Arity`,
-  `PromotionFlag` and `Boxity`.
-
-- Re-export `GHC.Builtin.Names` and `GHC.Builin.Types.Prim`.
-
-- Provide `MonadThings` instances for `TcPluginM` monads.
-
-# Version 0.6.1.0 (2021-12-13)
-
-- Re-export various useful types and functions to deal with type and coercion variables.
-
-- Re-export a few types and functions to deal with source locations.
-
-- Remove some re-exports for constructing function types, as not all functions make sense
-  across all GHC versions supported by the library.
-
-- Re-export `panic` and `pprPanic`.
-
-# Version 0.6.0.0 (2021-12-13)
-
-- Add support for GHC 8.8.
-
-- Re-export `evDataConApp`, which is useful for constructing typeclass dictionaries.
-
-# Version 0.5.1.0 (2021-08-31)
-
-- Fix a bug in the type-family rewriting compatibility layer (GHC 8.10, 9.0, 9.2)
-  by correctly downgrading the coercion used to cast the evidence, when necessary.
-
-# Version 0.5.0.0 (2021-08-30)
-
-- Re-export some additional types and functions that are useful for inspecting
-  and constructing evidence terms, such as `mkTyVar`, `newName`, `mkLocalId`, `lookupEvBind`...
-
-# Version 0.4.1.0 (2021-08-24)
-
-- Re-export a few GHC modules, such as GHC.Core.Make and GHC.Plugins.
-  These re-exports might be changed to be more selective in the future
-  to aid cross-version compatibility.
-
-# Version 0.4.0.0 (2021-08-24)
-
-- Adapt to GHC 9.4 changes in the `TcPluginSolveResult` datatype:
-  are now able to solve and emit constraints even when reporting
-  a contradiction. This can help with error messages.
-  Unfortunately these extra constraints will be dropped in versions
-  of GHC prior to 9.4.
-
-- Add a utility module for name resolution using constrained traversals.
-
-- Add compatibility for GHC 8.10.
-
-# Version 0.3.1.0 (2021-08-09)
-
-Ensure that the coercions stored in `Reduction`s are always
-oriented left-to-right, by making the internal rewriting compatibility layer
-also use left-to-right coercions.
-
-# Version 0.3.0.0 (2021-08-04)
-
-Account for changes in rewriting in GHC 9.4:
-
-  - rewriter plugins can no longer emit new Wanted constraints
-    if they don't rewrite the type family application;
-  - coercions in the rewriter are now oriented left-to-right,
-    requiring `mkTyFamAppReduction` to be adapted.
-
-# Version 0.2.0.0 (2021-07-22)
-
-Initial release on Hackage.
+# Version 0.8.1.0 (2022-10-05)++- Bugfix for the GHC 9.2 (and below) rewriter plugin compatibility shim:+  fix coercion orientations.++# Version 0.8.0.0 (2022-07-07)++- Compatibility for GHC 9.4.++- Change API for `lookupImportedModule` to use `PkgQual` and `UnitId`+  instead of `Maybe FastString`, with back-compatibility function `pkgQual_pkg`+  for use with older module lookup functions.++- Re-export `splitAppTys` and `unpackFS`.++# Version 0.7.1.0 (2022-01-04)++- `newWanted` now always uses the `CtLoc` information that it is provided with,+  as opposed to obtaining some information from the monadic environment.+  This means you no longer need to wrap calls to `newWanted` in `setCtLocM`+  to ensure that GHC reports the correct source span when reporting unsolved+  Wanteds in error messages.++- Remove the `newDerived` function, as Derived constraints are going to be+  removed from GHC.++# Version 0.7.0.0 (2021-12-31)++- Re-export functions for dealing with type-level literals,+  such as `mkNumLitTy` and `isStrLitTy`.++- Re-export functions for splitting apart type applications, such as+  `splitAppTy_maybe` and `tyConAppTyCon_maybe`.++- Redefine and re-export `mkUncheckedIntExpr` for GHC versions prior to 9.0.++- Re-export some basic types from `GHC.Types.Basic` such as `Arity`,+  `PromotionFlag` and `Boxity`.++- Re-export `GHC.Builtin.Names` and `GHC.Builin.Types.Prim`.++- Provide `MonadThings` instances for `TcPluginM` monads.++# Version 0.6.1.0 (2021-12-13)++- Re-export various useful types and functions to deal with type and coercion variables.++- Re-export a few types and functions to deal with source locations.++- Remove some re-exports for constructing function types, as not all functions make sense+  across all GHC versions supported by the library.++- Re-export `panic` and `pprPanic`.++# Version 0.6.0.0 (2021-12-13)++- Add support for GHC 8.8.++- Re-export `evDataConApp`, which is useful for constructing typeclass dictionaries.++# Version 0.5.1.0 (2021-08-31)++- Fix a bug in the type-family rewriting compatibility layer (GHC 8.10, 9.0, 9.2)+  by correctly downgrading the coercion used to cast the evidence, when necessary.++# Version 0.5.0.0 (2021-08-30)++- Re-export some additional types and functions that are useful for inspecting+  and constructing evidence terms, such as `mkTyVar`, `newName`, `mkLocalId`, `lookupEvBind`...++# Version 0.4.1.0 (2021-08-24)++- Re-export a few GHC modules, such as GHC.Core.Make and GHC.Plugins.+  These re-exports might be changed to be more selective in the future+  to aid cross-version compatibility.++# Version 0.4.0.0 (2021-08-24)++- Adapt to GHC 9.4 changes in the `TcPluginSolveResult` datatype:+  are now able to solve and emit constraints even when reporting+  a contradiction. This can help with error messages.+  Unfortunately these extra constraints will be dropped in versions+  of GHC prior to 9.4.++- Add a utility module for name resolution using constrained traversals.++- Add compatibility for GHC 8.10.++# Version 0.3.1.0 (2021-08-09)++Ensure that the coercions stored in `Reduction`s are always+oriented left-to-right, by making the internal rewriting compatibility layer+also use left-to-right coercions.++# Version 0.3.0.0 (2021-08-04)++Account for changes in rewriting in GHC 9.4:++  - rewriter plugins can no longer emit new Wanted constraints+    if they don't rewrite the type family application;+  - coercions in the rewriter are now oriented left-to-right,+    requiring `mkTyFamAppReduction` to be adapted.++# Version 0.2.0.0 (2021-07-22)++Initial release on Hackage.

@@ -1,158 +1,158 @@-cabal-version:  3.0
-name:           ghc-tcplugin-api
-version:        0.8.0.0
-synopsis:       An API for type-checker plugins.
-license:        BSD-3-Clause
-build-type:     Simple
-author:         Sam Derbyshire
-maintainer:     Sam Derbyshire
-copyright:      2021 Sam Derbyshire
-homepage:       https://github.com/sheaf/ghc-tcplugin-api
-category:       Type System, GHC, Plugin
-description:
-
-  This library provides a streamlined monadic interface
-  for writing GHC type-checking plugins.
-
-  Each stage in a type-checking plugin (initialisation, solving, rewriting,
-  shutdown) has a corresponding monad, preventing operations that are only
-  allowed in some stages to be used in the other stages.
-  Operations that work across multiple stages are overloaded across monads
-  using MTL-like typeclasses.
-
-  Some operations, like creating evidence for constraints or creating
-  custom type error messages, are also simplified.
-
-  Please refer to the <https://github.com/sheaf/ghc-tcplugin-api associated GitHub repository>
-  for example usage.
-
-extra-source-files:
-  changelog.md
-
-library
-
-  build-depends:
-    base
-      >= 4.13.0 && < 4.19,
-    ghc
-      >= 8.8    && < 9.7,
-    transformers
-      >= 0.5    && < 0.6,
-
-  default-language:
-    Haskell2010
-
-  ghc-options:
-    -Wall
-    -Wcompat
-    -fwarn-missing-local-signatures
-    -fwarn-incomplete-uni-patterns
-    -fwarn-missing-deriving-strategies
-    -fno-warn-unticked-promoted-constructors
-
-  hs-source-dirs:
-    src
-
-  exposed-modules:
-    GHC.TcPlugin.API,
-    GHC.TcPlugin.API.Names,
-    GHC.TcPlugin.API.Internal
-
-  reexported-modules:
-      GHC.Builtin.Names
-    , GHC.Builtin.Types
-    , GHC.Builtin.Types.Prim
-    , GHC.Core.Make
-    , GHC.Plugins
-    , GHC.Types.Unique.DFM
-    , GHC.Types.Unique.FM
-    , GHC.Utils.Outputable
-
-  if impl(ghc >= 9.3.0)
-    cpp-options: -DHAS_REWRITING
-  else
-    cpp-options: -DHAS_DERIVEDS
-    other-modules:
-      GHC.TcPlugin.API.Internal.Shim
-      GHC.TcPlugin.API.Internal.Shim.Reduction
-
-  -- Compatibility for versions of GHC prior to 9.0.
-  if impl(ghc < 9.0)
-
-    mixins:
-      ghc
-        ( GHC        as GHC
-
-        , PrelNames  as GHC.Builtin.Names
-        , TysWiredIn as GHC.Builtin.Types
-        , TysPrim    as GHC.Builtin.Types.Prim
-
-        , CoreSyn    as GHC.Core
-        , CoAxiom    as GHC.Core.Coercion.Axiom
-        , Coercion   as GHC.Core.Coercion
-        , Class      as GHC.Core.Class
-        , DataCon    as GHC.Core.DataCon
-        , FamInstEnv as GHC.Core.FamInstEnv
-        , InstEnv    as GHC.Core.InstEnv
-        , MkCore     as GHC.Core.Make
-        , TyCoRep    as GHC.Core.TyCo.Rep
-        , TyCon      as GHC.Core.TyCon
-        , Type       as GHC.Core.Type
-
-        , FastString as GHC.Data.FastString
-        , Pair       as GHC.Data.Pair
-
-        , Finder     as GHC.Driver.Finder
-        , DynFlags   as GHC.Driver.Session
-        , HscTypes   as GHC.Driver.Types
-
-        , GhcPlugins as GHC.Plugins
-
-        , TcPluginM  as GHC.Tc.Plugin
-        , TcSMonad   as GHC.Tc.Solver.Monad
-        , TcRnTypes  as GHC.Tc.Types
-        , TcEvidence as GHC.Tc.Types.Evidence
-        , TcRnMonad  as GHC.Tc.Utils.Monad
-        , TcType     as GHC.Tc.Utils.TcType
-        , TcMType    as GHC.Tc.Utils.TcMType
-
-        , BasicTypes as GHC.Types.Basic
-        , Id         as GHC.Types.Id
-        , Literal    as GHC.Types.Literal
-        , Name       as GHC.Types.Name
-        , OccName    as GHC.Types.Name.Occurrence
-        , SrcLoc     as GHC.Types.SrcLoc
-        , Unique     as GHC.Types.Unique
-        , UniqDFM    as GHC.Types.Unique.DFM
-        , UniqFM     as GHC.Types.Unique.FM
-        , Var        as GHC.Types.Var
-        , VarEnv     as GHC.Types.Var.Env
-        , VarSet     as GHC.Types.Var.Set
-
-        , Module     as GHC.Unit.Module
-        , Module     as GHC.Unit.Module.Name
-        , Module     as GHC.Unit.Types
-
-        , Util       as GHC.Utils.Misc
-        , TcRnMonad  as GHC.Utils.Monad
-        , Outputable as GHC.Utils.Outputable
-        , Panic      as GHC.Utils.Panic
-        )
-
-    if impl(ghc > 8.10)
-
-      mixins:
-        ghc
-          ( Predicate  as GHC.Core.Predicate
-          , Constraint as GHC.Tc.Types.Constraint
-          , TcOrigin   as GHC.Tc.Types.Origin
-          )
-
-    else
-
-      mixins:
-        ghc
-          ( Type      as GHC.Core.Predicate
-          , TcRnTypes as GHC.Tc.Types.Constraint
-          , TcRnTypes as GHC.Tc.Types.Origin
-          )
+cabal-version:  3.0+name:           ghc-tcplugin-api+version:        0.8.1.0+synopsis:       An API for type-checker plugins.+license:        BSD-3-Clause+build-type:     Simple+author:         Sam Derbyshire+maintainer:     Sam Derbyshire+copyright:      2021 Sam Derbyshire+homepage:       https://github.com/sheaf/ghc-tcplugin-api+category:       Type System, GHC, Plugin+description:++  This library provides a streamlined monadic interface+  for writing GHC type-checking plugins.++  Each stage in a type-checking plugin (initialisation, solving, rewriting,+  shutdown) has a corresponding monad, preventing operations that are only+  allowed in some stages to be used in the other stages.+  Operations that work across multiple stages are overloaded across monads+  using MTL-like typeclasses.++  Some operations, like creating evidence for constraints or creating+  custom type error messages, are also simplified.++  Please refer to the <https://github.com/sheaf/ghc-tcplugin-api associated GitHub repository>+  for example usage.++extra-source-files:+  changelog.md++library++  build-depends:+    base+      >= 4.13.0 && < 4.19,+    ghc+      >= 8.8    && < 9.7,+    transformers+      >= 0.5    && < 0.6,++  default-language:+    Haskell2010++  ghc-options:+    -Wall+    -Wcompat+    -fwarn-missing-local-signatures+    -fwarn-incomplete-uni-patterns+    -fwarn-missing-deriving-strategies+    -fno-warn-unticked-promoted-constructors++  hs-source-dirs:+    src++  exposed-modules:+    GHC.TcPlugin.API,+    GHC.TcPlugin.API.Names,+    GHC.TcPlugin.API.Internal++  reexported-modules:+      GHC.Builtin.Names+    , GHC.Builtin.Types+    , GHC.Builtin.Types.Prim+    , GHC.Core.Make+    , GHC.Plugins+    , GHC.Types.Unique.DFM+    , GHC.Types.Unique.FM+    , GHC.Utils.Outputable++  if impl(ghc >= 9.3.0)+    cpp-options: -DHAS_REWRITING+  else+    cpp-options: -DHAS_DERIVEDS+    other-modules:+      GHC.TcPlugin.API.Internal.Shim+      GHC.TcPlugin.API.Internal.Shim.Reduction++  -- Compatibility for versions of GHC prior to 9.0.+  if impl(ghc < 9.0)++    mixins:+      ghc+        ( GHC        as GHC++        , PrelNames  as GHC.Builtin.Names+        , TysWiredIn as GHC.Builtin.Types+        , TysPrim    as GHC.Builtin.Types.Prim++        , CoreSyn    as GHC.Core+        , CoAxiom    as GHC.Core.Coercion.Axiom+        , Coercion   as GHC.Core.Coercion+        , Class      as GHC.Core.Class+        , DataCon    as GHC.Core.DataCon+        , FamInstEnv as GHC.Core.FamInstEnv+        , InstEnv    as GHC.Core.InstEnv+        , MkCore     as GHC.Core.Make+        , TyCoRep    as GHC.Core.TyCo.Rep+        , TyCon      as GHC.Core.TyCon+        , Type       as GHC.Core.Type++        , FastString as GHC.Data.FastString+        , Pair       as GHC.Data.Pair++        , Finder     as GHC.Driver.Finder+        , DynFlags   as GHC.Driver.Session+        , HscTypes   as GHC.Driver.Types++        , GhcPlugins as GHC.Plugins++        , TcPluginM  as GHC.Tc.Plugin+        , TcSMonad   as GHC.Tc.Solver.Monad+        , TcRnTypes  as GHC.Tc.Types+        , TcEvidence as GHC.Tc.Types.Evidence+        , TcRnMonad  as GHC.Tc.Utils.Monad+        , TcType     as GHC.Tc.Utils.TcType+        , TcMType    as GHC.Tc.Utils.TcMType++        , BasicTypes as GHC.Types.Basic+        , Id         as GHC.Types.Id+        , Literal    as GHC.Types.Literal+        , Name       as GHC.Types.Name+        , OccName    as GHC.Types.Name.Occurrence+        , SrcLoc     as GHC.Types.SrcLoc+        , Unique     as GHC.Types.Unique+        , UniqDFM    as GHC.Types.Unique.DFM+        , UniqFM     as GHC.Types.Unique.FM+        , Var        as GHC.Types.Var+        , VarEnv     as GHC.Types.Var.Env+        , VarSet     as GHC.Types.Var.Set++        , Module     as GHC.Unit.Module+        , Module     as GHC.Unit.Module.Name+        , Module     as GHC.Unit.Types++        , Util       as GHC.Utils.Misc+        , TcRnMonad  as GHC.Utils.Monad+        , Outputable as GHC.Utils.Outputable+        , Panic      as GHC.Utils.Panic+        )++    if impl(ghc > 8.10)++      mixins:+        ghc+          ( Predicate  as GHC.Core.Predicate+          , Constraint as GHC.Tc.Types.Constraint+          , TcOrigin   as GHC.Tc.Types.Origin+          )++    else++      mixins:+        ghc+          ( Type      as GHC.Core.Predicate+          , TcRnTypes as GHC.Tc.Types.Constraint+          , TcRnTypes as GHC.Tc.Types.Origin+          )

@@ -1,1005 +1,1005 @@-{-# LANGUAGE CPP #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE DerivingStrategies #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE PatternSynonyms #-}
-{-# LANGUAGE UndecidableInstances #-}
-
-{-|
-Module: GHC.TcPlugin.API
-
-This module provides a unified interface for writing type-checking plugins for GHC.
-
-It attempts to re-export all the functionality from GHC that is relevant to plugin authors,
-as well as providing utility functions to streamline certain common operations such as
-creating evidence (to solve constraints), rewriting type family applications, throwing custom type errors.
-
-Consider making use of the table of contents to help navigate this documentation;
-don't hesitate to jump between sections to get an overview of the relevant aspects.
-
-For an illustration of the functionality, check the examples in the associated
-<https://github.com/sheaf/ghc-tcplugin-api GitHub repository>.
-
-The internal module "GHC.TcPlugin.API.Internal" can be used to directly
-lift and unlift computations in GHC's 'GHC.Tc.Types.TcM' monad, but it is hoped that
-the interface provided in this module is sufficient.
-
--}
-
-module GHC.TcPlugin.API
-  ( -- * Basic TcPlugin functionality
-
-    -- ** The 'TcPlugin' type
-    TcPlugin(..)
-  , mkTcPlugin
-
-    -- ** Plugin state
-    -- | A type-checker plugin can define its own state, corresponding to the existential parameter @s@
-    -- in the definition of 'TcPlugin'.
-    -- This allows a plugin to look up information a single time
-    -- on initialisation, and pass it on for access in all further invocations of the plugin.
-    --
-    -- For example:
-    --
-    -- > data MyDefinitions { myTyFam :: !TyCon, myClass :: !Class }
-    --
-    -- Usually, the 'tcPluginInit' part of the plugin looks up all this information and returns it:
-    --
-    -- > myTcPluginInit :: TcPluginM Init MyDefinitions
-    --
-    -- This step should also be used to initialise any external tools,
-    -- such as an external SMT solver.
-    --
-    -- This information will then be passed to other stages of the plugin:
-    --
-    -- > myTcPluginSolve :: MyDefinitions -> TcPluginSolver
-
-    -- ** The type-checking plugin monads
-
-    -- | Different stages of type-checking plugins have access to different information.
-    -- For a unified interface, an MTL-style approach is used, with the 'MonadTcPlugin'
-    -- typeclass providing overloading (for operations that work in all stages).
-  , TcPluginStage(..), MonadTcPlugin
-  , TcPluginM
-  , tcPluginIO
-
-    -- *** Emitting new work, and throwing type-errors
-
-    -- | Some operations only make sense in the two main phases, solving and rewriting.
-    -- This is captured by the 'MonadTcPluginWork' typeclass, which allows emitting
-    -- new work, including throwing type errors.
-  , MonadTcPluginWork
-  , TcPluginErrorMessage(..)
-  , mkTcPluginErrorTy
-
-    -- * Name resolution
-
-    -- | Name resolution is usually the first step in writing a type-checking plugin:
-    -- plugins need to look up the names of the objects they want to manipulate.
-    --
-    -- For instance, to lookup the type family @MyFam@ in module @MyModule@ in package @my-pkg@:
-    --
-    -- > lookupMyModule :: MonadTcPlugin m => m Module
-    -- > lookupMyModule = do
-    -- >    findResult <- findImportedModule ( mkModuleName "MyModule" ) ( Just $ fsLit "my-pkg" )
-    -- >    case findResult of
-    -- >      Found _ myModule -> pure myModule
-    -- >      _ -> error "MyPlugin couldn't find MyModule in my-pkg"
-    -- >
-    -- > lookupMyFam :: MonadTcPlugin m => Module -> m TyCon
-    -- > lookupMyFam myModule = tcLookupTyCon =<< lookupOrig myModule ( mkTcOcc "MyFam" )
-    --
-    -- Most of these operations should be performed in 'tcPluginInit', and passed on
-    -- to the other stages: the plugin initialisation is called only once in each module
-    -- that the plugin is used, whereas the solver and rewriter are usually called repeatedly.
-
-    -- ** Packages and modules
-
-    -- | Use these functions to lookup a module,
-    -- from the current package or imported packages.
-  , findImportedModule, fsLit, unpackFS, mkModuleName
-  , unitIdFS, stringToUnitId, pkgQual_pkg
-  , Module, ModuleName, FindResult(..), UnitId, PkgQual(..)
-
-    -- ** Names
-
-    -- *** Occurence names
-
-    -- | The most basic type of name is the 'OccName', which is a
-    -- simple textual name within a namespace (e.g. the class namespace),
-    -- without any disambiguation (no module qualifier, etc).
-  , mkVarOcc, mkDataOcc, mkTyVarOcc, mkTcOcc, mkClsOcc
-
-    -- *** Names
-
-    -- | After having looked up the 'Module', we can obtain the full 'Name'
-    -- referred to by an 'OccName'. This is fully unambiguous, as it
-    -- contains a 'Unique' identifier for the name.
-  , lookupOrig
-
-    -- *** 'TyCon', 'Class', 'DataCon', etc
-
-    -- | Finally, we can obtain the actual objects we're interested in handling,
-    -- such as classes, type families, data constructors... by looking them up
-    -- using their 'Name'.
-  , tcLookupTyCon
-  , tcLookupDataCon
-  , tcLookupClass
-  , tcLookupGlobal
-  , tcLookup
-  , tcLookupId
-  , promoteDataCon
-
-    -- * Constraint solving
-
-    -- | Type-checking plugins will often want to manipulate constraints,
-    -- e.g. solve constraints that GHC can't solve on its own, or emit
-    -- their own constraints.
-    --
-    -- There are two different constraint flavours:
-    --
-    --   - Given constraints, which are already known and
-    --     have evidence associated to them,
-    --   - Wanted constraints, for which evidence has not yet been found.
-    --
-    -- When GHC can't solve a Wanted constraint, it will get reported to the
-    -- user as a type error.
-
-  , TcPluginSolver
-#if HAS_REWRITING
-  , TcPluginSolveResult(..)
-#else
-  , TcPluginSolveResult
-  , pattern TcPluginContradiction, pattern TcPluginOk
-#endif
-
-    -- | The 'tcPluginSolve' method of a typechecker plugin will be invoked
-    -- in two different ways:
-    --
-    -- 1. to simplify Given constraints. In this case, the 'tcPluginSolve' function
-    --    will not be passed any Wanted constraints, and
-    -- 2. to solve Wanted constraints.
-    --
-    -- The plugin can then respond in one of two ways:
-    --
-    --   - with @TcPluginOk solved new@, where @solved@ is a list of solved constraints
-    --     and @new@ is a list of new constraints for GHC to process;
-    --   - with @TcPluginContradiction contras@, where @contras@ is a list of impossible
-    --     constraints, so that they can be turned into errors.
-    --
-    -- In both cases, the plugin must respond with constraints of the same flavour,
-    -- i.e. in (1) it should return only Givens, and for (2) it should return only
-    -- Wanteds; all other constraints will be ignored.
-
-    -- ** Getting started with constraint solving
-
-    -- | To get started, it can be helpful to immediately print out all the constraints
-    -- that the plugin is given, using 'tcPluginTrace':
-    --
-    -- > solver _ givens wanteds = do
-    -- >   tcPluginTrace "---Plugin start---" (ppr givens $$ ppr wanteds)
-    -- >   pure $ TcPluginOk [] []
-    --
-    -- This creates a plugin that prints outs the constraints it is passed,
-    -- without doing anything with them.
-    --
-    -- To see this output, you will need to pass the flags @-ddump-tc-trace@
-    -- and @-ddump-to-file@ to GHC. This will output the trace as a log file,
-    -- and you can search for @"---Plugin start---"@ to find the plugin inputs.
-    --
-    -- Note that pretty-printing in GHC is done using the 'Outputable' type class.
-    -- We use its 'ppr' method to turn things into pretty-printable documents,
-    -- and '($$)' to combine documents vertically.
-    -- If you need more capabilities for pretty-printing documents,
-    -- import GHC's "GHC.Utils.Outputable" module.
-  , tcPluginTrace
-
-    -- ** Inspecting constraints & predicates
-
-    -- *** Canonical and non-canonical constraints
-
-    -- | A constraint in GHC starts out as "non-canonical", which means that
-    -- GHC doesn't know what type of constraint it is.
-    -- GHC will inspect the constraint to turn it into a canonical form
-    -- (class constraint, equality constraint, etc.) which satisfies certain
-    -- invariants used during constraint solving.
-    --
-    -- Thus, whenever emitting new constraints, it is usually best to emit a
-    -- non-canonical constraint, letting GHC canonicalise it.
-  , mkNonCanonical
-
-    -- *** Predicates
-
-    -- | A type-checking plugin will usually need to inspect constraints,
-    -- so that it can pick out the constraints it is going to interact with.
-    --
-    -- In general, type-checking plugins can encounter all sorts of constraints,
-    -- whether in canonical form or not.
-    -- In order to handle these constraints in a uniform manner, it is usually
-    -- preferable to inspect each constraint's predicate, which can be obtained
-    -- by using 'classifyPredType' and 'ctPred'.
-    --
-    -- This allows the plugin to determine what kind of constraints it is dealing with:
-    --
-    --   - an equality constraint? at 'Nominal' or 'Representational' role?
-    --   - a type-class constraint? for which class?
-    --   - an irreducible constraint, e.g. something of the form @c a@?
-    --   - a quantified constraint?
-  , Pred
-  , pattern ClassPred, pattern EqPred, pattern IrredPred, pattern ForAllPred
-  , classifyPredType, ctPred
-
-    -- | == Handling type variables
-  , TyVar, CoVar
-  , MetaDetails, MetaInfo
-  , isSkolemTyVar
-  , isMetaTyVar, isFilledMetaTyVar_maybe
-  , writeMetaTyVar
-
-    -- | == Some further functions for inspecting constraints
-  , eqType
-  , ctLoc, ctEvidence, ctFlavour, ctEqRel, ctOrigin
-
-    -- ** Constraint evidence
-
-    -- *** Coercions
-
-    -- | 'GHC.Core.TyCo.Rep.Coercion's are the evidence for type equalities.
-    -- As such, when proving an equality, a type-checker plugin needs
-    -- to construct the associated coercions.
-  , mkPluginUnivCo
-  , newCoercionHole
-  , mkReflCo, mkSymCo, mkTransCo, mkUnivCo
-  , mkCoercionTy, isCoercionTy, isCoercionTy_maybe
-
-    -- *** Evidence terms
-
-    -- | Typeclass constraints have a different notion of evidence: evidence terms.
-    --
-    -- A plugin that wants to solve a class constraint will need to provide
-    -- an evidence term. Such evidence can be created from scratch, or it can be obtained
-    -- by combining evidence that is already available.
-
-  , mkPluginUnivEvTerm
-  , evDataConApp
-  , newEvVar, setEvBind
-  , evCoercion, evCast
-  , ctEvExpr
-  , askEvBinds, lookupEvBind, eb_lhs, eb_rhs
-  , newName, mkLocalId, mkTyVar
-  , ctev_pred, ctev_evar, ctev_loc, ctev_dest
-
-    -- *** Class dictionaries
-
-    -- | To create evidence terms for class constraints, type-checking plugins
-    -- need to be able to construct the appropriate dictionaries containing
-    -- the values for the class methods.
-    --
-    -- The class dictionary constructor can be obtained using 'classDataCon'.
-    -- Functions from "GHC.Core.Make", which is re-exported by this library,
-    -- will be useful for constructing the necessary terms
-    --
-    -- For instance, we can apply the class data constructor using 'mkCoreConApps'.
-    -- Remember that the type-level arguments (the typeclass variables) come first,
-    -- before the actual evidence term (the class dictionary expression).
-
-  , classDataCon
-#if !MIN_VERSION_ghc(9,0,0)
-  , mkUncheckedIntExpr
-#endif
-
-    -- | ==== Class instances
-
-    -- | In some cases, a type-checking plugin might need to access the
-    -- class instances that are currently in scope, e.g. to obtain certain
-    -- evidence terms.
-  , getInstEnvs
-
-    -- ** Emitting new constraints
-
-  , newWanted, newGiven
-
-    -- | The following functions allow plugins to create constraints
-    -- for typeclasses and type equalities.
-  , mkClassPred, mkPrimEqPredRole
-
-    -- | === Deriveds
-
-    -- | Derived constraints are like Wanted constraints, except that they
-    -- don't require evidence in order to be solved, and won't be seen
-    -- in error messages if they go unsolved.
-    --
-    -- Solver plugins usually ignore this type of constraint entirely.
-    -- They occur mostly when dealing with functional dependencies and type-family
-    -- injectivity annotations.
-    --
-    -- GHC 9.4 removes this flavour of constraints entirely, subsuming their uses into
-    -- Wanted constraints.
-  , askDeriveds
-
-    -- ** Location information and 'CtLoc's
-
-    -- | When creating new constraints, one still needs a mechanism allowing GHC
-    -- to report a certain source location associated to them when throwing an error,
-    -- as well as other information the type-checker was aware of at that point
-    -- (e.g. available instances, given constraints, etc).
-    --
-    -- This is the purpose of 'CtLoc'.
-  , setCtLocM
-  , setCtLocRewriteM
-
-    -- | 'bumpCtLocDepth' adds one to the "depth" of the constraint.
-    -- Can help avoid loops, by triggering a "maximum depth exceeded" error.
-  , bumpCtLocDepth
-
-    -- * Rewriting type-family applications
-
-  , TcPluginRewriter, TcPluginRewriteResult(..)
-
-    -- ** Querying for type family reductions
-
-  , matchFam
-  , getFamInstEnvs
-  , FamInstEnv
-
-    -- ** Specifying type family reductions
-
-    -- | A plugin that wants to rewrite a type family application must provide two
-    -- pieces of information:
-    --
-    --   - the type that the type family application reduces to,
-    --   - evidence for this reduction, i.e. a 'GHC.Core.TyCo.Rep.Coercion' proving the equality.
-    --
-    -- In the rewriting stage, type-checking plugins have access to the rewriter
-    -- environment 'RewriteEnv', which has information about the location of the
-    -- type family application, the local type-checking environment, among other things.
-    --
-    -- Note that a plugin should provide a 'UniqFM' from 'TyCon' to rewriting functions,
-    -- which specifies a rewriting function for each type family.
-    -- Use 'emptyUFM' or 'listToUFM' to construct this map,
-    -- or import the GHC module "GHC.Types.Unique.FM" for a more complete API.
-  , askRewriteEnv, rewriteEnvCtLoc, RewriteEnv
-  , mkTyFamAppReduction, Reduction(..)
-
-    -- * Handling Haskell types
-
-    -- ** Type variables
-  , newUnique
-  , newFlexiTyVar
-  , isTouchableTcPluginM
-  , mkTyVarTy, mkTyVarTys
-  , isTyVarTy, getTyVar_maybe
-  , TcType, TcTyVar, Unique, Kind
-
-    -- ** Type literals (natural numbers, type-level strings)
-  , mkNumLitTy, isNumLitTy
-  , mkStrLitTy, isStrLitTy
-
-    -- ** Creating and decomposing applications
-  , mkTyConTy, mkTyConApp, mkAppTy, mkAppTys
-  , splitTyConApp_maybe
-  , tyConAppTyConPicky_maybe, tyConAppTyCon_maybe
-  , splitAppTy_maybe, splitAppTys
-
-    -- ** Function types
-  , mkVisFunTyMany, mkVisFunTysMany
-  , mkInvisFunTyMany, mkInvisFunTysMany
-  , mkForAllTy, mkForAllTys
-  , mkPiTy, mkPiTys
-
-#if MIN_VERSION_ghc(9,0,0)
-  , Mult, pattern One, pattern Many
-#endif
-
-    -- ** Zonking
-
-    -- | Zonking is the operation in which GHC actually switches out mutable unification variables
-    -- for their actual filled in type.
-    --
-    -- See the Note [What is zonking?] in GHC's source code for more information.
-  , zonkTcType
-  , zonkCt
-
-    -- ** Panicking
-
-    -- | It is often better for type-checking plugins to panic when encountering a problem,
-    -- as opposed to silently doing something wrong. Use 'pprPanic' to throw an informative
-    -- error message, so that users of your plugin can report an issue if a problem occurs.
-  , panic, pprPanic
-
-    -- ** Map-like data structures based on 'Unique's
-
-    -- | Import "GHC.Types.Unique.FM" or "GHC.Types.Unique.DFM" for
-    -- a more complete interface to maps whose keys are 'Unique's.
-
-  , UniqDFM
-  , lookupUDFM, lookupUDFM_Directly, elemUDFM
-  , UniqFM
-  , emptyUFM, listToUFM
-
-    -- * The type-checking environment
-  , getEnvs
-
-    -- * Built-in types
-
-    -- | This module also re-exports the built-in types that GHC already knows about.
-    --
-    -- This allows plugins to directly refer to e.g. the promoted data constructor
-    -- 'True' without having to look up its name.
-    --
-    -- Refer to "GHC.Builtin.Names", "GHC.Builtin.Types" and "GHC.Builtin.Types.Prim".
-
-    -- * GHC types
-
-    -- | These are the types that the plugin will inspect and manipulate.
-
-    -- | = END OF API DOCUMENTATION, RE-EXPORTS FOLLOW
-
-    -- | == Some basic types
-
-  , module GHC.Types.Basic
-
-    -- | == Names
-  , Name, OccName, TyThing, TcTyThing
-  , MonadThings(..)
-  , Class(classTyCon), DataCon, TyCon, Id
-  , FastString
-
-    -- | == Constraints
-  , EqRel(..), FunDep, CtFlavour
-  , Ct, CtLoc, CtEvidence, CtOrigin
-  , QCInst
-  , Type, PredType
-  , InstEnvs, TcLevel
-
-    -- | === Coercions and evidence
-  , Coercion, Role(..), UnivCoProvenance
-  , CoercionHole(..)
-  , EvBind, EvTerm(EvExpr), EvVar, EvExpr, EvBindsVar
-  , Expr(Var, Type, Coercion), CoreBndr, CoreExpr
-  , TcEvDest(..)
-
-    -- | == The type-checking environment
-  , TcGblEnv, TcLclEnv
-
-    -- | == Source locations
-  , GenLocated(..), Located, RealLocated
-  , unLoc, getLoc
-
-    -- | == Pretty-printing
-  , SDoc, Outputable(..)
-
-  )
-  where
-
--- ghc
-import GHC
-  ( TyThing(..) )
-#if !MIN_VERSION_ghc(9,0,0)
-import GHC.Builtin.Types
-  ( intDataCon )
-import GHC.Builtin.Types.Prim
-  ( intPrimTy )
-#endif
-import GHC.Core
-  ( CoreBndr, CoreExpr, Expr(..) )
-import GHC.Core.Class
-  ( Class(..), FunDep )
-import GHC.Core.Coercion
-  ( mkReflCo, mkSymCo, mkTransCo
-  , mkUnivCo
-#if MIN_VERSION_ghc(8,10,0)
-  , mkPrimEqPredRole
-#endif
-  )
-import GHC.Core.Coercion.Axiom
-  ( Role(..) )
-import GHC.Core.DataCon
-  ( DataCon
-  , classDataCon, promoteDataCon
-  )
-import GHC.Core.FamInstEnv
-  ( FamInstEnv )
-import GHC.Core.InstEnv
-  ( InstEnvs(..) )
-#if !MIN_VERSION_ghc(9,0,0)
-import GHC.Core.Make
-  ( mkCoreConApps )
-#endif
-import GHC.Core.Predicate
-  ( EqRel(..)
-#if MIN_VERSION_ghc(8,10,0)
-  , Pred(..)
-#else
-  , PredTree(..), TyCoBinder
-  , mkPrimEqPred, mkReprPrimEqPred
-#endif
-  , classifyPredType, mkClassPred
-  )
-#if HAS_REWRITING
-import GHC.Core.Reduction
-  ( Reduction(..) )
-#endif
-import GHC.Core.TyCon
-  ( TyCon(..) )
-import GHC.Core.TyCo.Rep
-  ( Type, PredType, Kind
-  , Coercion(..), CoercionHole(..)
-  , UnivCoProvenance(..)
-#if MIN_VERSION_ghc(9,0,0)
-  , Mult
-  , mkVisFunTyMany, mkVisFunTysMany
-  , mkInvisFunTyMany, mkInvisFunTysMany
-#elif MIN_VERSION_ghc(8,10,0)
-  , mkVisFunTy, mkVisFunTys
-  , mkInvisFunTy, mkInvisFunTys
-#else
-  , mkFunTy, mkFunTys
-#endif
-#if MIN_VERSION_ghc(8,10,0)
-  , mkPiTy
-#endif
-  , mkPiTys
-  , mkTyVarTy, mkTyVarTys
-  , mkForAllTy, mkForAllTys
-  )
-import GHC.Core.Type
-  ( eqType, mkTyConTy, mkTyConApp, splitTyConApp_maybe
-  , splitAppTy_maybe, splitAppTys
-  , tyConAppTyConPicky_maybe, tyConAppTyCon_maybe
-  , mkAppTy, mkAppTys, isTyVarTy, getTyVar_maybe
-  , mkCoercionTy, isCoercionTy, isCoercionTy_maybe
-  , mkNumLitTy, isNumLitTy, mkStrLitTy, isStrLitTy
-#if MIN_VERSION_ghc(9,0,0)
-  , pattern One, pattern Many
-#endif
-  )
-import GHC.Data.FastString
-  ( FastString, fsLit, unpackFS )
-import qualified GHC.Tc.Plugin
-  as GHC
-import GHC.Tc.Types
-  ( TcTyThing(..), TcGblEnv(..), TcLclEnv(..)
-#if HAS_REWRITING
-  , TcPluginSolveResult(..), TcPluginRewriteResult(..)
-  , RewriteEnv(..)
-#endif
-  )
-import GHC.Tc.Types.Constraint
-  ( Ct(..), CtLoc(..), CtEvidence(..), CtFlavour(..)
-  , QCInst(..), TcEvDest(..)
-  , ctPred, ctLoc, ctEvidence, ctEvExpr
-  , ctFlavour, ctEqRel, ctOrigin
-  , bumpCtLocDepth
-  , mkNonCanonical
-  )
-import GHC.Tc.Types.Evidence
-  ( EvBind(..), EvTerm(..), EvExpr, EvBindsVar(..)
-  , evCoercion, evCast, lookupEvBind, evDataConApp
-  )
-import GHC.Tc.Types.Origin
-  ( CtOrigin(..) )
-import GHC.Tc.Utils.Monad
-  ( newName )
-import qualified GHC.Tc.Utils.Monad
-  as GHC
-    ( traceTc, setCtLocM )
-import GHC.Tc.Utils.TcType
-  ( TcType, TcLevel, MetaDetails, MetaInfo
-  , isSkolemTyVar, isMetaTyVar
-  )
-import GHC.Tc.Utils.TcMType
-  ( isFilledMetaTyVar_maybe, writeMetaTyVar )
-import GHC.Types.Basic
-  ( Arity, PromotionFlag(..), isPromoted
-  , Boxity(..), TupleSort(..)
-  )
-import GHC.Types.Id
-  ( Id, mkLocalId )
-#if !MIN_VERSION_ghc(9,0,0)
-import GHC.Types.Literal
-  ( Literal(..), LitNumType(..) )
-#endif
-import GHC.Types.Name
-  ( Name )
-import GHC.Types.Name.Occurrence
-  ( OccName(..)
-  , mkVarOcc, mkDataOcc, mkTyVarOcc, mkTcOcc, mkClsOcc
-  )
-#if MIN_VERSION_ghc(9,3,0)
-import GHC.Types.PkgQual
-  ( PkgQual(..) )
-#endif
-import GHC.Types.SrcLoc
-  ( GenLocated(..), Located, RealLocated
-  , unLoc, getLoc
-  )
-import GHC.Types.Unique
-  ( Unique )
-#if MIN_VERSION_ghc(9,0,0)
-import GHC.Types.Unique.FM as UniqFM
-  ( UniqFM, emptyUFM, listToUFM )
-#else
-import qualified GHC.Types.Unique.FM as GHC
-  ( UniqFM )
-import GHC.Types.Unique.FM as UniqFM
-  ( emptyUFM, listToUFM )
-#endif
-import GHC.Types.Unique.DFM
-  ( UniqDFM, lookupUDFM, lookupUDFM_Directly, elemUDFM )
-import GHC.Types.Var
-  ( TyVar, CoVar, TcTyVar, EvVar
-  , mkTyVar
-  )
-import GHC.Utils.Outputable
-  ( Outputable(..), SDoc
-#if !MIN_VERSION_ghc(9,2,0)
-  , panic, pprPanic
-#endif
-#if !MIN_VERSION_ghc(9,3,0)
-  , (<+>), doubleQuotes, empty, text
-#endif
-  )
-#if MIN_VERSION_ghc(9,2,0)
-import GHC.Utils.Panic
-  ( panic, pprPanic )
-#endif
-#if MIN_VERSION_ghc(9,2,0)
-import GHC.Unit.Finder
-  ( FindResult(..) )
-#else
-import GHC.Driver.Finder
-  ( FindResult(..) )
-#endif
-import GHC.Unit.Module
-  ( UnitId, unitIdFS, stringToUnitId, mkModuleName )
-#if MIN_VERSION_ghc(9,5,0)
-import Language.Haskell.Syntax.Module.Name
-  ( ModuleName )
-#else
-import GHC.Unit.Module.Name
-  ( ModuleName )
-#endif
-import GHC.Unit.Types
-  ( Module )
-
--- transformers
-import Control.Monad.IO.Class
-  ( MonadIO ( liftIO ) )
-
--- ghc-tcplugin-api
-import GHC.TcPlugin.API.Internal
-#ifndef HAS_REWRITING
-import GHC.TcPlugin.API.Internal.Shim
-#endif
-
---------------------------------------------------------------------------------
-
--- | Run an 'IO' computation within the plugin.
-tcPluginIO :: MonadTcPlugin m => IO a -> m a
-tcPluginIO = unsafeLiftTcM . liftIO
-
--- | Output some debugging information within the plugin.
-tcPluginTrace :: MonadTcPlugin m
-              => String -- ^ Text at the top of the debug message.
-              -> SDoc   -- ^ Formatted document to print (use the 'ppr' pretty-printing function to obtain an 'SDoc' from any 'Outputable')
-              -> m ()
-tcPluginTrace a b = unsafeLiftTcM $ GHC.traceTc a b
-
---------------------------------------------------------------------------------
-
-#if !MIN_VERSION_ghc(9,3,0)
--- | Package-qualifier after renaming
-data PkgQual
-  = NoPkgQual       -- ^ No package qualifier
-  | ThisPkg  UnitId -- ^ Import from home-unit
-  | OtherPkg UnitId -- ^ Import from another unit
-  deriving stock ( Ord, Eq )
-
-instance Outputable PkgQual where
-  ppr = \case
-    NoPkgQual  -> empty
-    ThisPkg  u -> doubleQuotes (ppr u)
-    OtherPkg u -> doubleQuotes (ppr u)
-#endif
-
--- | Compatibility function to convert a 'PkgQual' to @Maybe FastString@
--- on older versions of GHC (9.2 and below).
---
--- On newer GHCs, this is the identity function.
-pkgQual_pkg :: PkgQual
-#if MIN_VERSION_ghc(9,3,0)
-            -> PkgQual
-#else
-            -> Maybe FastString
-#endif
-pkgQual_pkg pkg =
-#if MIN_VERSION_ghc(9,3,0)
-  pkg
-#else
-  case pkg of
-    NoPkgQual        -> Nothing
-    ThisPkg  this    ->
-      let fs = unitIdFS this
-      in if fs == fsLit "this"
-      then Just fs
-      else pprPanic "pkgQual_pkg: \'ThisPkg\' package name should be \"this\"" (text "pkg:" <+> ppr pkg)
-    OtherPkg unit_id -> Just $ unitIdFS unit_id
-#endif
-
--- | Lookup a Haskell module from the given package.
-findImportedModule :: MonadTcPlugin m
-                   => ModuleName -- ^ Module name, e.g. @"Data.List"@.
-                   -> PkgQual -- ^ Package name, e.g. @Just "base"@.
-                              -- Use @Nothing@ for the current home package
-                   -> m FindResult
-findImportedModule mod_name pkg
-  = liftTcPluginM
-  $ GHC.findImportedModule mod_name (pkgQual_pkg pkg)
-
--- | Obtain the full internal 'Name' (with its unique identifier, etc) from its 'OccName'.
---
--- Example usage:
---
--- > lookupOrig preludeModule ( mkTcOcc "Bool" )
---
--- This will obtain the 'Name' associated with the type 'Bool'.
---
--- You can then call 'tcLookupTyCon' to obtain the associated 'TyCon'.
-lookupOrig :: MonadTcPlugin m => Module -> OccName -> m Name
-lookupOrig md = liftTcPluginM . GHC.lookupOrig md
-
--- | Lookup a type constructor from its name (datatype, type synonym or type family).
-tcLookupTyCon :: MonadTcPlugin m => Name -> m TyCon
-tcLookupTyCon = liftTcPluginM . GHC.tcLookupTyCon
-
--- | Lookup a data constructor (such as 'True', 'Just', ...) from its name.
-tcLookupDataCon :: MonadTcPlugin m => Name -> m DataCon
-tcLookupDataCon = liftTcPluginM . GHC.tcLookupDataCon
-
--- | Lookup a typeclass from its name.
-tcLookupClass :: MonadTcPlugin m => Name -> m Class
-tcLookupClass = liftTcPluginM . GHC.tcLookupClass
-
--- | Lookup a global typecheckable-thing from its name.
-tcLookupGlobal :: MonadTcPlugin m => Name -> m TyThing
-tcLookupGlobal = liftTcPluginM . GHC.tcLookupGlobal
-
--- | Lookup a typecheckable-thing available in a local context,
--- such as a local type variable.
-tcLookup :: MonadTcPlugin m => Name -> m TcTyThing
-tcLookup = liftTcPluginM . GHC.tcLookup
-
--- | Lookup an identifier, such as a type variable.
-tcLookupId :: MonadTcPlugin m => Name -> m Id
-tcLookupId = liftTcPluginM . GHC.tcLookupId
-
---------------------------------------------------------------------------------
-
-{-
-getTopEnv :: MonadTcPlugin m => m HscEnv
-getTopEnv = liftTcPluginM GHC.getTopEnv
--}
-
--- | Obtain the current global and local type-checking environments.
-getEnvs :: MonadTcPlugin m => m ( TcGblEnv, TcLclEnv )
-getEnvs = liftTcPluginM GHC.getEnvs
-
--- | Obtain all currently-reachable typeclass instances.
-getInstEnvs :: MonadTcPlugin m => m InstEnvs
-getInstEnvs = liftTcPluginM GHC.getInstEnvs
-
--- | Obtain all currently-reachable data/type family instances.
---
--- First result: external instances.
--- Second result: instances in the current home package.
-getFamInstEnvs :: MonadTcPlugin m => m ( FamInstEnv, FamInstEnv )
-getFamInstEnvs = liftTcPluginM GHC.getFamInstEnvs
-
--- | Ask GHC what a type family application reduces to.
---
--- __Warning__: can cause a loop when used within 'tcPluginRewrite'.
-matchFam :: MonadTcPlugin m
-         => TyCon -> [ TcType ]
-         -> m ( Maybe Reduction )
-matchFam tycon args =
-#ifndef HAS_REWRITING
-  fmap ( \ (co,ty) -> mkReduction (mkSymCo co) ty ) <$>
-  -- GHC 9.0 and 9.2 use a different orientation
-  -- when rewriting type family applications.
-#endif
-  ( liftTcPluginM $ GHC.matchFam tycon args )
-
---------------------------------------------------------------------------------
-
--- | Create a new unique. Useful for generating new variables in the plugin.
-newUnique :: MonadTcPlugin m => m Unique
-newUnique = liftTcPluginM GHC.newUnique
-
--- | Create a new meta-variable (unification variable) of the given kind.
-newFlexiTyVar :: MonadTcPlugin m => Kind -> m TcTyVar
-newFlexiTyVar = liftTcPluginM . GHC.newFlexiTyVar
-
--- | Query whether a type variable is touchable:
---   - is it a unification variable (and not a skolem variable)?
---   - is it actually unifiable given the current 'TcLevel'?
-isTouchableTcPluginM :: MonadTcPlugin m => TcTyVar -> m Bool
-isTouchableTcPluginM = liftTcPluginM . GHC.isTouchableTcPluginM
-
---------------------------------------------------------------------------------
-
--- | Zonk the given type, which takes the metavariables in the type and
--- substitutes their actual value.
-zonkTcType :: MonadTcPluginWork m => TcType -> m TcType
-zonkTcType = liftTcPluginM . GHC.zonkTcType
-
--- | Zonk a given constraint.
-zonkCt :: MonadTcPluginWork m => Ct -> m Ct
-zonkCt = liftTcPluginM . GHC.zonkCt
-
---------------------------------------------------------------------------------
-
--- | Create a new Wanted constraint.
---
--- Requires a location (so that error messages can say where the constraint came from,
--- what things were in scope at that point, etc), as well as the actual constraint (encoded as a type).
-newWanted :: MonadTcPluginWork m => CtLoc -> PredType -> m CtEvidence
-newWanted loc pty =
-#if !HAS_REWRITING
-  -- On GHC 9.2 and below, 'newWanted' doesn't use the location information
-  -- that is passed to it, retrieving it from the 'TcM' environment instead.
-  -- https://gitlab.haskell.org/ghc/ghc/-/issues/20895
-  setCtLocM loc $
-#endif
-  liftTcPluginM $ GHC.newWanted loc pty
-
--- | Create a new Given constraint.
---
--- Unlike 'newWanted', we need to supply evidence for this constraint.
-newGiven :: CtLoc -> PredType -> EvExpr -> TcPluginM Solve CtEvidence
-newGiven loc pty evtm = do
-#if HAS_REWRITING
-  tc_evbinds <- askEvBinds
-  liftTcPluginM $ GHC.newGiven tc_evbinds loc pty evtm
-#else
-  liftTcPluginM $ GHC.newGiven loc pty evtm
-#endif
-
-
--- | Obtain the 'CtLoc' from a 'RewriteEnv'.
---
--- This can be useful to obtain the location of the
--- constraint currently being rewritten,
--- so that newly emitted constraints can be given
--- the same location information.
-rewriteEnvCtLoc :: RewriteEnv -> CtLoc
-rewriteEnvCtLoc =
-#if MIN_VERSION_ghc(9,3,0)
-  re_loc
-#else
-  fe_loc
-#endif
-
--- | Set the location information for a computation.
-setCtLocM :: MonadTcPluginWork m => CtLoc -> m a -> m a
-setCtLocM loc = unsafeLiftThroughTcM ( GHC.setCtLocM loc )
-
--- | Use the 'RewriteEnv' to set the 'CtLoc' for a computation.
-setCtLocRewriteM :: TcPluginM Rewrite a -> TcPluginM Rewrite a
-setCtLocRewriteM ma = do
-  rewriteCtLoc <- rewriteEnvCtLoc <$> askRewriteEnv
-  setCtLocM rewriteCtLoc ma
-
---------------------------------------------------------------------------------
-
--- | Create a fresh evidence variable.
-newEvVar :: PredType -> TcPluginM Solve EvVar
-newEvVar = liftTcPluginM . GHC.newEvVar
-
--- | Create a fresh coercion hole.
-newCoercionHole :: PredType -> TcPluginM Solve CoercionHole
-newCoercionHole = liftTcPluginM . GHC.newCoercionHole
-
--- | Bind an evidence variable.
-setEvBind :: EvBind -> TcPluginM Solve ()
-setEvBind ev_bind = do
-#if HAS_REWRITING
-  tc_evbinds <- askEvBinds
-  liftTcPluginM $ GHC.setEvBind tc_evbinds ev_bind
-#else
-  liftTcPluginM $ GHC.setEvBind ev_bind
-#endif
-
---------------------------------------------------------------------------------
-
--- | Conjure up a coercion witnessing an equality between two types
--- at the given 'Role' ('Nominal' or 'Representational').
---
--- This amounts to telling GHC "believe me, these things are equal".
---
--- The plugin is responsible for not emitting any unsound coercions,
--- such as a coercion between 'Int' and 'Float'.
-mkPluginUnivCo
-  :: String -- ^ Name of equality (for the plugin's internal use, or for debugging)
-  -> Role
-  -> TcType -- ^ LHS
-  -> TcType -- ^ RHS
-  -> Coercion
-mkPluginUnivCo str role lhs rhs = mkUnivCo ( PluginProv str ) role lhs rhs
-
--- | Conjure up an evidence term for an equality between two types
--- at the given 'Role' ('Nominal' or 'Representational').
---
--- This can be used to supply a proof of a wanted equality in 'TcPluginOk'.
---
--- The plugin is responsible for not emitting any unsound equalities,
--- such as an equality between 'Int' and 'Float'.
-mkPluginUnivEvTerm
-  :: String -- ^ Name of equality (for the plugin's internal use, or for debugging)
-  -> Role
-  -> TcType -- ^ LHS
-  -> TcType -- ^ RHS
-  -> EvTerm
-mkPluginUnivEvTerm str role lhs rhs = evCoercion $ mkPluginUnivCo str role lhs rhs
-
--- | Provide a rewriting of a saturated type family application
--- at the given 'Role' ('Nominal' or 'Representational').
---
--- The result can be passed to 'TcPluginRewriteTo' to specify the outcome
--- of rewriting a type family application.
-mkTyFamAppReduction
-  :: String   -- ^ Name of reduction (for debugging)
-  -> Role     -- ^ Role of reduction ('Nominal' or 'Representational')
-  -> TyCon    -- ^ Type family 'TyCon'
-  -> [TcType] -- ^ Type family arguments
-  -> TcType   -- ^ The type that the type family application reduces to
-  -> Reduction
-mkTyFamAppReduction str role tc args ty =
-  Reduction ( mkPluginUnivCo str role ( mkTyConApp tc args ) ty ) ty
-
---------------------------------------------------------------------------------
-
-#if !MIN_VERSION_ghc(9,0,0)
-
-type UniqFM ty a = GHC.UniqFM a
-
-mkUncheckedIntExpr :: Integer -> CoreExpr
-mkUncheckedIntExpr i = mkCoreConApps intDataCon [Lit lit]
-  where
-    lit = LitNumber LitNumInt i intPrimTy
-
-#if MIN_VERSION_ghc(8,10,0)
-
-mkInvisFunTyMany, mkVisFunTyMany :: Type -> Type -> Type
-mkInvisFunTyMany = mkInvisFunTy
-mkVisFunTyMany   = mkVisFunTy
-
-mkInvisFunTysMany, mkVisFunTysMany :: [Type] -> Type -> Type
-mkInvisFunTysMany = mkInvisFunTys
-mkVisFunTysMany   = mkVisFunTys
-
-#else
-
-type Pred = PredTree
-
-mkInvisFunTyMany, mkVisFunTyMany  :: Type -> Type -> Type
-mkInvisFunTyMany = mkFunTy
-mkVisFunTyMany   = mkFunTy
-
-mkInvisFunTysMany, mkVisFunTysMany :: [Type] -> Type -> Type
-mkInvisFunTysMany = mkFunTys
-mkVisFunTysMany = mkFunTys
-
-mkPiTy :: TyCoBinder -> Type -> Type
-mkPiTy bndr ty = mkPiTys [bndr] ty
-
--- | Makes a lifted equality predicate at the given role
-mkPrimEqPredRole :: Role -> Type -> Type -> PredType
-mkPrimEqPredRole Nominal          = mkPrimEqPred
-mkPrimEqPredRole Representational = mkReprPrimEqPred
-mkPrimEqPredRole Phantom          = panic "mkPrimEqPredRole phantom"
-
-#endif
-#endif
+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE UndecidableInstances #-}++{-|+Module: GHC.TcPlugin.API++This module provides a unified interface for writing type-checking plugins for GHC.++It attempts to re-export all the functionality from GHC that is relevant to plugin authors,+as well as providing utility functions to streamline certain common operations such as+creating evidence (to solve constraints), rewriting type family applications, throwing custom type errors.++Consider making use of the table of contents to help navigate this documentation;+don't hesitate to jump between sections to get an overview of the relevant aspects.++For an illustration of the functionality, check the examples in the associated+<https://github.com/sheaf/ghc-tcplugin-api GitHub repository>.++The internal module "GHC.TcPlugin.API.Internal" can be used to directly+lift and unlift computations in GHC's 'GHC.Tc.Types.TcM' monad, but it is hoped that+the interface provided in this module is sufficient.++-}++module GHC.TcPlugin.API+  ( -- * Basic TcPlugin functionality++    -- ** The 'TcPlugin' type+    TcPlugin(..)+  , mkTcPlugin++    -- ** Plugin state+    -- | A type-checker plugin can define its own state, corresponding to the existential parameter @s@+    -- in the definition of 'TcPlugin'.+    -- This allows a plugin to look up information a single time+    -- on initialisation, and pass it on for access in all further invocations of the plugin.+    --+    -- For example:+    --+    -- > data MyDefinitions { myTyFam :: !TyCon, myClass :: !Class }+    --+    -- Usually, the 'tcPluginInit' part of the plugin looks up all this information and returns it:+    --+    -- > myTcPluginInit :: TcPluginM Init MyDefinitions+    --+    -- This step should also be used to initialise any external tools,+    -- such as an external SMT solver.+    --+    -- This information will then be passed to other stages of the plugin:+    --+    -- > myTcPluginSolve :: MyDefinitions -> TcPluginSolver++    -- ** The type-checking plugin monads++    -- | Different stages of type-checking plugins have access to different information.+    -- For a unified interface, an MTL-style approach is used, with the 'MonadTcPlugin'+    -- typeclass providing overloading (for operations that work in all stages).+  , TcPluginStage(..), MonadTcPlugin+  , TcPluginM+  , tcPluginIO++    -- *** Emitting new work, and throwing type-errors++    -- | Some operations only make sense in the two main phases, solving and rewriting.+    -- This is captured by the 'MonadTcPluginWork' typeclass, which allows emitting+    -- new work, including throwing type errors.+  , MonadTcPluginWork+  , TcPluginErrorMessage(..)+  , mkTcPluginErrorTy++    -- * Name resolution++    -- | Name resolution is usually the first step in writing a type-checking plugin:+    -- plugins need to look up the names of the objects they want to manipulate.+    --+    -- For instance, to lookup the type family @MyFam@ in module @MyModule@ in package @my-pkg@:+    --+    -- > lookupMyModule :: MonadTcPlugin m => m Module+    -- > lookupMyModule = do+    -- >    findResult <- findImportedModule ( mkModuleName "MyModule" ) ( Just $ fsLit "my-pkg" )+    -- >    case findResult of+    -- >      Found _ myModule -> pure myModule+    -- >      _ -> error "MyPlugin couldn't find MyModule in my-pkg"+    -- >+    -- > lookupMyFam :: MonadTcPlugin m => Module -> m TyCon+    -- > lookupMyFam myModule = tcLookupTyCon =<< lookupOrig myModule ( mkTcOcc "MyFam" )+    --+    -- Most of these operations should be performed in 'tcPluginInit', and passed on+    -- to the other stages: the plugin initialisation is called only once in each module+    -- that the plugin is used, whereas the solver and rewriter are usually called repeatedly.++    -- ** Packages and modules++    -- | Use these functions to lookup a module,+    -- from the current package or imported packages.+  , findImportedModule, fsLit, unpackFS, mkModuleName+  , unitIdFS, stringToUnitId, pkgQual_pkg+  , Module, ModuleName, FindResult(..), UnitId, PkgQual(..)++    -- ** Names++    -- *** Occurence names++    -- | The most basic type of name is the 'OccName', which is a+    -- simple textual name within a namespace (e.g. the class namespace),+    -- without any disambiguation (no module qualifier, etc).+  , mkVarOcc, mkDataOcc, mkTyVarOcc, mkTcOcc, mkClsOcc++    -- *** Names++    -- | After having looked up the 'Module', we can obtain the full 'Name'+    -- referred to by an 'OccName'. This is fully unambiguous, as it+    -- contains a 'Unique' identifier for the name.+  , lookupOrig++    -- *** 'TyCon', 'Class', 'DataCon', etc++    -- | Finally, we can obtain the actual objects we're interested in handling,+    -- such as classes, type families, data constructors... by looking them up+    -- using their 'Name'.+  , tcLookupTyCon+  , tcLookupDataCon+  , tcLookupClass+  , tcLookupGlobal+  , tcLookup+  , tcLookupId+  , promoteDataCon++    -- * Constraint solving++    -- | Type-checking plugins will often want to manipulate constraints,+    -- e.g. solve constraints that GHC can't solve on its own, or emit+    -- their own constraints.+    --+    -- There are two different constraint flavours:+    --+    --   - Given constraints, which are already known and+    --     have evidence associated to them,+    --   - Wanted constraints, for which evidence has not yet been found.+    --+    -- When GHC can't solve a Wanted constraint, it will get reported to the+    -- user as a type error.++  , TcPluginSolver+#if HAS_REWRITING+  , TcPluginSolveResult(..)+#else+  , TcPluginSolveResult+  , pattern TcPluginContradiction, pattern TcPluginOk+#endif++    -- | The 'tcPluginSolve' method of a typechecker plugin will be invoked+    -- in two different ways:+    --+    -- 1. to simplify Given constraints. In this case, the 'tcPluginSolve' function+    --    will not be passed any Wanted constraints, and+    -- 2. to solve Wanted constraints.+    --+    -- The plugin can then respond in one of two ways:+    --+    --   - with @TcPluginOk solved new@, where @solved@ is a list of solved constraints+    --     and @new@ is a list of new constraints for GHC to process;+    --   - with @TcPluginContradiction contras@, where @contras@ is a list of impossible+    --     constraints, so that they can be turned into errors.+    --+    -- In both cases, the plugin must respond with constraints of the same flavour,+    -- i.e. in (1) it should return only Givens, and for (2) it should return only+    -- Wanteds; all other constraints will be ignored.++    -- ** Getting started with constraint solving++    -- | To get started, it can be helpful to immediately print out all the constraints+    -- that the plugin is given, using 'tcPluginTrace':+    --+    -- > solver _ givens wanteds = do+    -- >   tcPluginTrace "---Plugin start---" (ppr givens $$ ppr wanteds)+    -- >   pure $ TcPluginOk [] []+    --+    -- This creates a plugin that prints outs the constraints it is passed,+    -- without doing anything with them.+    --+    -- To see this output, you will need to pass the flags @-ddump-tc-trace@+    -- and @-ddump-to-file@ to GHC. This will output the trace as a log file,+    -- and you can search for @"---Plugin start---"@ to find the plugin inputs.+    --+    -- Note that pretty-printing in GHC is done using the 'Outputable' type class.+    -- We use its 'ppr' method to turn things into pretty-printable documents,+    -- and '($$)' to combine documents vertically.+    -- If you need more capabilities for pretty-printing documents,+    -- import GHC's "GHC.Utils.Outputable" module.+  , tcPluginTrace++    -- ** Inspecting constraints & predicates++    -- *** Canonical and non-canonical constraints++    -- | A constraint in GHC starts out as "non-canonical", which means that+    -- GHC doesn't know what type of constraint it is.+    -- GHC will inspect the constraint to turn it into a canonical form+    -- (class constraint, equality constraint, etc.) which satisfies certain+    -- invariants used during constraint solving.+    --+    -- Thus, whenever emitting new constraints, it is usually best to emit a+    -- non-canonical constraint, letting GHC canonicalise it.+  , mkNonCanonical++    -- *** Predicates++    -- | A type-checking plugin will usually need to inspect constraints,+    -- so that it can pick out the constraints it is going to interact with.+    --+    -- In general, type-checking plugins can encounter all sorts of constraints,+    -- whether in canonical form or not.+    -- In order to handle these constraints in a uniform manner, it is usually+    -- preferable to inspect each constraint's predicate, which can be obtained+    -- by using 'classifyPredType' and 'ctPred'.+    --+    -- This allows the plugin to determine what kind of constraints it is dealing with:+    --+    --   - an equality constraint? at 'Nominal' or 'Representational' role?+    --   - a type-class constraint? for which class?+    --   - an irreducible constraint, e.g. something of the form @c a@?+    --   - a quantified constraint?+  , Pred+  , pattern ClassPred, pattern EqPred, pattern IrredPred, pattern ForAllPred+  , classifyPredType, ctPred++    -- | == Handling type variables+  , TyVar, CoVar+  , MetaDetails, MetaInfo+  , isSkolemTyVar+  , isMetaTyVar, isFilledMetaTyVar_maybe+  , writeMetaTyVar++    -- | == Some further functions for inspecting constraints+  , eqType+  , ctLoc, ctEvidence, ctFlavour, ctEqRel, ctOrigin++    -- ** Constraint evidence++    -- *** Coercions++    -- | 'GHC.Core.TyCo.Rep.Coercion's are the evidence for type equalities.+    -- As such, when proving an equality, a type-checker plugin needs+    -- to construct the associated coercions.+  , mkPluginUnivCo+  , newCoercionHole+  , mkReflCo, mkSymCo, mkTransCo, mkUnivCo+  , mkCoercionTy, isCoercionTy, isCoercionTy_maybe++    -- *** Evidence terms++    -- | Typeclass constraints have a different notion of evidence: evidence terms.+    --+    -- A plugin that wants to solve a class constraint will need to provide+    -- an evidence term. Such evidence can be created from scratch, or it can be obtained+    -- by combining evidence that is already available.++  , mkPluginUnivEvTerm+  , evDataConApp+  , newEvVar, setEvBind+  , evCoercion, evCast+  , ctEvExpr+  , askEvBinds, lookupEvBind, eb_lhs, eb_rhs+  , newName, mkLocalId, mkTyVar+  , ctev_pred, ctev_evar, ctev_loc, ctev_dest++    -- *** Class dictionaries++    -- | To create evidence terms for class constraints, type-checking plugins+    -- need to be able to construct the appropriate dictionaries containing+    -- the values for the class methods.+    --+    -- The class dictionary constructor can be obtained using 'classDataCon'.+    -- Functions from "GHC.Core.Make", which is re-exported by this library,+    -- will be useful for constructing the necessary terms+    --+    -- For instance, we can apply the class data constructor using 'mkCoreConApps'.+    -- Remember that the type-level arguments (the typeclass variables) come first,+    -- before the actual evidence term (the class dictionary expression).++  , classDataCon+#if !MIN_VERSION_ghc(9,0,0)+  , mkUncheckedIntExpr+#endif++    -- | ==== Class instances++    -- | In some cases, a type-checking plugin might need to access the+    -- class instances that are currently in scope, e.g. to obtain certain+    -- evidence terms.+  , getInstEnvs++    -- ** Emitting new constraints++  , newWanted, newGiven++    -- | The following functions allow plugins to create constraints+    -- for typeclasses and type equalities.+  , mkClassPred, mkPrimEqPredRole++    -- | === Deriveds++    -- | Derived constraints are like Wanted constraints, except that they+    -- don't require evidence in order to be solved, and won't be seen+    -- in error messages if they go unsolved.+    --+    -- Solver plugins usually ignore this type of constraint entirely.+    -- They occur mostly when dealing with functional dependencies and type-family+    -- injectivity annotations.+    --+    -- GHC 9.4 removes this flavour of constraints entirely, subsuming their uses into+    -- Wanted constraints.+  , askDeriveds++    -- ** Location information and 'CtLoc's++    -- | When creating new constraints, one still needs a mechanism allowing GHC+    -- to report a certain source location associated to them when throwing an error,+    -- as well as other information the type-checker was aware of at that point+    -- (e.g. available instances, given constraints, etc).+    --+    -- This is the purpose of 'CtLoc'.+  , setCtLocM+  , setCtLocRewriteM++    -- | 'bumpCtLocDepth' adds one to the "depth" of the constraint.+    -- Can help avoid loops, by triggering a "maximum depth exceeded" error.+  , bumpCtLocDepth++    -- * Rewriting type-family applications++  , TcPluginRewriter, TcPluginRewriteResult(..)++    -- ** Querying for type family reductions++  , matchFam+  , getFamInstEnvs+  , FamInstEnv++    -- ** Specifying type family reductions++    -- | A plugin that wants to rewrite a type family application must provide two+    -- pieces of information:+    --+    --   - the type that the type family application reduces to,+    --   - evidence for this reduction, i.e. a 'GHC.Core.TyCo.Rep.Coercion' proving the equality.+    --+    -- In the rewriting stage, type-checking plugins have access to the rewriter+    -- environment 'RewriteEnv', which has information about the location of the+    -- type family application, the local type-checking environment, among other things.+    --+    -- Note that a plugin should provide a 'UniqFM' from 'TyCon' to rewriting functions,+    -- which specifies a rewriting function for each type family.+    -- Use 'emptyUFM' or 'listToUFM' to construct this map,+    -- or import the GHC module "GHC.Types.Unique.FM" for a more complete API.+  , askRewriteEnv, rewriteEnvCtLoc, RewriteEnv+  , mkTyFamAppReduction, Reduction(..)++    -- * Handling Haskell types++    -- ** Type variables+  , newUnique+  , newFlexiTyVar+  , isTouchableTcPluginM+  , mkTyVarTy, mkTyVarTys+  , isTyVarTy, getTyVar_maybe+  , TcType, TcTyVar, Unique, Kind++    -- ** Type literals (natural numbers, type-level strings)+  , mkNumLitTy, isNumLitTy+  , mkStrLitTy, isStrLitTy++    -- ** Creating and decomposing applications+  , mkTyConTy, mkTyConApp, mkAppTy, mkAppTys+  , splitTyConApp_maybe+  , tyConAppTyConPicky_maybe, tyConAppTyCon_maybe+  , splitAppTy_maybe, splitAppTys++    -- ** Function types+  , mkVisFunTyMany, mkVisFunTysMany+  , mkInvisFunTyMany, mkInvisFunTysMany+  , mkForAllTy, mkForAllTys+  , mkPiTy, mkPiTys++#if MIN_VERSION_ghc(9,0,0)+  , Mult, pattern One, pattern Many+#endif++    -- ** Zonking++    -- | Zonking is the operation in which GHC actually switches out mutable unification variables+    -- for their actual filled in type.+    --+    -- See the Note [What is zonking?] in GHC's source code for more information.+  , zonkTcType+  , zonkCt++    -- ** Panicking++    -- | It is often better for type-checking plugins to panic when encountering a problem,+    -- as opposed to silently doing something wrong. Use 'pprPanic' to throw an informative+    -- error message, so that users of your plugin can report an issue if a problem occurs.+  , panic, pprPanic++    -- ** Map-like data structures based on 'Unique's++    -- | Import "GHC.Types.Unique.FM" or "GHC.Types.Unique.DFM" for+    -- a more complete interface to maps whose keys are 'Unique's.++  , UniqDFM+  , lookupUDFM, lookupUDFM_Directly, elemUDFM+  , UniqFM+  , emptyUFM, listToUFM++    -- * The type-checking environment+  , getEnvs++    -- * Built-in types++    -- | This module also re-exports the built-in types that GHC already knows about.+    --+    -- This allows plugins to directly refer to e.g. the promoted data constructor+    -- 'True' without having to look up its name.+    --+    -- Refer to "GHC.Builtin.Names", "GHC.Builtin.Types" and "GHC.Builtin.Types.Prim".++    -- * GHC types++    -- | These are the types that the plugin will inspect and manipulate.++    -- | = END OF API DOCUMENTATION, RE-EXPORTS FOLLOW++    -- | == Some basic types++  , module GHC.Types.Basic++    -- | == Names+  , Name, OccName, TyThing, TcTyThing+  , MonadThings(..)+  , Class(classTyCon), DataCon, TyCon, Id+  , FastString++    -- | == Constraints+  , EqRel(..), FunDep, CtFlavour+  , Ct, CtLoc, CtEvidence, CtOrigin+  , QCInst+  , Type, PredType+  , InstEnvs, TcLevel++    -- | === Coercions and evidence+  , Coercion, Role(..), UnivCoProvenance+  , CoercionHole(..)+  , EvBind, EvTerm(EvExpr), EvVar, EvExpr, EvBindsVar+  , Expr(Var, Type, Coercion), CoreBndr, CoreExpr+  , TcEvDest(..)++    -- | == The type-checking environment+  , TcGblEnv, TcLclEnv++    -- | == Source locations+  , GenLocated(..), Located, RealLocated+  , unLoc, getLoc++    -- | == Pretty-printing+  , SDoc, Outputable(..)++  )+  where++-- ghc+import GHC+  ( TyThing(..) )+#if !MIN_VERSION_ghc(9,0,0)+import GHC.Builtin.Types+  ( intDataCon )+import GHC.Builtin.Types.Prim+  ( intPrimTy )+#endif+import GHC.Core+  ( CoreBndr, CoreExpr, Expr(..) )+import GHC.Core.Class+  ( Class(..), FunDep )+import GHC.Core.Coercion+  ( mkReflCo, mkSymCo, mkTransCo+  , mkUnivCo+#if MIN_VERSION_ghc(8,10,0)+  , mkPrimEqPredRole+#endif+  )+import GHC.Core.Coercion.Axiom+  ( Role(..) )+import GHC.Core.DataCon+  ( DataCon+  , classDataCon, promoteDataCon+  )+import GHC.Core.FamInstEnv+  ( FamInstEnv )+import GHC.Core.InstEnv+  ( InstEnvs(..) )+#if !MIN_VERSION_ghc(9,0,0)+import GHC.Core.Make+  ( mkCoreConApps )+#endif+import GHC.Core.Predicate+  ( EqRel(..)+#if MIN_VERSION_ghc(8,10,0)+  , Pred(..)+#else+  , PredTree(..), TyCoBinder+  , mkPrimEqPred, mkReprPrimEqPred+#endif+  , classifyPredType, mkClassPred+  )+#if HAS_REWRITING+import GHC.Core.Reduction+  ( Reduction(..) )+#endif+import GHC.Core.TyCon+  ( TyCon(..) )+import GHC.Core.TyCo.Rep+  ( Type, PredType, Kind+  , Coercion(..), CoercionHole(..)+  , UnivCoProvenance(..)+#if MIN_VERSION_ghc(9,0,0)+  , Mult+  , mkVisFunTyMany, mkVisFunTysMany+  , mkInvisFunTyMany, mkInvisFunTysMany+#elif MIN_VERSION_ghc(8,10,0)+  , mkVisFunTy, mkVisFunTys+  , mkInvisFunTy, mkInvisFunTys+#else+  , mkFunTy, mkFunTys+#endif+#if MIN_VERSION_ghc(8,10,0)+  , mkPiTy+#endif+  , mkPiTys+  , mkTyVarTy, mkTyVarTys+  , mkForAllTy, mkForAllTys+  )+import GHC.Core.Type+  ( eqType, mkTyConTy, mkTyConApp, splitTyConApp_maybe+  , splitAppTy_maybe, splitAppTys+  , tyConAppTyConPicky_maybe, tyConAppTyCon_maybe+  , mkAppTy, mkAppTys, isTyVarTy, getTyVar_maybe+  , mkCoercionTy, isCoercionTy, isCoercionTy_maybe+  , mkNumLitTy, isNumLitTy, mkStrLitTy, isStrLitTy+#if MIN_VERSION_ghc(9,0,0)+  , pattern One, pattern Many+#endif+  )+import GHC.Data.FastString+  ( FastString, fsLit, unpackFS )+import qualified GHC.Tc.Plugin+  as GHC+import GHC.Tc.Types+  ( TcTyThing(..), TcGblEnv(..), TcLclEnv(..)+#if HAS_REWRITING+  , TcPluginSolveResult(..), TcPluginRewriteResult(..)+  , RewriteEnv(..)+#endif+  )+import GHC.Tc.Types.Constraint+  ( Ct(..), CtLoc(..), CtEvidence(..), CtFlavour(..)+  , QCInst(..), TcEvDest(..)+  , ctPred, ctLoc, ctEvidence, ctEvExpr+  , ctFlavour, ctEqRel, ctOrigin+  , bumpCtLocDepth+  , mkNonCanonical+  )+import GHC.Tc.Types.Evidence+  ( EvBind(..), EvTerm(..), EvExpr, EvBindsVar(..)+  , evCoercion, evCast, lookupEvBind, evDataConApp+  )+import GHC.Tc.Types.Origin+  ( CtOrigin(..) )+import GHC.Tc.Utils.Monad+  ( newName )+import qualified GHC.Tc.Utils.Monad+  as GHC+    ( traceTc, setCtLocM )+import GHC.Tc.Utils.TcType+  ( TcType, TcLevel, MetaDetails, MetaInfo+  , isSkolemTyVar, isMetaTyVar+  )+import GHC.Tc.Utils.TcMType+  ( isFilledMetaTyVar_maybe, writeMetaTyVar )+import GHC.Types.Basic+  ( Arity, PromotionFlag(..), isPromoted+  , Boxity(..), TupleSort(..)+  )+import GHC.Types.Id+  ( Id, mkLocalId )+#if !MIN_VERSION_ghc(9,0,0)+import GHC.Types.Literal+  ( Literal(..), LitNumType(..) )+#endif+import GHC.Types.Name+  ( Name )+import GHC.Types.Name.Occurrence+  ( OccName(..)+  , mkVarOcc, mkDataOcc, mkTyVarOcc, mkTcOcc, mkClsOcc+  )+#if MIN_VERSION_ghc(9,3,0)+import GHC.Types.PkgQual+  ( PkgQual(..) )+#endif+import GHC.Types.SrcLoc+  ( GenLocated(..), Located, RealLocated+  , unLoc, getLoc+  )+import GHC.Types.Unique+  ( Unique )+#if MIN_VERSION_ghc(9,0,0)+import GHC.Types.Unique.FM as UniqFM+  ( UniqFM, emptyUFM, listToUFM )+#else+import qualified GHC.Types.Unique.FM as GHC+  ( UniqFM )+import GHC.Types.Unique.FM as UniqFM+  ( emptyUFM, listToUFM )+#endif+import GHC.Types.Unique.DFM+  ( UniqDFM, lookupUDFM, lookupUDFM_Directly, elemUDFM )+import GHC.Types.Var+  ( TyVar, CoVar, TcTyVar, EvVar+  , mkTyVar+  )+import GHC.Utils.Outputable+  ( Outputable(..), SDoc+#if !MIN_VERSION_ghc(9,2,0)+  , panic, pprPanic+#endif+#if !MIN_VERSION_ghc(9,3,0)+  , (<+>), doubleQuotes, empty, text+#endif+  )+#if MIN_VERSION_ghc(9,2,0)+import GHC.Utils.Panic+  ( panic, pprPanic )+#endif+#if MIN_VERSION_ghc(9,2,0)+import GHC.Unit.Finder+  ( FindResult(..) )+#else+import GHC.Driver.Finder+  ( FindResult(..) )+#endif+import GHC.Unit.Module+  ( UnitId, unitIdFS, stringToUnitId, mkModuleName )+#if MIN_VERSION_ghc(9,5,0)+import Language.Haskell.Syntax.Module.Name+  ( ModuleName )+#else+import GHC.Unit.Module.Name+  ( ModuleName )+#endif+import GHC.Unit.Types+  ( Module )++-- transformers+import Control.Monad.IO.Class+  ( MonadIO ( liftIO ) )++-- ghc-tcplugin-api+import GHC.TcPlugin.API.Internal+#ifndef HAS_REWRITING+import GHC.TcPlugin.API.Internal.Shim+#endif++--------------------------------------------------------------------------------++-- | Run an 'IO' computation within the plugin.+tcPluginIO :: MonadTcPlugin m => IO a -> m a+tcPluginIO = unsafeLiftTcM . liftIO++-- | Output some debugging information within the plugin.+tcPluginTrace :: MonadTcPlugin m+              => String -- ^ Text at the top of the debug message.+              -> SDoc   -- ^ Formatted document to print (use the 'ppr' pretty-printing function to obtain an 'SDoc' from any 'Outputable')+              -> m ()+tcPluginTrace a b = unsafeLiftTcM $ GHC.traceTc a b++--------------------------------------------------------------------------------++#if !MIN_VERSION_ghc(9,3,0)+-- | Package-qualifier after renaming+data PkgQual+  = NoPkgQual       -- ^ No package qualifier+  | ThisPkg  UnitId -- ^ Import from home-unit+  | OtherPkg UnitId -- ^ Import from another unit+  deriving stock ( Ord, Eq )++instance Outputable PkgQual where+  ppr = \case+    NoPkgQual  -> empty+    ThisPkg  u -> doubleQuotes (ppr u)+    OtherPkg u -> doubleQuotes (ppr u)+#endif++-- | Compatibility function to convert a 'PkgQual' to @Maybe FastString@+-- on older versions of GHC (9.2 and below).+--+-- On newer GHCs, this is the identity function.+pkgQual_pkg :: PkgQual+#if MIN_VERSION_ghc(9,3,0)+            -> PkgQual+#else+            -> Maybe FastString+#endif+pkgQual_pkg pkg =+#if MIN_VERSION_ghc(9,3,0)+  pkg+#else+  case pkg of+    NoPkgQual        -> Nothing+    ThisPkg  this    ->+      let fs = unitIdFS this+      in if fs == fsLit "this"+      then Just fs+      else pprPanic "pkgQual_pkg: \'ThisPkg\' package name should be \"this\"" (text "pkg:" <+> ppr pkg)+    OtherPkg unit_id -> Just $ unitIdFS unit_id+#endif++-- | Lookup a Haskell module from the given package.+findImportedModule :: MonadTcPlugin m+                   => ModuleName -- ^ Module name, e.g. @"Data.List"@.+                   -> PkgQual -- ^ Package name, e.g. @Just "base"@.+                              -- Use @Nothing@ for the current home package+                   -> m FindResult+findImportedModule mod_name pkg+  = liftTcPluginM+  $ GHC.findImportedModule mod_name (pkgQual_pkg pkg)++-- | Obtain the full internal 'Name' (with its unique identifier, etc) from its 'OccName'.+--+-- Example usage:+--+-- > lookupOrig preludeModule ( mkTcOcc "Bool" )+--+-- This will obtain the 'Name' associated with the type 'Bool'.+--+-- You can then call 'tcLookupTyCon' to obtain the associated 'TyCon'.+lookupOrig :: MonadTcPlugin m => Module -> OccName -> m Name+lookupOrig md = liftTcPluginM . GHC.lookupOrig md++-- | Lookup a type constructor from its name (datatype, type synonym or type family).+tcLookupTyCon :: MonadTcPlugin m => Name -> m TyCon+tcLookupTyCon = liftTcPluginM . GHC.tcLookupTyCon++-- | Lookup a data constructor (such as 'True', 'Just', ...) from its name.+tcLookupDataCon :: MonadTcPlugin m => Name -> m DataCon+tcLookupDataCon = liftTcPluginM . GHC.tcLookupDataCon++-- | Lookup a typeclass from its name.+tcLookupClass :: MonadTcPlugin m => Name -> m Class+tcLookupClass = liftTcPluginM . GHC.tcLookupClass++-- | Lookup a global typecheckable-thing from its name.+tcLookupGlobal :: MonadTcPlugin m => Name -> m TyThing+tcLookupGlobal = liftTcPluginM . GHC.tcLookupGlobal++-- | Lookup a typecheckable-thing available in a local context,+-- such as a local type variable.+tcLookup :: MonadTcPlugin m => Name -> m TcTyThing+tcLookup = liftTcPluginM . GHC.tcLookup++-- | Lookup an identifier, such as a type variable.+tcLookupId :: MonadTcPlugin m => Name -> m Id+tcLookupId = liftTcPluginM . GHC.tcLookupId++--------------------------------------------------------------------------------++{-+getTopEnv :: MonadTcPlugin m => m HscEnv+getTopEnv = liftTcPluginM GHC.getTopEnv+-}++-- | Obtain the current global and local type-checking environments.+getEnvs :: MonadTcPlugin m => m ( TcGblEnv, TcLclEnv )+getEnvs = liftTcPluginM GHC.getEnvs++-- | Obtain all currently-reachable typeclass instances.+getInstEnvs :: MonadTcPlugin m => m InstEnvs+getInstEnvs = liftTcPluginM GHC.getInstEnvs++-- | Obtain all currently-reachable data/type family instances.+--+-- First result: external instances.+-- Second result: instances in the current home package.+getFamInstEnvs :: MonadTcPlugin m => m ( FamInstEnv, FamInstEnv )+getFamInstEnvs = liftTcPluginM GHC.getFamInstEnvs++-- | Ask GHC what a type family application reduces to.+--+-- __Warning__: can cause a loop when used within 'tcPluginRewrite'.+matchFam :: MonadTcPlugin m+         => TyCon -> [ TcType ]+         -> m ( Maybe Reduction )+matchFam tycon args =+#ifndef HAS_REWRITING+  fmap ( \ (co,ty) -> mkReduction (mkSymCo co) ty ) <$>+  -- GHC 9.0 and 9.2 use a different orientation+  -- when rewriting type family applications.+#endif+  ( liftTcPluginM $ GHC.matchFam tycon args )++--------------------------------------------------------------------------------++-- | Create a new unique. Useful for generating new variables in the plugin.+newUnique :: MonadTcPlugin m => m Unique+newUnique = liftTcPluginM GHC.newUnique++-- | Create a new meta-variable (unification variable) of the given kind.+newFlexiTyVar :: MonadTcPlugin m => Kind -> m TcTyVar+newFlexiTyVar = liftTcPluginM . GHC.newFlexiTyVar++-- | Query whether a type variable is touchable:+--   - is it a unification variable (and not a skolem variable)?+--   - is it actually unifiable given the current 'TcLevel'?+isTouchableTcPluginM :: MonadTcPlugin m => TcTyVar -> m Bool+isTouchableTcPluginM = liftTcPluginM . GHC.isTouchableTcPluginM++--------------------------------------------------------------------------------++-- | Zonk the given type, which takes the metavariables in the type and+-- substitutes their actual value.+zonkTcType :: MonadTcPluginWork m => TcType -> m TcType+zonkTcType = liftTcPluginM . GHC.zonkTcType++-- | Zonk a given constraint.+zonkCt :: MonadTcPluginWork m => Ct -> m Ct+zonkCt = liftTcPluginM . GHC.zonkCt++--------------------------------------------------------------------------------++-- | Create a new Wanted constraint.+--+-- Requires a location (so that error messages can say where the constraint came from,+-- what things were in scope at that point, etc), as well as the actual constraint (encoded as a type).+newWanted :: MonadTcPluginWork m => CtLoc -> PredType -> m CtEvidence+newWanted loc pty =+#if !HAS_REWRITING+  -- On GHC 9.2 and below, 'newWanted' doesn't use the location information+  -- that is passed to it, retrieving it from the 'TcM' environment instead.+  -- https://gitlab.haskell.org/ghc/ghc/-/issues/20895+  setCtLocM loc $+#endif+  liftTcPluginM $ GHC.newWanted loc pty++-- | Create a new Given constraint.+--+-- Unlike 'newWanted', we need to supply evidence for this constraint.+newGiven :: CtLoc -> PredType -> EvExpr -> TcPluginM Solve CtEvidence+newGiven loc pty evtm = do+#if HAS_REWRITING+  tc_evbinds <- askEvBinds+  liftTcPluginM $ GHC.newGiven tc_evbinds loc pty evtm+#else+  liftTcPluginM $ GHC.newGiven loc pty evtm+#endif+++-- | Obtain the 'CtLoc' from a 'RewriteEnv'.+--+-- This can be useful to obtain the location of the+-- constraint currently being rewritten,+-- so that newly emitted constraints can be given+-- the same location information.+rewriteEnvCtLoc :: RewriteEnv -> CtLoc+rewriteEnvCtLoc =+#if MIN_VERSION_ghc(9,3,0)+  re_loc+#else+  fe_loc+#endif++-- | Set the location information for a computation.+setCtLocM :: MonadTcPluginWork m => CtLoc -> m a -> m a+setCtLocM loc = unsafeLiftThroughTcM ( GHC.setCtLocM loc )++-- | Use the 'RewriteEnv' to set the 'CtLoc' for a computation.+setCtLocRewriteM :: TcPluginM Rewrite a -> TcPluginM Rewrite a+setCtLocRewriteM ma = do+  rewriteCtLoc <- rewriteEnvCtLoc <$> askRewriteEnv+  setCtLocM rewriteCtLoc ma++--------------------------------------------------------------------------------++-- | Create a fresh evidence variable.+newEvVar :: PredType -> TcPluginM Solve EvVar+newEvVar = liftTcPluginM . GHC.newEvVar++-- | Create a fresh coercion hole.+newCoercionHole :: PredType -> TcPluginM Solve CoercionHole+newCoercionHole = liftTcPluginM . GHC.newCoercionHole++-- | Bind an evidence variable.+setEvBind :: EvBind -> TcPluginM Solve ()+setEvBind ev_bind = do+#if HAS_REWRITING+  tc_evbinds <- askEvBinds+  liftTcPluginM $ GHC.setEvBind tc_evbinds ev_bind+#else+  liftTcPluginM $ GHC.setEvBind ev_bind+#endif++--------------------------------------------------------------------------------++-- | Conjure up a coercion witnessing an equality between two types+-- at the given 'Role' ('Nominal' or 'Representational').+--+-- This amounts to telling GHC "believe me, these things are equal".+--+-- The plugin is responsible for not emitting any unsound coercions,+-- such as a coercion between 'Int' and 'Float'.+mkPluginUnivCo+  :: String -- ^ Name of equality (for the plugin's internal use, or for debugging)+  -> Role+  -> TcType -- ^ LHS+  -> TcType -- ^ RHS+  -> Coercion+mkPluginUnivCo str role lhs rhs = mkUnivCo ( PluginProv str ) role lhs rhs++-- | Conjure up an evidence term for an equality between two types+-- at the given 'Role' ('Nominal' or 'Representational').+--+-- This can be used to supply a proof of a wanted equality in 'TcPluginOk'.+--+-- The plugin is responsible for not emitting any unsound equalities,+-- such as an equality between 'Int' and 'Float'.+mkPluginUnivEvTerm+  :: String -- ^ Name of equality (for the plugin's internal use, or for debugging)+  -> Role+  -> TcType -- ^ LHS+  -> TcType -- ^ RHS+  -> EvTerm+mkPluginUnivEvTerm str role lhs rhs = evCoercion $ mkPluginUnivCo str role lhs rhs++-- | Provide a rewriting of a saturated type family application+-- at the given 'Role' ('Nominal' or 'Representational').+--+-- The result can be passed to 'TcPluginRewriteTo' to specify the outcome+-- of rewriting a type family application.+mkTyFamAppReduction+  :: String   -- ^ Name of reduction (for debugging)+  -> Role     -- ^ Role of reduction ('Nominal' or 'Representational')+  -> TyCon    -- ^ Type family 'TyCon'+  -> [TcType] -- ^ Type family arguments+  -> TcType   -- ^ The type that the type family application reduces to+  -> Reduction+mkTyFamAppReduction str role tc args ty =+  Reduction ( mkPluginUnivCo str role ( mkTyConApp tc args ) ty ) ty++--------------------------------------------------------------------------------++#if !MIN_VERSION_ghc(9,0,0)++type UniqFM ty a = GHC.UniqFM a++mkUncheckedIntExpr :: Integer -> CoreExpr+mkUncheckedIntExpr i = mkCoreConApps intDataCon [Lit lit]+  where+    lit = LitNumber LitNumInt i intPrimTy++#if MIN_VERSION_ghc(8,10,0)++mkInvisFunTyMany, mkVisFunTyMany :: Type -> Type -> Type+mkInvisFunTyMany = mkInvisFunTy+mkVisFunTyMany   = mkVisFunTy++mkInvisFunTysMany, mkVisFunTysMany :: [Type] -> Type -> Type+mkInvisFunTysMany = mkInvisFunTys+mkVisFunTysMany   = mkVisFunTys++#else++type Pred = PredTree++mkInvisFunTyMany, mkVisFunTyMany  :: Type -> Type -> Type+mkInvisFunTyMany = mkFunTy+mkVisFunTyMany   = mkFunTy++mkInvisFunTysMany, mkVisFunTysMany :: [Type] -> Type -> Type+mkInvisFunTysMany = mkFunTys+mkVisFunTysMany = mkFunTys++mkPiTy :: TyCoBinder -> Type -> Type+mkPiTy bndr ty = mkPiTys [bndr] ty++-- | Makes a lifted equality predicate at the given role+mkPrimEqPredRole :: Role -> Type -> Type -> PredType+mkPrimEqPredRole Nominal          = mkPrimEqPred+mkPrimEqPredRole Representational = mkReprPrimEqPred+mkPrimEqPredRole Phantom          = panic "mkPrimEqPredRole phantom"++#endif+#endif

@@ -1,575 +1,575 @@-{-# LANGUAGE BlockArguments #-}
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE DerivingVia #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE NamedFieldPuns #-}
-{-# LANGUAGE QuantifiedConstraints #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE RecordWildCards #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE UndecidableInstances #-}
-
-{-|
-Module: GHC.TcPlugin.API.Internal
-
-This module provides operations to directly lift and unlift computations in
-GHC's 'GHC.Tc.TcM' monad to the various type-checking plugin monads, in the form
-of the functions
-
-  > unsafeLiftTcM :: TcM a -> m a
-
-  > unsafeWithRunInTcM :: ( ( forall a. m a -> TcM a ) -> TcM b ) -> m b
-
-Here 'GHC.Tc.TcM' is GHC's internal type-checker monad.
-
-It also exposes extra environment available in the solving/rewriting stages:
-
-  > askRewriteEnv :: TcPluginM Rewrite RewriteEnv
-
-  > askEvBinds :: TcPluginM Solve EvBindsVar
-
-It is hoped that none of these internal operations are necessary, and that users
-can fulfill their needs without importing this internal module.
-
-Please file a bug on the issue tracker if you have encountered a situation
-which requires the import of this module.
-
--}
-
-module GHC.TcPlugin.API.Internal
-  ( -- * Internal functions and types
-    MonadTcPlugin(..), MonadTcPluginWork
-  , unsafeLiftThroughTcM
-    -- * Re-exported functions and types
-  , TcPlugin(..), TcPluginStage(..)
-  , TcPluginSolver
-  , TcPluginM(..)
-  , TcPluginErrorMessage(..)
-  , TcPluginRewriter
-  , MonadThings(..)
-  , askRewriteEnv
-  , askDeriveds
-  , askEvBinds
-  , mkTcPlugin
-  , mkTcPluginErrorTy
-  )
-  where
-
--- base
-import Data.Coerce
-  ( Coercible )
-import Data.Kind
-  ( Type )
-import GHC.TypeLits
-  ( TypeError, ErrorMessage(..) )
-
--- transformers
-import Control.Monad.Trans.Reader
-  ( ReaderT(..) )
-
--- ghc
-import qualified GHC.Builtin.Names
-  as GHC.TypeLits
-    ( errorMessageTypeErrorFamName
-    , typeErrorTextDataConName
-    , typeErrorAppendDataConName
-    , typeErrorVAppendDataConName
-    , typeErrorShowTypeDataConName
-    )
-import qualified GHC.Builtin.Types
-  as GHC
-    ( constraintKind )
-import qualified GHC.Core.DataCon
-  as GHC
-    ( promoteDataCon )
-import qualified GHC.Core.TyCon
-  as GHC
-    ( TyCon )
-import qualified GHC.Core.TyCo.Rep
-  as GHC
-    ( PredType, Type(..), TyLit(..) )
-import qualified GHC.Core.Type
-  as GHC
-    ( mkTyConApp, tcTypeKind )
-import qualified GHC.Data.FastString
-  as GHC
-    ( fsLit )
-import qualified GHC.Tc.Plugin
-  as GHC
-    ( tcLookupDataCon, tcLookupTyCon )
-import qualified GHC.Tc.Types
-  as GHC
-    ( TcM, TcPlugin(..), TcPluginM
-    , TcPluginSolver
-#ifdef HAS_REWRITING
-    , TcPluginRewriter
-#else
-    , getEvBindsTcPluginM
-#endif
-    , runTcPluginM, unsafeTcPluginTcM
-    )
-#ifdef HAS_REWRITING
-import GHC.Tc.Types
-    ( TcPluginSolveResult
-    , TcPluginRewriteResult
-    , RewriteEnv
-    )
-#endif
-import qualified GHC.Tc.Types.Constraint
-  as GHC
-    ( Ct )
-import qualified GHC.Tc.Types.Evidence
-  as GHC
-    ( EvBindsVar )
-import qualified GHC.Types.Unique.FM
-  as GHC
-    ( UniqFM )
-#if MIN_VERSION_ghc(9,1,0)
-import GHC.Types.TyThing
-  ( MonadThings(..) )
-#else
-import GHC.Driver.Types
-  ( MonadThings(..) )
-#endif
-
--- ghc-tcplugin-api
-#ifndef HAS_REWRITING
-import GHC.TcPlugin.API.Internal.Shim
-  ( TcPluginSolveResult, TcPluginRewriteResult(..)
-  , RewriteEnv
-  , shimRewriter
-  )
-#endif
-
---------------------------------------------------------------------------------
--- Public types and functions.
-
--- | Stage of a type-checking plugin, used as a data kind.
-data TcPluginStage
-  = Init
-  | Solve
-  | Rewrite
-  | Stop
-
--- | The @solve@ function of a type-checking plugin takes in Given and Wanted
--- constraints, and should return a 'GHC.Tc.Types.TcPluginSolveResult'
--- indicating which Wanted constraints it could solve, or whether any are
--- insoluble.
-type TcPluginSolver
-  =  [GHC.Ct] -- ^ Givens
-  -> [GHC.Ct] -- ^ Wanteds
-  -> TcPluginM Solve TcPluginSolveResult
-
--- | For rewriting type family applications, a type-checking plugin provides
--- a function of this type for each type family 'GHC.Core.TyCon.TyCon'.
---
--- The function is provided with the current set of Given constraints, together
--- with the arguments to the type family.
--- The type family application will always be fully saturated.
-type TcPluginRewriter
-  =  [GHC.Ct]     -- ^ Givens
-  -> [GHC.Type]   -- ^ Type family arguments (saturated)
-  -> TcPluginM Rewrite TcPluginRewriteResult
-
--- | A record containing all the stages necessary for the
--- operation of a type-checking plugin, as defined in this API.
---
--- __Note__: this is not the same record as GHC's built-in
--- 'GHC.Tc.Types.TcPlugin' record. Use 'mkTcPlugin' for the conversion.
---
--- To create a type-checking plugin, define something of this type
--- and then call 'mkTcPlugin' on the result.
--- This will return something that can be passed to 'GHC.Plugins.Plugin':
---
--- > plugin :: GHC.Plugins.Plugin
--- > plugin =
--- >   GHC.Plugins.defaultPlugin
--- >     { GHC.Plugins.tcPlugin =
--- >         \ args -> Just $
--- >            GHC.TcPlugin.API.mkTcPlugin ( myTcPlugin args )
--- >     }
--- >
--- > myTcPlugin :: [String] -> GHC.TcPlugin.API.TcPlugin
--- > myTcPlugin args = ...
-data TcPlugin = forall s. TcPlugin
-  { tcPluginInit :: TcPluginM Init s
-      -- ^ Initialise plugin, when entering type-checker.
-
-  , tcPluginSolve :: s -> TcPluginSolver
-      -- ^ Solve some constraints.
-      --
-      -- This function will be invoked at two points in the constraint solving
-      -- process: once to manipulate given constraints, and once to solve
-      -- wanted constraints. In the first case (and only in the first case),
-      -- no wanted constraints will be passed to the plugin.
-      --
-      -- The plugin can either return a contradiction,
-      -- or specify that it has solved some constraints (with evidence),
-      -- and possibly emit additional wanted constraints.
-      --
-      -- Use @ \\ _ _ _ -> pure $ TcPluginOK [] [] @ if your plugin
-      -- does not provide this functionality.
-
-  , tcPluginRewrite
-      :: s -> GHC.UniqFM
-#if MIN_VERSION_ghc(9,0,0)
-                GHC.TyCon
-#endif
-                TcPluginRewriter
-    -- ^ Rewrite saturated type family applications.
-    --
-    -- The plugin is expected to supply a mapping from type family names to
-    -- rewriting functions. For each type family 'GHC.Core.TyCon.TyCon',
-    -- the plugin should provide a function which takes in the given constraints
-    -- and arguments of a saturated type family application, and return
-    -- a possible rewriting.
-    -- See 'TcPluginRewriter' for the expected shape of such a function.
-    --
-    -- Use @ const emptyUFM @ if your plugin does not provide this functionality.
-
-  , tcPluginStop :: s -> TcPluginM Stop ()
-   -- ^ Clean up after the plugin, when exiting the type-checker.
-  }
-
--- | The monad used for a type-checker plugin, parametrised by
--- the 'TcPluginStage' of the plugin.
-data family TcPluginM (s :: TcPluginStage) :: Type -> Type
-newtype instance TcPluginM Init a =
-  TcPluginInitM { tcPluginInitM :: GHC.TcPluginM a }
-  deriving newtype ( Functor, Applicative, Monad )
-#ifdef HAS_DERIVEDS
-newtype instance TcPluginM Solve a =
-  TcPluginSolveM { tcPluginSolveM :: BuiltinDefs -> GHC.EvBindsVar -> [GHC.Ct] -> GHC.TcPluginM a }
-  deriving ( Functor, Applicative, Monad )
-    via ( ReaderT BuiltinDefs ( ReaderT GHC.EvBindsVar ( ReaderT [GHC.Ct] GHC.TcPluginM ) ) )
-#else
-newtype instance TcPluginM Solve a =
-  TcPluginSolveM { tcPluginSolveM :: BuiltinDefs -> GHC.EvBindsVar -> GHC.TcPluginM a }
-  deriving ( Functor, Applicative, Monad )
-    via ( ReaderT BuiltinDefs ( ReaderT GHC.EvBindsVar GHC.TcPluginM ) )
-#endif
-newtype instance TcPluginM Rewrite a =
-  TcPluginRewriteM { tcPluginRewriteM :: BuiltinDefs -> RewriteEnv -> GHC.TcPluginM a }
-  deriving ( Functor, Applicative, Monad )
-    via ( ReaderT BuiltinDefs ( ReaderT RewriteEnv GHC.TcPluginM ) )
-newtype instance TcPluginM Stop a =
-  TcPluginStopM { tcPluginStopM :: GHC.TcPluginM a }
-  deriving newtype ( Functor, Applicative, Monad )
-
--- | Ask for the evidence currently gathered by the type-checker.
---
--- Only available in the solver part of the type-checking plugin.
-askEvBinds :: TcPluginM Solve GHC.EvBindsVar
-askEvBinds = TcPluginSolveM
-  \ _defs
-    evBinds
-#ifdef HAS_DERIVEDS
-    _deriveds
-#endif
-  -> pure evBinds
-
--- | Ask for the Derived constraints that the solver was provided with.
---
--- Always returns the empty list on GHC 9.4 or above.
-askDeriveds :: TcPluginM Solve [GHC.Ct]
-askDeriveds =
-#ifdef HAS_DERIVEDS
-  TcPluginSolveM \ _defs _evBinds deriveds -> pure deriveds
-#else
-  pure []
-#endif
-
--- | Ask for the current rewriting environment.
---
--- Only available in the rewriter part of the type-checking plugin.
-askRewriteEnv :: TcPluginM Rewrite RewriteEnv
-askRewriteEnv = TcPluginRewriteM ( \ _ rewriteEnv -> pure rewriteEnv )
-
--- | A 'MonadTcPlugin' is essentially a reader monad over GHC's 'GHC.Tc.TcM' monad.
---
--- This means we have both a @lift@ and an @unlift@ operation,
--- similar to @MonadUnliftIO@ or @MonadBaseControl@.
---
--- See for instance 'unsafeLiftThroughTcM', which is an example of function that
--- one would not be able to write using only a @lift@ operation.
---
--- Note that you must import the internal module in order to access the methods.
--- Please report a bug if you find yourself needing this functionality.
-class ( Monad m, ( forall x y. Coercible x y => Coercible (m x) (m y) ) ) => MonadTcPlugin (m :: Type -> Type) where
-
-  {-# MINIMAL liftTcPluginM, unsafeWithRunInTcM #-}
-
-  -- N.B.: these methods are not re-exported from the main module.
-
-  -- | Lift a computation from GHC's 'GHC.TcPluginM' monad.
-  liftTcPluginM :: GHC.TcPluginM a -> m a
-
-  -- | Lift a computation from the 'GHC.Tc.TcM' monad.
-  unsafeLiftTcM :: GHC.TcM a -> m a
-  unsafeLiftTcM = liftTcPluginM . GHC.unsafeTcPluginTcM
-
-  -- | Unlift a computation from the 'GHC.Tc.TcM' monad.
-  --
-  -- If this type signature seems confusing, I recommend reading Alexis King's
-  -- excellent blog post on @MonadBaseControl@:
-  --
-  -- <https://lexi-lambda.github.io/blog/2019/09/07/demystifying-monadbasecontrol/ Demystifying MonadBaseControl>
-  unsafeWithRunInTcM :: ( ( forall a. m a -> GHC.TcM a ) -> GHC.TcM b ) -> m b
-
-instance MonadTcPlugin ( TcPluginM Init ) where
-  liftTcPluginM = TcPluginInitM
-  unsafeWithRunInTcM runInTcM
-    = unsafeLiftTcM $ runInTcM
-#ifdef HAS_REWRITING
-      ( GHC.runTcPluginM . tcPluginInitM )
-#else
-      ( ( `GHC.runTcPluginM` ( error "tcPluginInit: cannot access EvBindsVar" ) ) . tcPluginInitM )
-#endif
-instance MonadTcPlugin ( TcPluginM Solve ) where
-  liftTcPluginM  = TcPluginSolveM
-#ifdef HAS_DERIVEDS
-                 . ( \ ma _defs _evBinds _deriveds -> ma )
-#else
-                 . ( \ ma _defs _evBinds -> ma )
-#endif
-  unsafeWithRunInTcM runInTcM
-    = TcPluginSolveM
-      \ builtinDefs
-        evBinds
-#ifdef HAS_DERIVEDS
-        deriveds
-#endif
-      ->
-        GHC.unsafeTcPluginTcM $ runInTcM
-#ifdef HAS_REWRITING
-  -- (no deriveds)
-          ( GHC.runTcPluginM
-          . ( \ f -> f builtinDefs evBinds )
-          . tcPluginSolveM )
-#else
-          ( ( `GHC.runTcPluginM` evBinds )
-          . ( \ f -> f builtinDefs evBinds deriveds )
-          . tcPluginSolveM
-          )
-#endif
-instance MonadTcPlugin ( TcPluginM Rewrite ) where
-  liftTcPluginM = TcPluginRewriteM . ( \ ma _ _ -> ma )
-  unsafeWithRunInTcM runInTcM
-    = TcPluginRewriteM \ builtinDefs rewriteEnv ->
-      GHC.unsafeTcPluginTcM $ runInTcM
-#ifdef HAS_REWRITING
-        ( GHC.runTcPluginM
-#else
-        ( ( `GHC.runTcPluginM` ( error "tcPluginRewrite: cannot access EvBindsVar" ) )
-#endif
-        . ( \ f -> f builtinDefs rewriteEnv )
-        . tcPluginRewriteM )
-instance MonadTcPlugin ( TcPluginM Stop ) where
-  liftTcPluginM = TcPluginStopM
-  unsafeWithRunInTcM runInTcM
-    = unsafeLiftTcM $ runInTcM
-#ifdef HAS_REWRITING
-      ( GHC.runTcPluginM . tcPluginStopM )
-#else
-      ( ( `GHC.runTcPluginM` ( error "tcPluginStop: cannot access EvBindsVar" ) ) . tcPluginStopM )
-#endif
-
--- | Take a function whose argument and result types are both within the 'GHC.Tc.TcM' monad,
--- and return a function that works within a type-checking plugin monad.
---
--- Please report a bug if you find yourself needing to use this function.
-unsafeLiftThroughTcM :: MonadTcPlugin m => ( GHC.TcM a -> GHC.TcM b ) -> m a -> m b
-unsafeLiftThroughTcM f ma = unsafeWithRunInTcM \ runInTcM -> f ( runInTcM ma )
-
--- | Use this function to create a type-checker plugin to pass to GHC.
-mkTcPlugin
-  :: TcPlugin     -- ^ type-checking plugin written with this library
-  -> GHC.TcPlugin -- ^ type-checking plugin for GHC
-mkTcPlugin ( TcPlugin
-              { tcPluginInit = tcPluginInit :: TcPluginM Init userDefs
-              , tcPluginSolve
-              , tcPluginRewrite
-              , tcPluginStop
-              }
-           ) =
-  GHC.TcPlugin
-    { GHC.tcPluginInit    = adaptUserInit    tcPluginInit
-#ifdef HAS_REWRITING
-    , GHC.tcPluginSolve   = adaptUserSolve   tcPluginSolve
-    , GHC.tcPluginRewrite = adaptUserRewrite tcPluginRewrite
-#else
-    , GHC.tcPluginSolve   = adaptUserSolveAndRewrite
-                              tcPluginSolve tcPluginRewrite
-#endif
-    , GHC.tcPluginStop    = adaptUserStop    tcPluginStop
-    }
-  where
-    adaptUserInit :: TcPluginM Init userDefs -> GHC.TcPluginM ( TcPluginDefs userDefs )
-    adaptUserInit userInit = do
-      tcPluginBuiltinDefs <- initBuiltinDefs
-      tcPluginUserDefs    <- tcPluginInitM userInit
-      pure ( TcPluginDefs { tcPluginBuiltinDefs, tcPluginUserDefs })
-
-#ifdef HAS_REWRITING
-  -- (no deriveds)
-    adaptUserSolve :: ( userDefs -> TcPluginSolver )
-                   -> TcPluginDefs userDefs
-                   -> GHC.TcPluginSolver
-    adaptUserSolve userSolve ( TcPluginDefs { tcPluginUserDefs, tcPluginBuiltinDefs } )
-      = \ evBindsVar givens wanteds -> do
-        tcPluginSolveM ( userSolve tcPluginUserDefs givens wanteds )
-          tcPluginBuiltinDefs evBindsVar
-    adaptUserRewrite :: ( userDefs -> GHC.UniqFM GHC.TyCon TcPluginRewriter )
-                     -> TcPluginDefs userDefs -> GHC.UniqFM GHC.TyCon GHC.TcPluginRewriter
-    adaptUserRewrite userRewrite ( TcPluginDefs { tcPluginUserDefs, tcPluginBuiltinDefs })
-      = fmap
-          ( \ userRewriter rewriteEnv givens tys ->
-            tcPluginRewriteM ( userRewriter givens tys ) tcPluginBuiltinDefs rewriteEnv
-          )
-          ( userRewrite tcPluginUserDefs )
-#else
-    adaptUserSolveAndRewrite
-      :: ( userDefs -> TcPluginSolver )
-      -> ( userDefs -> GHC.UniqFM
-#if MIN_VERSION_ghc(9,0,0)
-                         GHC.TyCon
-#endif
-                         TcPluginRewriter
-         )
-      -> TcPluginDefs userDefs
-      -> GHC.TcPluginSolver
-    adaptUserSolveAndRewrite userSolve userRewrite ( TcPluginDefs { tcPluginUserDefs, tcPluginBuiltinDefs } )
-      = \ givens deriveds wanteds -> do
-        evBindsVar <- GHC.getEvBindsTcPluginM
-        shimRewriter
-          givens deriveds wanteds
-          ( fmap
-              ( \ userRewriter rewriteEnv gs tys ->
-                tcPluginRewriteM ( userRewriter gs tys )
-                  tcPluginBuiltinDefs rewriteEnv
-              )
-              ( userRewrite tcPluginUserDefs )
-          )
-          ( \ gs ds ws ->
-            tcPluginSolveM ( userSolve tcPluginUserDefs gs ws )
-              tcPluginBuiltinDefs evBindsVar ds
-          )
-#endif
-
-    adaptUserStop :: ( userDefs -> TcPluginM Stop () ) -> TcPluginDefs userDefs -> GHC.TcPluginM ()
-    adaptUserStop userStop ( TcPluginDefs { tcPluginUserDefs } ) =
-      tcPluginStopM $ userStop tcPluginUserDefs
-
--- | Monads for type-checking plugins which are able to emit new constraints
--- and throw errors.
---
--- These operations are supported by the monads that 'tcPluginSolve'
--- and 'tcPluginRewrite' use; it is not possible to emit work or
--- throw type errors in 'tcPluginInit' or 'tcPluginStop'.
---
--- See 'mkTcPluginErrorTy' and 'GHC.TcPlugin.API.emitWork' for functions
--- which require this typeclass.
-class MonadTcPlugin m => MonadTcPluginWork m where
-  {-# MINIMAL #-} -- to avoid the methods appearing in the haddocks
-  askBuiltins :: m BuiltinDefs
-  askBuiltins = error "askBuiltins: no default implementation"
-instance MonadTcPluginWork ( TcPluginM Solve ) where
-  askBuiltins = TcPluginSolveM
-    \ builtinDefs
-      _evBinds
-#ifdef HAS_DERIVEDS
-      _deriveds
-#endif
-    -> pure builtinDefs
-instance MonadTcPluginWork ( TcPluginM Rewrite ) where
-  askBuiltins = TcPluginRewriteM \ builtinDefs _evBinds -> pure builtinDefs
-
-instance TypeError ( 'Text "Cannot emit new work in 'tcPluginInit'." )
-      => MonadTcPluginWork ( TcPluginM Init ) where
-  askBuiltins = error "Cannot emit new work in 'tcPluginInit'."
-instance TypeError ( 'Text "Cannot emit new work in 'tcPluginStop'." )
-      => MonadTcPluginWork ( TcPluginM Stop ) where
-  askBuiltins = error "Cannot emit new work in 'tcPluginStop'."
-
--- | Use this type like 'GHC.TypeLits.ErrorMessage' to write an error message.
--- This error message can then be thrown at the type-level by the plugin,
--- by emitting a wanted constraint whose predicate is obtained from 'mkTcPluginErrorTy'.
---
--- A 'GHC.Tc.Types.Constraint.CtLoc' will still need to be provided in order to inform GHC of the
--- origin of the error (e.g.: which part of the source code should be
--- highlighted?). See 'GHC.TcPlugin.API.setCtLocM'.
-data TcPluginErrorMessage
-  = Txt !String
-  -- ^ Show the text as is.
-  | PrintType !GHC.Type
-  -- ^ Pretty print the given type.
-  | (:|:) !TcPluginErrorMessage !TcPluginErrorMessage
-  -- ^ Put two messages side by side.
-  | (:-:) !TcPluginErrorMessage !TcPluginErrorMessage
-  -- ^ Stack two messages vertically.
-infixl 5 :|:
-infixl 6 :-:
-
--- | Create an error type with the desired error message.
---
--- The result can be paired with a 'GHC.Tc.Types.Constraint.CtLoc' in order to throw a type error,
--- for instance by using 'GHC.TcPlugin.API.newWanted'.
-mkTcPluginErrorTy :: MonadTcPluginWork m => TcPluginErrorMessage -> m GHC.PredType
-mkTcPluginErrorTy msg = do
-  builtinDefs@( BuiltinDefs { typeErrorTyCon } ) <- askBuiltins
-  let
-    errorMsgTy :: GHC.PredType
-    errorMsgTy = interpretErrorMessage builtinDefs msg
-  pure $ GHC.mkTyConApp typeErrorTyCon [ GHC.constraintKind, errorMsgTy ]
-
-instance ( Monad (TcPluginM s), MonadTcPlugin (TcPluginM s) )
-      => MonadThings (TcPluginM s) where
-  lookupThing = unsafeLiftTcM . lookupThing
-
---------------------------------------------------------------------------------
--- Private types and functions.
--- Not exposed at all, even from the internal module.
-
-data BuiltinDefs =
-  BuiltinDefs
-    { typeErrorTyCon :: !GHC.TyCon
-    , textTyCon      :: !GHC.TyCon
-    , showTypeTyCon  :: !GHC.TyCon
-    , concatTyCon    :: !GHC.TyCon
-    , vcatTyCon      :: !GHC.TyCon
-    }
-
-data TcPluginDefs s
-  = TcPluginDefs
-  { tcPluginBuiltinDefs :: !BuiltinDefs
-  , tcPluginUserDefs    :: !s
-  }
-
-initBuiltinDefs :: GHC.TcPluginM BuiltinDefs
-initBuiltinDefs = do
-  typeErrorTyCon  <-                        GHC.tcLookupTyCon   GHC.TypeLits.errorMessageTypeErrorFamName
-  textTyCon       <- GHC.promoteDataCon <$> GHC.tcLookupDataCon GHC.TypeLits.typeErrorTextDataConName
-  showTypeTyCon   <- GHC.promoteDataCon <$> GHC.tcLookupDataCon GHC.TypeLits.typeErrorShowTypeDataConName
-  concatTyCon     <- GHC.promoteDataCon <$> GHC.tcLookupDataCon GHC.TypeLits.typeErrorAppendDataConName
-  vcatTyCon       <- GHC.promoteDataCon <$> GHC.tcLookupDataCon GHC.TypeLits.typeErrorVAppendDataConName
-  pure ( BuiltinDefs { .. } )
-
-interpretErrorMessage :: BuiltinDefs -> TcPluginErrorMessage -> GHC.PredType
-interpretErrorMessage ( BuiltinDefs { .. } ) = go
-  where
-    go :: TcPluginErrorMessage -> GHC.PredType
-    go ( Txt str ) =
-      GHC.mkTyConApp textTyCon [ GHC.LitTy . GHC.StrTyLit . GHC.fsLit $ str ]
-    go ( PrintType ty ) =
-      GHC.mkTyConApp showTypeTyCon [ GHC.tcTypeKind ty, ty ]
-        -- The kind gets ignored by GHC when printing the error message (see GHC.Core.Type.pprUserTypeErrorTy).
-        -- However, including the wrong kind can lead to ASSERT failures, so we compute the kind and pass it.
-    go ( msg1 :|: msg2 ) =
-      GHC.mkTyConApp concatTyCon [ go msg1, go msg2 ]
-    go ( msg1 :-: msg2 ) =
-      GHC.mkTyConApp vcatTyCon [ go msg1, go msg2 ]
+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}++{-|+Module: GHC.TcPlugin.API.Internal++This module provides operations to directly lift and unlift computations in+GHC's 'GHC.Tc.TcM' monad to the various type-checking plugin monads, in the form+of the functions++  > unsafeLiftTcM :: TcM a -> m a++  > unsafeWithRunInTcM :: ( ( forall a. m a -> TcM a ) -> TcM b ) -> m b++Here 'GHC.Tc.TcM' is GHC's internal type-checker monad.++It also exposes extra environment available in the solving/rewriting stages:++  > askRewriteEnv :: TcPluginM Rewrite RewriteEnv++  > askEvBinds :: TcPluginM Solve EvBindsVar++It is hoped that none of these internal operations are necessary, and that users+can fulfill their needs without importing this internal module.++Please file a bug on the issue tracker if you have encountered a situation+which requires the import of this module.++-}++module GHC.TcPlugin.API.Internal+  ( -- * Internal functions and types+    MonadTcPlugin(..), MonadTcPluginWork+  , unsafeLiftThroughTcM+    -- * Re-exported functions and types+  , TcPlugin(..), TcPluginStage(..)+  , TcPluginSolver+  , TcPluginM(..)+  , TcPluginErrorMessage(..)+  , TcPluginRewriter+  , MonadThings(..)+  , askRewriteEnv+  , askDeriveds+  , askEvBinds+  , mkTcPlugin+  , mkTcPluginErrorTy+  )+  where++-- base+import Data.Coerce+  ( Coercible )+import Data.Kind+  ( Type )+import GHC.TypeLits+  ( TypeError, ErrorMessage(..) )++-- transformers+import Control.Monad.Trans.Reader+  ( ReaderT(..) )++-- ghc+import qualified GHC.Builtin.Names+  as GHC.TypeLits+    ( errorMessageTypeErrorFamName+    , typeErrorTextDataConName+    , typeErrorAppendDataConName+    , typeErrorVAppendDataConName+    , typeErrorShowTypeDataConName+    )+import qualified GHC.Builtin.Types+  as GHC+    ( constraintKind )+import qualified GHC.Core.DataCon+  as GHC+    ( promoteDataCon )+import qualified GHC.Core.TyCon+  as GHC+    ( TyCon )+import qualified GHC.Core.TyCo.Rep+  as GHC+    ( PredType, Type(..), TyLit(..) )+import qualified GHC.Core.Type+  as GHC+    ( mkTyConApp, tcTypeKind )+import qualified GHC.Data.FastString+  as GHC+    ( fsLit )+import qualified GHC.Tc.Plugin+  as GHC+    ( tcLookupDataCon, tcLookupTyCon )+import qualified GHC.Tc.Types+  as GHC+    ( TcM, TcPlugin(..), TcPluginM+    , TcPluginSolver+#ifdef HAS_REWRITING+    , TcPluginRewriter+#else+    , getEvBindsTcPluginM+#endif+    , runTcPluginM, unsafeTcPluginTcM+    )+#ifdef HAS_REWRITING+import GHC.Tc.Types+    ( TcPluginSolveResult+    , TcPluginRewriteResult+    , RewriteEnv+    )+#endif+import qualified GHC.Tc.Types.Constraint+  as GHC+    ( Ct )+import qualified GHC.Tc.Types.Evidence+  as GHC+    ( EvBindsVar )+import qualified GHC.Types.Unique.FM+  as GHC+    ( UniqFM )+#if MIN_VERSION_ghc(9,1,0)+import GHC.Types.TyThing+  ( MonadThings(..) )+#else+import GHC.Driver.Types+  ( MonadThings(..) )+#endif++-- ghc-tcplugin-api+#ifndef HAS_REWRITING+import GHC.TcPlugin.API.Internal.Shim+  ( TcPluginSolveResult, TcPluginRewriteResult(..)+  , RewriteEnv+  , shimRewriter+  )+#endif++--------------------------------------------------------------------------------+-- Public types and functions.++-- | Stage of a type-checking plugin, used as a data kind.+data TcPluginStage+  = Init+  | Solve+  | Rewrite+  | Stop++-- | The @solve@ function of a type-checking plugin takes in Given and Wanted+-- constraints, and should return a 'GHC.Tc.Types.TcPluginSolveResult'+-- indicating which Wanted constraints it could solve, or whether any are+-- insoluble.+type TcPluginSolver+  =  [GHC.Ct] -- ^ Givens+  -> [GHC.Ct] -- ^ Wanteds+  -> TcPluginM Solve TcPluginSolveResult++-- | For rewriting type family applications, a type-checking plugin provides+-- a function of this type for each type family 'GHC.Core.TyCon.TyCon'.+--+-- The function is provided with the current set of Given constraints, together+-- with the arguments to the type family.+-- The type family application will always be fully saturated.+type TcPluginRewriter+  =  [GHC.Ct]     -- ^ Givens+  -> [GHC.Type]   -- ^ Type family arguments (saturated)+  -> TcPluginM Rewrite TcPluginRewriteResult++-- | A record containing all the stages necessary for the+-- operation of a type-checking plugin, as defined in this API.+--+-- __Note__: this is not the same record as GHC's built-in+-- 'GHC.Tc.Types.TcPlugin' record. Use 'mkTcPlugin' for the conversion.+--+-- To create a type-checking plugin, define something of this type+-- and then call 'mkTcPlugin' on the result.+-- This will return something that can be passed to 'GHC.Plugins.Plugin':+--+-- > plugin :: GHC.Plugins.Plugin+-- > plugin =+-- >   GHC.Plugins.defaultPlugin+-- >     { GHC.Plugins.tcPlugin =+-- >         \ args -> Just $+-- >            GHC.TcPlugin.API.mkTcPlugin ( myTcPlugin args )+-- >     }+-- >+-- > myTcPlugin :: [String] -> GHC.TcPlugin.API.TcPlugin+-- > myTcPlugin args = ...+data TcPlugin = forall s. TcPlugin+  { tcPluginInit :: TcPluginM Init s+      -- ^ Initialise plugin, when entering type-checker.++  , tcPluginSolve :: s -> TcPluginSolver+      -- ^ Solve some constraints.+      --+      -- This function will be invoked at two points in the constraint solving+      -- process: once to manipulate given constraints, and once to solve+      -- wanted constraints. In the first case (and only in the first case),+      -- no wanted constraints will be passed to the plugin.+      --+      -- The plugin can either return a contradiction,+      -- or specify that it has solved some constraints (with evidence),+      -- and possibly emit additional wanted constraints.+      --+      -- Use @ \\ _ _ _ -> pure $ TcPluginOK [] [] @ if your plugin+      -- does not provide this functionality.++  , tcPluginRewrite+      :: s -> GHC.UniqFM+#if MIN_VERSION_ghc(9,0,0)+                GHC.TyCon+#endif+                TcPluginRewriter+    -- ^ Rewrite saturated type family applications.+    --+    -- The plugin is expected to supply a mapping from type family names to+    -- rewriting functions. For each type family 'GHC.Core.TyCon.TyCon',+    -- the plugin should provide a function which takes in the given constraints+    -- and arguments of a saturated type family application, and return+    -- a possible rewriting.+    -- See 'TcPluginRewriter' for the expected shape of such a function.+    --+    -- Use @ const emptyUFM @ if your plugin does not provide this functionality.++  , tcPluginStop :: s -> TcPluginM Stop ()+   -- ^ Clean up after the plugin, when exiting the type-checker.+  }++-- | The monad used for a type-checker plugin, parametrised by+-- the 'TcPluginStage' of the plugin.+data family TcPluginM (s :: TcPluginStage) :: Type -> Type+newtype instance TcPluginM Init a =+  TcPluginInitM { tcPluginInitM :: GHC.TcPluginM a }+  deriving newtype ( Functor, Applicative, Monad )+#ifdef HAS_DERIVEDS+newtype instance TcPluginM Solve a =+  TcPluginSolveM { tcPluginSolveM :: BuiltinDefs -> GHC.EvBindsVar -> [GHC.Ct] -> GHC.TcPluginM a }+  deriving ( Functor, Applicative, Monad )+    via ( ReaderT BuiltinDefs ( ReaderT GHC.EvBindsVar ( ReaderT [GHC.Ct] GHC.TcPluginM ) ) )+#else+newtype instance TcPluginM Solve a =+  TcPluginSolveM { tcPluginSolveM :: BuiltinDefs -> GHC.EvBindsVar -> GHC.TcPluginM a }+  deriving ( Functor, Applicative, Monad )+    via ( ReaderT BuiltinDefs ( ReaderT GHC.EvBindsVar GHC.TcPluginM ) )+#endif+newtype instance TcPluginM Rewrite a =+  TcPluginRewriteM { tcPluginRewriteM :: BuiltinDefs -> RewriteEnv -> GHC.TcPluginM a }+  deriving ( Functor, Applicative, Monad )+    via ( ReaderT BuiltinDefs ( ReaderT RewriteEnv GHC.TcPluginM ) )+newtype instance TcPluginM Stop a =+  TcPluginStopM { tcPluginStopM :: GHC.TcPluginM a }+  deriving newtype ( Functor, Applicative, Monad )++-- | Ask for the evidence currently gathered by the type-checker.+--+-- Only available in the solver part of the type-checking plugin.+askEvBinds :: TcPluginM Solve GHC.EvBindsVar+askEvBinds = TcPluginSolveM+  \ _defs+    evBinds+#ifdef HAS_DERIVEDS+    _deriveds+#endif+  -> pure evBinds++-- | Ask for the Derived constraints that the solver was provided with.+--+-- Always returns the empty list on GHC 9.4 or above.+askDeriveds :: TcPluginM Solve [GHC.Ct]+askDeriveds =+#ifdef HAS_DERIVEDS+  TcPluginSolveM \ _defs _evBinds deriveds -> pure deriveds+#else+  pure []+#endif++-- | Ask for the current rewriting environment.+--+-- Only available in the rewriter part of the type-checking plugin.+askRewriteEnv :: TcPluginM Rewrite RewriteEnv+askRewriteEnv = TcPluginRewriteM ( \ _ rewriteEnv -> pure rewriteEnv )++-- | A 'MonadTcPlugin' is essentially a reader monad over GHC's 'GHC.Tc.TcM' monad.+--+-- This means we have both a @lift@ and an @unlift@ operation,+-- similar to @MonadUnliftIO@ or @MonadBaseControl@.+--+-- See for instance 'unsafeLiftThroughTcM', which is an example of function that+-- one would not be able to write using only a @lift@ operation.+--+-- Note that you must import the internal module in order to access the methods.+-- Please report a bug if you find yourself needing this functionality.+class ( Monad m, ( forall x y. Coercible x y => Coercible (m x) (m y) ) ) => MonadTcPlugin (m :: Type -> Type) where++  {-# MINIMAL liftTcPluginM, unsafeWithRunInTcM #-}++  -- N.B.: these methods are not re-exported from the main module.++  -- | Lift a computation from GHC's 'GHC.TcPluginM' monad.+  liftTcPluginM :: GHC.TcPluginM a -> m a++  -- | Lift a computation from the 'GHC.Tc.TcM' monad.+  unsafeLiftTcM :: GHC.TcM a -> m a+  unsafeLiftTcM = liftTcPluginM . GHC.unsafeTcPluginTcM++  -- | Unlift a computation from the 'GHC.Tc.TcM' monad.+  --+  -- If this type signature seems confusing, I recommend reading Alexis King's+  -- excellent blog post on @MonadBaseControl@:+  --+  -- <https://lexi-lambda.github.io/blog/2019/09/07/demystifying-monadbasecontrol/ Demystifying MonadBaseControl>+  unsafeWithRunInTcM :: ( ( forall a. m a -> GHC.TcM a ) -> GHC.TcM b ) -> m b++instance MonadTcPlugin ( TcPluginM Init ) where+  liftTcPluginM = TcPluginInitM+  unsafeWithRunInTcM runInTcM+    = unsafeLiftTcM $ runInTcM+#ifdef HAS_REWRITING+      ( GHC.runTcPluginM . tcPluginInitM )+#else+      ( ( `GHC.runTcPluginM` ( error "tcPluginInit: cannot access EvBindsVar" ) ) . tcPluginInitM )+#endif+instance MonadTcPlugin ( TcPluginM Solve ) where+  liftTcPluginM  = TcPluginSolveM+#ifdef HAS_DERIVEDS+                 . ( \ ma _defs _evBinds _deriveds -> ma )+#else+                 . ( \ ma _defs _evBinds -> ma )+#endif+  unsafeWithRunInTcM runInTcM+    = TcPluginSolveM+      \ builtinDefs+        evBinds+#ifdef HAS_DERIVEDS+        deriveds+#endif+      ->+        GHC.unsafeTcPluginTcM $ runInTcM+#ifdef HAS_REWRITING+  -- (no deriveds)+          ( GHC.runTcPluginM+          . ( \ f -> f builtinDefs evBinds )+          . tcPluginSolveM )+#else+          ( ( `GHC.runTcPluginM` evBinds )+          . ( \ f -> f builtinDefs evBinds deriveds )+          . tcPluginSolveM+          )+#endif+instance MonadTcPlugin ( TcPluginM Rewrite ) where+  liftTcPluginM = TcPluginRewriteM . ( \ ma _ _ -> ma )+  unsafeWithRunInTcM runInTcM+    = TcPluginRewriteM \ builtinDefs rewriteEnv ->+      GHC.unsafeTcPluginTcM $ runInTcM+#ifdef HAS_REWRITING+        ( GHC.runTcPluginM+#else+        ( ( `GHC.runTcPluginM` ( error "tcPluginRewrite: cannot access EvBindsVar" ) )+#endif+        . ( \ f -> f builtinDefs rewriteEnv )+        . tcPluginRewriteM )+instance MonadTcPlugin ( TcPluginM Stop ) where+  liftTcPluginM = TcPluginStopM+  unsafeWithRunInTcM runInTcM+    = unsafeLiftTcM $ runInTcM+#ifdef HAS_REWRITING+      ( GHC.runTcPluginM . tcPluginStopM )+#else+      ( ( `GHC.runTcPluginM` ( error "tcPluginStop: cannot access EvBindsVar" ) ) . tcPluginStopM )+#endif++-- | Take a function whose argument and result types are both within the 'GHC.Tc.TcM' monad,+-- and return a function that works within a type-checking plugin monad.+--+-- Please report a bug if you find yourself needing to use this function.+unsafeLiftThroughTcM :: MonadTcPlugin m => ( GHC.TcM a -> GHC.TcM b ) -> m a -> m b+unsafeLiftThroughTcM f ma = unsafeWithRunInTcM \ runInTcM -> f ( runInTcM ma )++-- | Use this function to create a type-checker plugin to pass to GHC.+mkTcPlugin+  :: TcPlugin     -- ^ type-checking plugin written with this library+  -> GHC.TcPlugin -- ^ type-checking plugin for GHC+mkTcPlugin ( TcPlugin+              { tcPluginInit = tcPluginInit :: TcPluginM Init userDefs+              , tcPluginSolve+              , tcPluginRewrite+              , tcPluginStop+              }+           ) =+  GHC.TcPlugin+    { GHC.tcPluginInit    = adaptUserInit    tcPluginInit+#ifdef HAS_REWRITING+    , GHC.tcPluginSolve   = adaptUserSolve   tcPluginSolve+    , GHC.tcPluginRewrite = adaptUserRewrite tcPluginRewrite+#else+    , GHC.tcPluginSolve   = adaptUserSolveAndRewrite+                              tcPluginSolve tcPluginRewrite+#endif+    , GHC.tcPluginStop    = adaptUserStop    tcPluginStop+    }+  where+    adaptUserInit :: TcPluginM Init userDefs -> GHC.TcPluginM ( TcPluginDefs userDefs )+    adaptUserInit userInit = do+      tcPluginBuiltinDefs <- initBuiltinDefs+      tcPluginUserDefs    <- tcPluginInitM userInit+      pure ( TcPluginDefs { tcPluginBuiltinDefs, tcPluginUserDefs })++#ifdef HAS_REWRITING+  -- (no deriveds)+    adaptUserSolve :: ( userDefs -> TcPluginSolver )+                   -> TcPluginDefs userDefs+                   -> GHC.TcPluginSolver+    adaptUserSolve userSolve ( TcPluginDefs { tcPluginUserDefs, tcPluginBuiltinDefs } )+      = \ evBindsVar givens wanteds -> do+        tcPluginSolveM ( userSolve tcPluginUserDefs givens wanteds )+          tcPluginBuiltinDefs evBindsVar+    adaptUserRewrite :: ( userDefs -> GHC.UniqFM GHC.TyCon TcPluginRewriter )+                     -> TcPluginDefs userDefs -> GHC.UniqFM GHC.TyCon GHC.TcPluginRewriter+    adaptUserRewrite userRewrite ( TcPluginDefs { tcPluginUserDefs, tcPluginBuiltinDefs })+      = fmap+          ( \ userRewriter rewriteEnv givens tys ->+            tcPluginRewriteM ( userRewriter givens tys ) tcPluginBuiltinDefs rewriteEnv+          )+          ( userRewrite tcPluginUserDefs )+#else+    adaptUserSolveAndRewrite+      :: ( userDefs -> TcPluginSolver )+      -> ( userDefs -> GHC.UniqFM+#if MIN_VERSION_ghc(9,0,0)+                         GHC.TyCon+#endif+                         TcPluginRewriter+         )+      -> TcPluginDefs userDefs+      -> GHC.TcPluginSolver+    adaptUserSolveAndRewrite userSolve userRewrite ( TcPluginDefs { tcPluginUserDefs, tcPluginBuiltinDefs } )+      = \ givens deriveds wanteds -> do+        evBindsVar <- GHC.getEvBindsTcPluginM+        shimRewriter+          givens deriveds wanteds+          ( fmap+              ( \ userRewriter rewriteEnv gs tys ->+                tcPluginRewriteM ( userRewriter gs tys )+                  tcPluginBuiltinDefs rewriteEnv+              )+              ( userRewrite tcPluginUserDefs )+          )+          ( \ gs ds ws ->+            tcPluginSolveM ( userSolve tcPluginUserDefs gs ws )+              tcPluginBuiltinDefs evBindsVar ds+          )+#endif++    adaptUserStop :: ( userDefs -> TcPluginM Stop () ) -> TcPluginDefs userDefs -> GHC.TcPluginM ()+    adaptUserStop userStop ( TcPluginDefs { tcPluginUserDefs } ) =+      tcPluginStopM $ userStop tcPluginUserDefs++-- | Monads for type-checking plugins which are able to emit new constraints+-- and throw errors.+--+-- These operations are supported by the monads that 'tcPluginSolve'+-- and 'tcPluginRewrite' use; it is not possible to emit work or+-- throw type errors in 'tcPluginInit' or 'tcPluginStop'.+--+-- See 'mkTcPluginErrorTy' and 'GHC.TcPlugin.API.emitWork' for functions+-- which require this typeclass.+class MonadTcPlugin m => MonadTcPluginWork m where+  {-# MINIMAL #-} -- to avoid the methods appearing in the haddocks+  askBuiltins :: m BuiltinDefs+  askBuiltins = error "askBuiltins: no default implementation"+instance MonadTcPluginWork ( TcPluginM Solve ) where+  askBuiltins = TcPluginSolveM+    \ builtinDefs+      _evBinds+#ifdef HAS_DERIVEDS+      _deriveds+#endif+    -> pure builtinDefs+instance MonadTcPluginWork ( TcPluginM Rewrite ) where+  askBuiltins = TcPluginRewriteM \ builtinDefs _evBinds -> pure builtinDefs++instance TypeError ( 'Text "Cannot emit new work in 'tcPluginInit'." )+      => MonadTcPluginWork ( TcPluginM Init ) where+  askBuiltins = error "Cannot emit new work in 'tcPluginInit'."+instance TypeError ( 'Text "Cannot emit new work in 'tcPluginStop'." )+      => MonadTcPluginWork ( TcPluginM Stop ) where+  askBuiltins = error "Cannot emit new work in 'tcPluginStop'."++-- | Use this type like 'GHC.TypeLits.ErrorMessage' to write an error message.+-- This error message can then be thrown at the type-level by the plugin,+-- by emitting a wanted constraint whose predicate is obtained from 'mkTcPluginErrorTy'.+--+-- A 'GHC.Tc.Types.Constraint.CtLoc' will still need to be provided in order to inform GHC of the+-- origin of the error (e.g.: which part of the source code should be+-- highlighted?). See 'GHC.TcPlugin.API.setCtLocM'.+data TcPluginErrorMessage+  = Txt !String+  -- ^ Show the text as is.+  | PrintType !GHC.Type+  -- ^ Pretty print the given type.+  | (:|:) !TcPluginErrorMessage !TcPluginErrorMessage+  -- ^ Put two messages side by side.+  | (:-:) !TcPluginErrorMessage !TcPluginErrorMessage+  -- ^ Stack two messages vertically.+infixl 5 :|:+infixl 6 :-:++-- | Create an error type with the desired error message.+--+-- The result can be paired with a 'GHC.Tc.Types.Constraint.CtLoc' in order to throw a type error,+-- for instance by using 'GHC.TcPlugin.API.newWanted'.+mkTcPluginErrorTy :: MonadTcPluginWork m => TcPluginErrorMessage -> m GHC.PredType+mkTcPluginErrorTy msg = do+  builtinDefs@( BuiltinDefs { typeErrorTyCon } ) <- askBuiltins+  let+    errorMsgTy :: GHC.PredType+    errorMsgTy = interpretErrorMessage builtinDefs msg+  pure $ GHC.mkTyConApp typeErrorTyCon [ GHC.constraintKind, errorMsgTy ]++instance ( Monad (TcPluginM s), MonadTcPlugin (TcPluginM s) )+      => MonadThings (TcPluginM s) where+  lookupThing = unsafeLiftTcM . lookupThing++--------------------------------------------------------------------------------+-- Private types and functions.+-- Not exposed at all, even from the internal module.++data BuiltinDefs =+  BuiltinDefs+    { typeErrorTyCon :: !GHC.TyCon+    , textTyCon      :: !GHC.TyCon+    , showTypeTyCon  :: !GHC.TyCon+    , concatTyCon    :: !GHC.TyCon+    , vcatTyCon      :: !GHC.TyCon+    }++data TcPluginDefs s+  = TcPluginDefs+  { tcPluginBuiltinDefs :: !BuiltinDefs+  , tcPluginUserDefs    :: !s+  }++initBuiltinDefs :: GHC.TcPluginM BuiltinDefs+initBuiltinDefs = do+  typeErrorTyCon  <-                        GHC.tcLookupTyCon   GHC.TypeLits.errorMessageTypeErrorFamName+  textTyCon       <- GHC.promoteDataCon <$> GHC.tcLookupDataCon GHC.TypeLits.typeErrorTextDataConName+  showTypeTyCon   <- GHC.promoteDataCon <$> GHC.tcLookupDataCon GHC.TypeLits.typeErrorShowTypeDataConName+  concatTyCon     <- GHC.promoteDataCon <$> GHC.tcLookupDataCon GHC.TypeLits.typeErrorAppendDataConName+  vcatTyCon       <- GHC.promoteDataCon <$> GHC.tcLookupDataCon GHC.TypeLits.typeErrorVAppendDataConName+  pure ( BuiltinDefs { .. } )++interpretErrorMessage :: BuiltinDefs -> TcPluginErrorMessage -> GHC.PredType+interpretErrorMessage ( BuiltinDefs { .. } ) = go+  where+    go :: TcPluginErrorMessage -> GHC.PredType+    go ( Txt str ) =+      GHC.mkTyConApp textTyCon [ GHC.LitTy . GHC.StrTyLit . GHC.fsLit $ str ]+    go ( PrintType ty ) =+      GHC.mkTyConApp showTypeTyCon [ GHC.tcTypeKind ty, ty ]+        -- The kind gets ignored by GHC when printing the error message (see GHC.Core.Type.pprUserTypeErrorTy).+        -- However, including the wrong kind can lead to ASSERT failures, so we compute the kind and pass it.+    go ( msg1 :|: msg2 ) =+      GHC.mkTyConApp concatTyCon [ go msg1, go msg2 ]+    go ( msg1 :-: msg2 ) =+      GHC.mkTyConApp vcatTyCon [ go msg1, go msg2 ]

@@ -1,962 +1,962 @@-{-# LANGUAGE BangPatterns    #-}
-{-# LANGUAGE BlockArguments  #-}
-{-# LANGUAGE CPP             #-}
-{-# LANGUAGE DerivingVia     #-}
-{-# LANGUAGE LambdaCase      #-}
-{-# LANGUAGE NamedFieldPuns  #-}
-{-# LANGUAGE PatternSynonyms #-}
-{-# LANGUAGE TupleSections   #-}
-{-# LANGUAGE ViewPatterns    #-}
-
-{-|
-Module: GHC.TcPlugin.API.Internal.Shim
-
-This module defines a compatibility shim which allows
-the library to support a limited form of type-family rewriting
-in typechecking plugins on GHC 9.0 and 9.2.
--}
-
-module GHC.TcPlugin.API.Internal.Shim
-  ( Reduction(..), mkReduction
-  , TcPluginSolveResult(TcPluginContradiction, TcPluginOk, ..), TcPluginRewriteResult(..)
-  , RewriteEnv(..)
-  , shimRewriter
-  )
-  where
-
--- base
-import Prelude
-  hiding ( Floating(cos), iterate )
-import Control.Monad
-  ( forM, unless, when )
-import Data.Foldable
-  ( traverse_
-#if !MIN_VERSION_ghc(9,2,0)
-  , foldlM
-#endif
-  )
-#if MIN_VERSION_ghc(9,2,0)
-import Data.List.NonEmpty
-  ( NonEmpty((:|)) )
-#endif
-import Data.Maybe
-  ( fromMaybe )
-
--- transformers
-import Control.Monad.Trans.Reader
-  ( ReaderT(..) )
-import Control.Monad.Trans.State.Strict
-  ( StateT(..) )
-
--- ghc
-import GHC.Core.Coercion
-  ( coercionRole
-  , mkReflCo, mkSymCo
-  , mkAppCos, mkNomReflCo, mkSubCo
-  , mkTyConAppCo, tyConRolesX
-  , tyConRolesRepresentational
-  )
-import GHC.Core.Predicate
-  ( EqRel(..), eqRelRole )
-import GHC.Core.TyCo.Rep
-  ( Type(..), Kind, Coercion(..), MCoercion(..), TyCoBinder(..)
-  , isNamedBinder, mkTyVarTy
-  )
-import GHC.Core.TyCon
-  ( TyCon(..), TyConBinder, TyConBndrVis(..)
-#if MIN_VERSION_ghc(9,2,0)
-  , isForgetfulSynTyCon
-#endif
-  , isFamFreeTyCon, isTypeSynonymTyCon
-  , isTypeFamilyTyCon
-  , tyConBinders, tyConResKind
-  , tyConArity
-  )
-import GHC.Core.Type
-  ( TyVar
-  , tcView , mkTyConApp
-#if MIN_VERSION_ghc(9,0,0)
-  , mkScaled, tymult
-#endif
-  , coreView, tyVarKind
-  )
-#if MIN_VERSION_ghc(9,2,0)
-import GHC.Data.Maybe
-  ( firstJustsM )
-#endif
-import GHC.Tc.Plugin
-  ( newWanted, newDerived )
-import GHC.Tc.Solver.Monad
-  ( TcS
-  , zonkCo, zonkTcType
-  , isFilledMetaTyVar_maybe
-  , getInertEqs
-  , checkReductionDepth
-  , matchFam
-  , runTcPluginTcS, runTcSWithEvBinds
-  , traceTcS
-  , setWantedEvTerm
-#if MIN_VERSION_ghc(9,2,0)
-  , lookupFamAppCache, lookupFamAppInert, extendFamAppCache
-  , pattern EqualCtList
-#else
-  , lookupFlatCache, extendFlatCache
-#endif
-  )
-import GHC.Tc.Types
-  ( TcPluginM
-  , unsafeTcPluginTcM, getEvBindsTcPluginM
-  )
-import qualified GHC.Tc.Types as GHC
-  ( TcPluginResult(..) )
-import GHC.Tc.Types.Constraint
-  ( Ct(..), CtEvidence(..)
-  , CtLoc, CtFlavour(..), CtFlavourRole, ShadowInfo(..)
-#if MIN_VERSION_ghc(9,2,0)
-  , CanEqLHS(..)
-#endif
-  , ctLoc, ctFlavour, ctEvidence, ctEqRel, ctEvPred
-  , ctEvExpr, ctEvCoercion, ctEvFlavour
-  , bumpCtLocDepth, eqCanRewriteFR, mkNonCanonical
-  )
-import GHC.Tc.Types.Evidence
-  ( EvTerm(..), Role(..)
-  , evCast, mkTcTransCo , mkTcTyConAppCo
-  )
-import GHC.Tc.Utils.TcType
-  ( TcTyCoVarSet
-#if MIN_VERSION_ghc(9,2,0)
-  , tcSplitForAllTyVarBinders
-#else
-  , tcSplitForAllVarBndrs
-#endif
-  , tcSplitTyConApp_maybe
-  , tcTypeKind
-  , tyCoVarsOfType
-  )
-import GHC.Types.Unique.FM
-  ( UniqFM, lookupUFM, isNullUFM )
-import GHC.Types.Var
-  ( TcTyVar, VarBndr(..)
-#if !MIN_VERSION_ghc(9,2,0)
-  , TyVarBinder
-#endif
-  , updateTyVarKindM
-  )
-import GHC.Types.Var.Env
-  ( lookupDVarEnv )
-import GHC.Types.Var.Set
-  ( emptyVarSet )
-import GHC.Utils.Misc
-  ( dropList )
-import GHC.Utils.Monad
-  ( zipWith3M )
-import GHC.Utils.Outputable
-  ( Outputable(..), SDoc, empty )
-
--- ghc-tcplugin-api
-import GHC.TcPlugin.API.Internal.Shim.Reduction
-
---------------------------------------------------------------------------------
-
--- | The type-family rewriting environment.
-data RewriteEnv
-  = FE { fe_loc     :: !CtLoc
-       , fe_flavour :: !CtFlavour
-       , fe_eq_rel  :: !EqRel
-       }
-
--- | Result of running a solver plugin.
-data TcPluginSolveResult
-  = TcPluginSolveResult
-  { -- | Insoluble constraints found by the plugin.
-    --
-    -- These constraints will be added to the inert set,
-    -- and reported as insoluble to the user.
-    tcPluginInsolubleCts :: [Ct]
-    -- | Solved constraints, together with their evidence.
-    --
-    -- These are removed from the inert set, and the
-    -- evidence for them is recorded.
-  , tcPluginSolvedCts :: [(EvTerm, Ct)]
-    -- | New constraints that the plugin wishes to emit.
-    --
-    -- These will be added to the work list.
-  , tcPluginNewCts :: [Ct]
-  }
-
--- | The plugin found a contradiction.
--- The returned constraints are removed from the inert set,
--- and recorded as insoluble.
---
--- The returned list of constraints should never be empty.
-pattern TcPluginContradiction :: [Ct] -> TcPluginSolveResult
-pattern TcPluginContradiction insols
-  = TcPluginSolveResult
-  { tcPluginInsolubleCts = insols
-  , tcPluginSolvedCts    = []
-  , tcPluginNewCts       = [] }
-
--- | The plugin has not found any contradictions,
---
--- The first field is for constraints that were solved.
--- The second field contains new work, that should be processed by
--- the constraint solver.
-pattern TcPluginOk :: [(EvTerm, Ct)] -> [Ct] -> TcPluginSolveResult
-pattern TcPluginOk solved new
-  = TcPluginSolveResult
-  { tcPluginInsolubleCts = []
-  , tcPluginSolvedCts    = solved
-  , tcPluginNewCts       = new }
-
--- The 'TcPluginSolveResult' datatype changed in GHC 9.4,
--- allowing users to return solved and new constraints even in case of
--- a contradiction.
---
--- This function simply drops the solved and new constraints on older versions,
--- although it does at least still bind the evidence in case of solved Wanteds.
-adaptSolveResult :: Bool -> TcPluginSolveResult -> TcPluginM GHC.TcPluginResult
-adaptSolveResult doingGivens
-  ( TcPluginSolveResult
-    { tcPluginInsolubleCts = insols
-    , tcPluginSolvedCts    = solved
-    , tcPluginNewCts       = new
-    }
-  )
-    | null insols
-    = pure $ GHC.TcPluginOk solved new
-    | null solved && null new
-    = pure $ GHC.TcPluginContradiction insols
-    | otherwise
-    = do
-      evBinds <- getEvBindsTcPluginM
-      unsafeTcPluginTcM . runTcSWithEvBinds evBinds $ do
-        unless doingGivens $ traverse_ ( uncurry setEv ) solved
-        --updInertCans (removeInertCts $ fmap snd solved) -- These don't do anything, as the inert set and work list
-        --emitWork new                                    -- are confined to this run of the plugin.
-      pure $ GHC.TcPluginContradiction insols
-  where
-    setEv :: EvTerm -> Ct -> TcS ()
-    setEv ev ( ctEvidence -> CtWanted { ctev_dest = dest } )
-      = setWantedEvTerm dest ev
-    setEv _ _
-      = pure ()
-
-data TcPluginRewriteResult
-  =
-  -- | The plugin does not rewrite the type family application.
-    TcPluginNoRewrite
-
-  -- | The plugin rewrites the type family application
-  -- providing a rewriting together with evidence.
-  --
-  -- The plugin can also emit additional wanted constraints.
-  | TcPluginRewriteTo
-    { tcPluginReduction :: !Reduction
-    , tcRewriterWanteds :: [Ct]
-    }
-
-type Rewriter = RewriteEnv -> [Ct] -> [Type] -> TcPluginM TcPluginRewriteResult
-
-type Rewriters =
-  UniqFM
-#if MIN_VERSION_ghc(9,0,0)
-    TyCon
-#endif
-    Rewriter
-
--- | Emulate type-family rewriting functionality in a constraint solving plugin,
--- by traversing through all the constraints and rewriting any type-family applications
--- inside them.
-shimRewriter :: [Ct] -> [Ct] -> [Ct]
-             -> Rewriters
-             -> ( [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginSolveResult )
-             -> TcPluginM GHC.TcPluginResult
-shimRewriter givens deriveds wanteds rws solver
-  | isNullUFM rws
-  = adaptSolveResult (null wanteds) =<< solver givens deriveds wanteds
-  | otherwise
-  = do
-    TcPluginSolveResult
-      { tcPluginInsolubleCts = contras
-      , tcPluginSolvedCts    = solved
-      , tcPluginNewCts       = new
-      } <- solver givens deriveds wanteds
-    ( rewrittenDeriveds, solvedDeriveds, newCts1 ) <- traverseCts ( reduceCt rws givens ) deriveds
-    ( rewrittenWanteds , solvedWanteds , newCts2 ) <- traverseCts ( reduceCt rws givens ) wanteds
-    adaptSolveResult (null wanteds) $
-      TcPluginSolveResult
-        { tcPluginInsolubleCts = contras
-        , tcPluginSolvedCts    = solved ++ solvedDeriveds ++ solvedWanteds
-        , tcPluginNewCts       = new ++ newCts1 ++ rewrittenDeriveds ++ newCts2 ++ rewrittenWanteds
-        }
-
-reduceCt :: Rewriters
-         -> [Ct]
-         -> Ct
-         -> TcPluginM ( Maybe ( Ct, (EvTerm, Ct) ), [Ct] )
-reduceCt rws givens ct = do
-  let
-    predTy :: Type
-    predTy = ctEvPred ( ctEvidence ct )
-    rwEnv :: RewriteEnv
-    rwEnv = FE ( ctLoc ct ) ( ctFlavour ct ) ( ctEqRel ct )
-    shimRewriteEnv :: ShimRewriteEnv
-    shimRewriteEnv = ShimRewriteEnv rws rwEnv givens
-  ( res, newCts ) <- runRewritePluginM shimRewriteEnv ( rewrite_one predTy )
-  case res of
-    Nothing -> pure ( Nothing, newCts )
-    Just ( Reduction co predTy' ) -> do
-      ctEv' <- case ctFlavour ct of
-        Given     -> error "ghc-tcplugin-api: unexpected Given in reduceCt"
-        Wanted {} -> newWanted  ( ctLoc ct ) predTy'
-        Derived   -> newDerived ( ctLoc ct ) predTy'
-      let
-        role :: Role
-        role = coercionRole co
-        cast_co :: Coercion
-        cast_co = mkSymCo $ case role of
-          Nominal -> mkSubCo co
-          _       -> co
-      pure ( Just
-              ( mkNonCanonical ctEv'
-              , ( evCast ( ctEvExpr ctEv' ) cast_co, ct )
-              )
-           , newCts
-           )
-
-traverseCts :: Monad m
-            => ( a -> m ( Maybe (b, c), [d] ) )
-            -> [a]
-            -> m ( [b], [c], [d] )
-traverseCts _ [] = pure ( [], [], [] )
-traverseCts f (a : as) = do
-  ( mb_bc, ds ) <- f a
-  ( bs, cs, dss ) <- traverseCts f as
-  case mb_bc of
-    Nothing    -> pure ( bs, cs, ds ++ dss )
-    Just (b,c) -> pure ( b : bs, c : cs, ds ++ dss )
-
---------------------------------------------------------------------------------
--- The following is (mostly) copied from GHC 9.4's GHC.Tc.Solver.Rewrite module.
-
-rewrite_one :: Type -> RewriteM Reduction
-rewrite_one ty
-  | Just ty' <- rewriterView ty  -- See Note [Rewriting synonyms]
-  = rewrite_one ty'
-
-rewrite_one xi@(LitTy {})
-  = do { role <- getRole
-       ; return $ mkReflRedn role xi }
-
-rewrite_one (TyVarTy tv)
-  = rewriteTyVar tv
-
-rewrite_one (AppTy ty1 ty2)
-  = rewrite_app_tys ty1 [ty2]
-
-rewrite_one (TyConApp tc tys)
-  | isTypeFamilyTyCon tc
-  = rewrite_fam_app tc tys
-
-  | otherwise
-  = rewrite_ty_con_app tc tys
-
-rewrite_one
-  (FunTy
-#if MIN_VERSION_ghc(8,10,0)
-    vis
-#endif
-#if MIN_VERSION_ghc(9,0,0)
-    mult
-#endif
-    ty1
-    ty2
-  )
-  = do { arg_redn <- rewrite_one ty1
-       ; res_redn <- rewrite_one ty2
-#if MIN_VERSION_ghc(9,0,0)
-       ; w_redn <- setEqRel NomEq $ rewrite_one mult
-#endif
-       ; role <- getRole
-       ; return $
-           mkFunRedn
-             role
-#if MIN_VERSION_ghc(8,10,0)
-             vis
-#endif
-#if MIN_VERSION_ghc(9,0,0)
-             w_redn
-#endif
-             arg_redn
-             res_redn
-        }
-
-rewrite_one ty@(ForAllTy {})
-  = do { let (bndrs, rho) = tcSplitForAllTyVarBinders ty
-       ; redn <- rewrite_one rho
-       ; return $ mkHomoForAllRedn bndrs redn }
-
-rewrite_one (CastTy ty g)
-  = do { redn <- rewrite_one ty
-       ; g'   <- rewrite_co g
-       ; role <- getRole
-       ; return $ mkCastRedn1 role ty g' redn }
-
-rewrite_one (CoercionTy co)
-  = do { co' <- rewrite_co co
-       ; role <- getRole
-       ; return $ mkReflCoRedn role co' }
-
-rewrite_reduction :: Reduction -> RewriteM Reduction
-rewrite_reduction (Reduction co xi) = do
-  redn <- bumpDepth $ rewrite_one xi
-  pure $ co `mkTransRedn` redn
-
-rewrite_app_tys :: Type -> [Type] -> RewriteM Reduction
-rewrite_app_tys (AppTy ty1 ty2) tys = rewrite_app_tys ty1 (ty2:tys)
-rewrite_app_tys fun_ty arg_tys
-  = do { redn <- rewrite_one fun_ty
-       ; rewrite_app_ty_args redn arg_tys }
-
-rewrite_app_ty_args :: Reduction -> [Type] -> RewriteM Reduction
-rewrite_app_ty_args redn []
-  = return redn
-rewrite_app_ty_args fun_redn@(Reduction fun_co fun_xi) arg_tys
-  = do { het_redn <- case tcSplitTyConApp_maybe fun_xi of
-           Just (tc, xis) ->
-             do { let tc_roles  = tyConRolesRepresentational tc
-                      arg_roles = dropList xis tc_roles
-                ; ArgsReductions (Reductions arg_cos arg_xis) kind_co
-                    <- rewrite_vector (tcTypeKind fun_xi) arg_roles arg_tys
-
-                ; eq_rel <- getEqRel
-                ; let app_xi = mkTyConApp tc (xis ++ arg_xis)
-                      app_co = case eq_rel of
-                        NomEq  -> mkAppCos fun_co arg_cos
-                        ReprEq -> mkAppCos fun_co (map mkNomReflCo arg_tys)
-                                  `mkTcTransCo`
-                                  mkTcTyConAppCo Representational tc
-                                    (zipWith mkReflCo tc_roles xis ++ arg_cos)
-
-                ; return $
-                    mkHetReduction
-                      (mkReduction app_co app_xi )
-                      kind_co }
-           Nothing ->
-             do { ArgsReductions redns kind_co
-                    <- rewrite_vector (tcTypeKind fun_xi) (repeat Nominal) arg_tys
-                ; return $ mkHetReduction (mkAppRedns fun_redn redns) kind_co }
-
-       ; role <- getRole
-       ; return (homogeniseHetRedn role het_redn) }
-
-{-# INLINE rewrite_args_tc #-}
-rewrite_args_tc :: TyCon -> Maybe [Role] -> [Type] -> RewriteM ArgsReductions
-rewrite_args_tc tc = rewrite_args all_bndrs any_named_bndrs inner_ki emptyVarSet
-  -- NB: TyCon kinds are always closed
-  where
-  -- There are many bang patterns in here. It's been observed that they
-  -- greatly improve performance of an optimized build.
-  -- The T9872 test cases are good witnesses of this fact.
-
-    (bndrs, named)
-      = ty_con_binders_ty_binders' (tyConBinders tc)
-    -- it's possible that the result kind has arrows (for, e.g., a type family)
-    -- so we must split it
-    (inner_bndrs, inner_ki, inner_named) = split_pi_tys' (tyConResKind tc)
-    !all_bndrs                           = bndrs `chkAppend` inner_bndrs
-    !any_named_bndrs                     = named || inner_named
-    -- NB: Those bangs there drop allocations in T9872{a,c,d} by 8%.
-
-rewrite_fam_app :: TyCon -> [Type] -> RewriteM Reduction
-rewrite_fam_app tc tys = do
-  let (tys1, tys_rest) = splitAt (tyConArity tc) tys
-  redn <- rewrite_exact_fam_app tc tys1
-  rewrite_app_ty_args redn tys_rest
-
-rewrite_exact_fam_app :: TyCon -> [Type] -> RewriteM Reduction
-rewrite_exact_fam_app tc tys = do
-  checkStackDepth $ mkTyConApp tc tys
-  rws <- getRewriters
-  let
-    mbRewriter :: Maybe Rewriter
-    mbRewriter = lookupUFM rws tc
-  result1 <- try_to_reduce tc tys mbRewriter
-  case result1 of
-    Just redn -> finish False redn
-    _ -> do
-      eq_rel <- getEqRel
-      ArgsReductions (Reductions cos xis) kind_co <-
-        if eq_rel == NomEq
-        then rewrite_args_tc tc Nothing tys
-        else setEqRel NomEq $
-             rewrite_args_tc tc Nothing tys
-      let
-        role    = eqRelRole eq_rel
-        args_co = mkTyConAppCo role tc cos
-        homogenise :: Reduction -> Reduction
-        homogenise redn
-          = homogeniseHetRedn role
-          $ mkHetReduction
-              (args_co `mkTransRedn` redn)
-              kind_co
-        give_up :: Reduction
-        give_up = homogenise $ mkReflRedn role (mkTyConApp tc xis)
-
-      result2 <- liftTcS $ lookupFamAppInert tc xis
-      flavour <- getFlavour
-      case result2 of
-        Just (co, xi, fr@(_, inert_eq_rel))
-          | fr `eqCanRewriteFR` (flavour, eq_rel)
-          , let
-              redn :: Reduction
-              redn = Reduction (mkSymCo co) xi -- inerts use a different orientation in GHC 9.0 and 9.2
-          -> finish True (homogenise $ downgradeRedn role' inert_role redn)
-          where
-            inert_role      = eqRelRole inert_eq_rel
-            role'           = eqRelRole eq_rel
-        _ -> do
-          result3 <- try_to_reduce tc xis mbRewriter
-          case result3 of
-            Just redn -> finish True (homogenise redn)
-            _         -> return give_up
-  where
-    finish :: Bool -> Reduction -> RewriteM Reduction
-    finish use_cache (Reduction co xi) = do
-      Reduction fully_co fully <- bumpDepth $ rewrite_one xi
-      let final_redn@(Reduction final_co final_xi) = Reduction (fully_co `mkTcTransCo` co) fully
-      eq_rel <- getEqRel
-      flavour <- getFlavour
-      when (use_cache && eq_rel == NomEq && flavour /= Derived) $
-        liftTcS $
-          extendFamAppCache tc tys
-            ( mkSymCo final_co, final_xi ) -- different orientation in GHC 9.0 and 9.2
-#if !MIN_VERSION_ghc(9,2,0)
-            flavour
-#endif
-      return final_redn
-    {-# INLINE finish #-}
-
--- Returned coercion is output ~r input, where r is the role in the RewriteM monad
--- See Note [How to normalise a family application]
-try_to_reduce :: TyCon -> [Type] -> Maybe Rewriter
-              -> RewriteM (Maybe Reduction)
-try_to_reduce tc tys mb_rewriter = do
-  result <-
-    firstJustsM
-      [ runTcPluginRewriter mb_rewriter tys
-      , liftTcS $ mkRed <$> lookupFamAppCache tc tys
-      , liftTcS $ mkRed <$> matchFam tc tys ]
-  forM result downgrade
-    where
-      mkRed :: Maybe (Coercion, Type) -> Maybe Reduction
-      mkRed = fmap $ uncurry Reduction
-      downgrade :: Reduction -> RewriteM Reduction
-      downgrade redn@(Reduction co xi) = do
-        eq_rel <- getEqRel
-        case eq_rel of
-          NomEq  -> return redn
-          ReprEq -> return $ Reduction (mkSubCo co) xi
-
-runTcPluginRewriter :: Maybe Rewriter
-                    -> [Type]
-                    -> RewriteM (Maybe Reduction)
-runTcPluginRewriter mbRewriter tys =
-  case mbRewriter of
-    Nothing -> return Nothing
-    Just rewriter -> do
-      traceRewriteM "runTcPluginRewriter { " empty
-      res <- runRewriter rewriter
-      traceRewriteM "runTcPluginRewriter }" ( ppr res )
-      pure res
-  where
-  runRewriter :: Rewriter -> RewriteM (Maybe Reduction)
-  runRewriter rewriter = do
-    rewriteResult <- RewriteM \ env s -> do
-      res <- runTcPluginTcS ( rewriter ( rewriteEnv env ) ( rewriteGivens env ) tys )
-      pure ( res, s )
-    case rewriteResult of
-      TcPluginRewriteTo
-        { tcPluginReduction = redn
-        , tcRewriterWanteds = wanteds
-        } -> addRewriting ( Just redn ) wanteds
-      TcPluginNoRewrite { }
-          -> addRewriting Nothing []
-
-rewrite_ty_con_app :: TyCon -> [Type] -> RewriteM Reduction
-rewrite_ty_con_app tc tys
-  = do { role <- getRole
-       ; let m_roles | Nominal <- role = Nothing
-                     | otherwise       = Just $ tyConRolesX role tc
-       ; ArgsReductions redns kind_co <- rewrite_args_tc tc m_roles tys
-       ; let tyconapp_redn
-                = mkHetReduction
-                    (mkTyConAppRedn role tc redns)
-                    kind_co
-       ; return $ homogeniseHetRedn role tyconapp_redn }
-
-rewrite_co :: Coercion -> RewriteM Coercion
-rewrite_co co = liftTcS $ zonkCo co
-
-rewriterView :: Type -> Maybe Type
-rewriterView ty@(TyConApp tc _)
-  | ( isTypeSynonymTyCon tc && not (isFamFreeTyCon tc) )
-#if MIN_VERSION_ghc(9,2,0)
-  || isForgetfulSynTyCon tc
-#endif
-  = tcView ty
-rewriterView _other = Nothing
-
-rewriteTyVar :: TyVar -> RewriteM Reduction
-rewriteTyVar tv = do
-  mb_yes <- rewrite_tyvar1 tv
-  case mb_yes of
-    RTRFollowed redn -> rewrite_reduction redn
-    RTRNotFollowed -> do
-      tv' <- liftTcS $ updateTyVarKindM zonkTcType tv
-      role <- getRole
-      let ty' = mkTyVarTy tv'
-      pure $ mkReflRedn role ty'
-
-data RewriteTvResult
-  = RTRNotFollowed
-  | RTRFollowed !Reduction
-
-rewrite_tyvar1 :: TcTyVar -> RewriteM RewriteTvResult
-rewrite_tyvar1 tv = do
-  mb_ty <- liftTcS $ isFilledMetaTyVar_maybe tv
-  case mb_ty of
-    Just ty -> do
-      role <- getRole
-      return $ RTRFollowed $ mkReflRedn role ty
-    Nothing -> do
-      fr <- getFlavourRole
-      rewrite_tyvar2 tv fr
-
-rewrite_tyvar2 :: TcTyVar -> CtFlavourRole -> RewriteM RewriteTvResult
-rewrite_tyvar2 tv fr@(_, eq_rel) = do
-  ieqs <- liftTcS $ getInertEqs
-  case lookupDVarEnv ieqs tv of
-#if MIN_VERSION_ghc(9,2,0)
-    Just (EqualCtList (ct :| _))
-      | CEqCan { cc_ev = ctev, cc_lhs = TyVarLHS {}
-               , cc_rhs = rhs_ty, cc_eq_rel = ct_eq_rel } <- ct
-#else
-    Just (ct : _)
-      | CTyEqCan { cc_ev = ctev
-                 , cc_rhs = rhs_ty, cc_eq_rel = ct_eq_rel } <- ct
-#endif
-      , let ct_fr = (ctEvFlavour ctev, ct_eq_rel)
-      , ct_fr `eqCanRewriteFR` fr
-      -> do
-          let rewriting_co1 = ctEvCoercion ctev
-              rewriting_co  = case (ct_eq_rel, eq_rel) of
-                (ReprEq, _rel)  -> rewriting_co1
-                (NomEq, NomEq)  -> rewriting_co1
-                (NomEq, ReprEq) -> mkSubCo rewriting_co1
-          return $ RTRFollowed $ mkReduction rewriting_co rhs_ty 
-    _other -> return RTRNotFollowed
-
-rewrite_vector :: Kind
-               -> [Role]
-               -> [Type]
-               -> RewriteM ArgsReductions
-rewrite_vector ki roles tys
-  = do { eq_rel <- getEqRel
-       ; let mb_roles = case eq_rel of { NomEq -> Nothing; ReprEq -> Just roles }
-       ; rewrite_args bndrs any_named_bndrs inner_ki fvs mb_roles tys
-       }
-  where
-    (bndrs, inner_ki, any_named_bndrs) = split_pi_tys' ki
-    fvs                                = tyCoVarsOfType ki
-{-# INLINE rewrite_vector #-}
-
-split_pi_tys' :: Type -> ([TyCoBinder], Type, Bool)
-split_pi_tys' ty = split ty ty
-  where
-  split _ (ForAllTy b res) =
-    let !(bs, ty', _) = split res res
-    in  (Named b : bs, ty', True)
-  split _
-    (FunTy
-#if MIN_VERSION_ghc(8,10,0)
-      af
-#endif
-#if MIN_VERSION_ghc(9,0,0)
-      w
-#endif
-      arg
-      res
-    ) =
-    let !(bs, ty', named) = split res res
-    in  ( Anon
-#if MIN_VERSION_ghc(8,10,0)
-          af
-#endif
-#if MIN_VERSION_ghc(9,0,0)
-          (mkScaled w arg)
-#else
-          arg
-#endif
-          : bs
-        , ty', named
-        )
-  split orig_ty ty' | Just ty'' <- coreView ty' = split orig_ty ty''
-  split orig_ty _ = ([], orig_ty, False)
-{-# INLINE split_pi_tys' #-}
-
-ty_con_binders_ty_binders' :: [TyConBinder] -> ([TyCoBinder], Bool)
-ty_con_binders_ty_binders' = foldr go ([], False)
-  where
-    go (Bndr tv (NamedTCB vis)) (bndrs, _)
-      = (Named (Bndr tv vis) : bndrs, True)
-    go (Bndr tv
-         (AnonTCB
-#if MIN_VERSION_ghc(8,10,0)
-           af
-#endif
-         )
-       )   (bndrs, n)
-      = (Anon
-#if MIN_VERSION_ghc(8,10,0)
-          af
-#endif
-          (
-#if MIN_VERSION_ghc(9,0,0)
-            tymult
-#endif
-             (tyVarKind tv)
-          )
-          : bndrs
-        , n)
-    {-# INLINE go #-}
-{-# INLINE ty_con_binders_ty_binders' #-}
-
-{-# INLINE rewrite_args #-}
-rewrite_args :: [TyCoBinder] -> Bool
-             -> Kind -> TcTyCoVarSet
-             -> Maybe [Role] -> [Type]
-             -> RewriteM ArgsReductions
-rewrite_args orig_binders
-             any_named_bndrs
-             orig_inner_ki
-             orig_fvs
-             orig_m_roles
-             orig_tys
-  = case (orig_m_roles, any_named_bndrs) of
-      (Nothing, False) -> rewrite_args_fast orig_tys
-      _ -> rewrite_args_slow orig_binders orig_inner_ki orig_fvs orig_roles orig_tys
-        where orig_roles = fromMaybe (repeat Nominal) orig_m_roles
-
-{-# INLINE rewrite_args_fast #-}
-rewrite_args_fast :: [Type] -> RewriteM ArgsReductions
-rewrite_args_fast orig_tys
-  = fmap finish (iterate orig_tys)
-  where
-
-    iterate :: [Type] -> RewriteM Reductions
-    iterate (ty : tys) = do
-      Reduction  co  xi  <- rewrite_one ty
-      Reductions cos xis <- iterate tys
-      pure $ Reductions (co : cos) (xi : xis)
-    iterate [] = pure $ Reductions [] []
-
-    {-# INLINE finish #-}
-    finish :: Reductions -> ArgsReductions
-    finish redns = ArgsReductions redns MRefl
-
-{-# INLINE rewrite_args_slow #-}
-rewrite_args_slow :: [TyCoBinder] -> Kind -> TcTyCoVarSet
-                  -> [Role] -> [Type]
-                  -> RewriteM ArgsReductions
-rewrite_args_slow binders inner_ki fvs roles tys
-  = do { rewritten_args <- zipWith3M fl (map isNamedBinder binders ++ repeat True)
-                                        roles tys
-       ; return $ simplifyArgsWorker binders inner_ki fvs roles rewritten_args }
-  where
-    {-# INLINE fl #-}
-    fl :: Bool   -- must we ensure to produce a real coercion here?
-                 -- see comment at top of function
-       -> Role -> Type -> RewriteM Reduction
-    fl True  r ty = noBogusCoercions $ fl1 r ty
-    fl False r ty =                    fl1 r ty
-
-    {-# INLINE fl1 #-}
-    fl1 :: Role -> Type -> RewriteM Reduction
-    fl1 Nominal ty
-      = setEqRel NomEq $
-        rewrite_one ty
-
-    fl1 Representational ty
-      = setEqRel ReprEq $
-        rewrite_one ty
-
-    fl1 Phantom ty
-      = do { ty' <- liftTcS $ zonkTcType ty
-           ; return $ mkReflRedn Phantom ty' }
-
-noBogusCoercions :: RewriteM a -> RewriteM a
-noBogusCoercions thing_inside
-  = RewriteM \ env s ->
-    let !renv  = rewriteEnv env
-        !renv' = case fe_flavour renv of
-          Derived -> renv { fe_flavour = Wanted WDeriv }
-          _       -> renv
-        !env' = env { rewriteEnv = renv' }
-    in
-    runRewriteM thing_inside env' s
-
-chkAppend :: [a] -> [a] -> [a]
-chkAppend xs ys
-  | null ys   = xs
-  | otherwise = xs ++ ys
-
---------------------------------------------------------------------------------
-
-data ReduceQ = NoReduction | DidReduce
-instance Semigroup ReduceQ where
-  NoReduction <> NoReduction = NoReduction
-  _ <> _ = DidReduce
-instance Monoid ReduceQ where
-  mempty = NoReduction
-
-data RewriteState =
-  RewriteState
-   { rewrittenCts      :: ![ Ct ]
-   , reductionOccurred :: !ReduceQ
-   }
-
-data ShimRewriteEnv
-  = ShimRewriteEnv
-  { rewriters     :: !Rewriters
-  , rewriteEnv    :: !RewriteEnv
-  , rewriteGivens :: ![ Ct ]
-  }
-
-newtype RewriteM a
-  = RewriteM
-  { runRewriteM
-    :: ShimRewriteEnv
-    -> RewriteState
-    -> TcS ( a, RewriteState )
-  }
-  deriving ( Functor, Applicative, Monad )
-    via ( ReaderT ShimRewriteEnv
-          ( StateT RewriteState TcS )
-        )
-
-runRewritePluginM :: ShimRewriteEnv
-                  -> RewriteM a
-                  -> TcPluginM ( Maybe a, [Ct] )
-runRewritePluginM env ( RewriteM { runRewriteM = run } ) = do
-
-  evBindsVar <- getEvBindsTcPluginM
-  ( a, RewriteState { rewrittenCts, reductionOccurred } )
-    <- unsafeTcPluginTcM
-     $ runTcSWithEvBinds evBindsVar
-     $ run env ( RewriteState [] NoReduction )
-  let
-    mb_a = case reductionOccurred of
-      NoReduction -> Nothing
-      DidReduce   -> Just a
-  pure ( mb_a, rewrittenCts )
-
-addRewriting :: Maybe Reduction -> [Ct] -> RewriteM ( Maybe Reduction )
-addRewriting mbRedn newCts = RewriteM \ _ ( RewriteState cts s ) ->
-  let
-    s' :: ReduceQ
-    s'
-      | Just _ <- mbRedn
-      = DidReduce
-      | otherwise
-      = s
-  in pure ( mbRedn , RewriteState ( cts <> newCts ) s' )
-
-getRewriters :: RewriteM Rewriters
-getRewriters = RewriteM \ env s -> pure ( rewriters env, s )
-
-getRewriteEnvField :: (RewriteEnv -> a) -> RewriteM a
-getRewriteEnvField accessor = RewriteM \ env s ->
-  pure ( accessor ( rewriteEnv env ), s )
-
-getEqRel :: RewriteM EqRel
-getEqRel = getRewriteEnvField fe_eq_rel
-
-getRole :: RewriteM Role
-getRole = eqRelRole <$> getEqRel
-
-getFlavour :: RewriteM CtFlavour
-getFlavour = getRewriteEnvField fe_flavour
-
-getFlavourRole :: RewriteM CtFlavourRole
-getFlavourRole = do
-  flavour <- getFlavour
-  eq_rel <- getEqRel
-  return (flavour, eq_rel)
-
-setEqRel :: EqRel -> RewriteM a -> RewriteM a
-setEqRel new_eq_rel thing_inside = RewriteM \ env s ->
-  if new_eq_rel == fe_eq_rel ( rewriteEnv env )
-  then runRewriteM thing_inside env s
-  else runRewriteM thing_inside ( setEqRel' env ) s
-    where
-      setEqRel' :: ShimRewriteEnv -> ShimRewriteEnv
-      setEqRel' env = env { rewriteEnv = ( rewriteEnv env ) { fe_eq_rel = new_eq_rel } }
-{-# INLINE setEqRel #-}
-
-liftTcS :: TcS a -> RewriteM a
-liftTcS thing_inside = RewriteM \ _env s -> do
-  a <- thing_inside
-  pure ( a, s )
-
-traceRewriteM :: String -> SDoc -> RewriteM ()
-traceRewriteM herald doc = liftTcS $ traceTcS herald doc
-{-# INLINE traceRewriteM #-}
-
-getLoc :: RewriteM CtLoc
-getLoc = getRewriteEnvField fe_loc
-
-checkStackDepth :: Type -> RewriteM ()
-checkStackDepth ty = do
-  loc <- getLoc
-  liftTcS $ checkReductionDepth loc ty
-
-bumpDepth :: RewriteM a -> RewriteM a
-bumpDepth (RewriteM thing_inside) = RewriteM \ env s -> do
-  let !renv  = rewriteEnv env
-      !renv' = renv { fe_loc = bumpCtLocDepth ( fe_loc renv ) }
-      !env'  = env { rewriteEnv = renv' }
-  thing_inside env' s
-
-#if !MIN_VERSION_ghc(9,2,0)
---------------------------------------------------------------------------------
--- GHC 9.0 compatibility.
-
-firstJustsM :: (Monad m, Foldable f) => f (m (Maybe a)) -> m (Maybe a)
-firstJustsM = foldlM go Nothing where
-  go :: Monad m => Maybe a -> m (Maybe a) -> m (Maybe a)
-  go Nothing         action  = action
-  go result@(Just _) _action = return result
-
-lookupFamAppCache :: TyCon -> [Type] -> TcS (Maybe (Coercion, Type))
-lookupFamAppCache fam_tc tys = do
-  res <- lookupFlatCache fam_tc tys
-  pure $ case res of
-    Nothing -> Nothing
-    Just  ( co, ty, _ ) -> Just ( co, ty )
-
-extendFamAppCache :: TyCon -> [Type] -> (Coercion, Type) -> CtFlavour -> TcS ()
-extendFamAppCache tc xi_args (co, ty) f = extendFlatCache tc xi_args (co, ty, f)
-
-lookupFamAppInert :: TyCon -> [Type] -> TcS (Maybe (Coercion, Type, CtFlavourRole))
-lookupFamAppInert tc tys = do
-  res <- lookupFlatCache tc tys
-  pure $ case res of
-    Nothing -> Nothing
-    Just ( co, ty, f ) -> Just ( co, ty, (f, NomEq) )
-
-tcSplitForAllTyVarBinders :: Type -> ([TyVarBinder], Type)
-tcSplitForAllTyVarBinders = tcSplitForAllVarBndrs
-
-#endif
+{-# LANGUAGE BangPatterns    #-}+{-# LANGUAGE BlockArguments  #-}+{-# LANGUAGE CPP             #-}+{-# LANGUAGE DerivingVia     #-}+{-# LANGUAGE LambdaCase      #-}+{-# LANGUAGE NamedFieldPuns  #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE TupleSections   #-}+{-# LANGUAGE ViewPatterns    #-}++{-|+Module: GHC.TcPlugin.API.Internal.Shim++This module defines a compatibility shim which allows+the library to support a limited form of type-family rewriting+in typechecking plugins on GHC 9.0 and 9.2.+-}++module GHC.TcPlugin.API.Internal.Shim+  ( Reduction(..), mkReduction+  , TcPluginSolveResult(TcPluginContradiction, TcPluginOk, ..), TcPluginRewriteResult(..)+  , RewriteEnv(..)+  , shimRewriter+  )+  where++-- base+import Prelude+  hiding ( Floating(cos), iterate )+import Control.Monad+  ( forM, unless, when )+import Data.Foldable+  ( traverse_+#if !MIN_VERSION_ghc(9,2,0)+  , foldlM+#endif+  )+#if MIN_VERSION_ghc(9,2,0)+import Data.List.NonEmpty+  ( NonEmpty((:|)) )+#endif+import Data.Maybe+  ( fromMaybe )++-- transformers+import Control.Monad.Trans.Reader+  ( ReaderT(..) )+import Control.Monad.Trans.State.Strict+  ( StateT(..) )++-- ghc+import GHC.Core.Coercion+  ( coercionRole+  , mkReflCo, mkSymCo+  , mkAppCos, mkNomReflCo, mkSubCo+  , mkTyConAppCo, tyConRolesX+  , tyConRolesRepresentational+  )+import GHC.Core.Predicate+  ( EqRel(..), eqRelRole )+import GHC.Core.TyCo.Rep+  ( Type(..), Kind, Coercion(..), MCoercion(..), TyCoBinder(..)+  , isNamedBinder, mkTyVarTy+  )+import GHC.Core.TyCon+  ( TyCon(..), TyConBinder, TyConBndrVis(..)+#if MIN_VERSION_ghc(9,2,0)+  , isForgetfulSynTyCon+#endif+  , isFamFreeTyCon, isTypeSynonymTyCon+  , isTypeFamilyTyCon+  , tyConBinders, tyConResKind+  , tyConArity+  )+import GHC.Core.Type+  ( TyVar+  , tcView , mkTyConApp+#if MIN_VERSION_ghc(9,0,0)+  , mkScaled, tymult+#endif+  , coreView, tyVarKind+  )+#if MIN_VERSION_ghc(9,2,0)+import GHC.Data.Maybe+  ( firstJustsM )+#endif+import GHC.Tc.Plugin+  ( newWanted, newDerived )+import GHC.Tc.Solver.Monad+  ( TcS+  , zonkCo, zonkTcType+  , isFilledMetaTyVar_maybe+  , getInertEqs+  , checkReductionDepth+  , matchFam+  , runTcPluginTcS, runTcSWithEvBinds+  , traceTcS+  , setWantedEvTerm+#if MIN_VERSION_ghc(9,2,0)+  , lookupFamAppCache, lookupFamAppInert, extendFamAppCache+  , pattern EqualCtList+#else+  , lookupFlatCache, extendFlatCache+#endif+  )+import GHC.Tc.Types+  ( TcPluginM+  , unsafeTcPluginTcM, getEvBindsTcPluginM+  )+import qualified GHC.Tc.Types as GHC+  ( TcPluginResult(..) )+import GHC.Tc.Types.Constraint+  ( Ct(..), CtEvidence(..)+  , CtLoc, CtFlavour(..), CtFlavourRole, ShadowInfo(..)+#if MIN_VERSION_ghc(9,2,0)+  , CanEqLHS(..)+#endif+  , ctLoc, ctFlavour, ctEvidence, ctEqRel, ctEvPred+  , ctEvExpr, ctEvCoercion, ctEvFlavour+  , bumpCtLocDepth, eqCanRewriteFR, mkNonCanonical+  )+import GHC.Tc.Types.Evidence+  ( EvTerm(..), Role(..)+  , evCast, mkTcTransCo , mkTcTyConAppCo+  )+import GHC.Tc.Utils.TcType+  ( TcTyCoVarSet+#if MIN_VERSION_ghc(9,2,0)+  , tcSplitForAllTyVarBinders+#else+  , tcSplitForAllVarBndrs+#endif+  , tcSplitTyConApp_maybe+  , tcTypeKind+  , tyCoVarsOfType+  )+import GHC.Types.Unique.FM+  ( UniqFM, lookupUFM, isNullUFM )+import GHC.Types.Var+  ( TcTyVar, VarBndr(..)+#if !MIN_VERSION_ghc(9,2,0)+  , TyVarBinder+#endif+  , updateTyVarKindM+  )+import GHC.Types.Var.Env+  ( lookupDVarEnv )+import GHC.Types.Var.Set+  ( emptyVarSet )+import GHC.Utils.Misc+  ( dropList )+import GHC.Utils.Monad+  ( zipWith3M )+import GHC.Utils.Outputable+  ( Outputable(..), SDoc, empty )++-- ghc-tcplugin-api+import GHC.TcPlugin.API.Internal.Shim.Reduction++--------------------------------------------------------------------------------++-- | The type-family rewriting environment.+data RewriteEnv+  = FE { fe_loc     :: !CtLoc+       , fe_flavour :: !CtFlavour+       , fe_eq_rel  :: !EqRel+       }++-- | Result of running a solver plugin.+data TcPluginSolveResult+  = TcPluginSolveResult+  { -- | Insoluble constraints found by the plugin.+    --+    -- These constraints will be added to the inert set,+    -- and reported as insoluble to the user.+    tcPluginInsolubleCts :: [Ct]+    -- | Solved constraints, together with their evidence.+    --+    -- These are removed from the inert set, and the+    -- evidence for them is recorded.+  , tcPluginSolvedCts :: [(EvTerm, Ct)]+    -- | New constraints that the plugin wishes to emit.+    --+    -- These will be added to the work list.+  , tcPluginNewCts :: [Ct]+  }++-- | The plugin found a contradiction.+-- The returned constraints are removed from the inert set,+-- and recorded as insoluble.+--+-- The returned list of constraints should never be empty.+pattern TcPluginContradiction :: [Ct] -> TcPluginSolveResult+pattern TcPluginContradiction insols+  = TcPluginSolveResult+  { tcPluginInsolubleCts = insols+  , tcPluginSolvedCts    = []+  , tcPluginNewCts       = [] }++-- | The plugin has not found any contradictions,+--+-- The first field is for constraints that were solved.+-- The second field contains new work, that should be processed by+-- the constraint solver.+pattern TcPluginOk :: [(EvTerm, Ct)] -> [Ct] -> TcPluginSolveResult+pattern TcPluginOk solved new+  = TcPluginSolveResult+  { tcPluginInsolubleCts = []+  , tcPluginSolvedCts    = solved+  , tcPluginNewCts       = new }++-- The 'TcPluginSolveResult' datatype changed in GHC 9.4,+-- allowing users to return solved and new constraints even in case of+-- a contradiction.+--+-- This function simply drops the solved and new constraints on older versions,+-- although it does at least still bind the evidence in case of solved Wanteds.+adaptSolveResult :: Bool -> TcPluginSolveResult -> TcPluginM GHC.TcPluginResult+adaptSolveResult doingGivens+  ( TcPluginSolveResult+    { tcPluginInsolubleCts = insols+    , tcPluginSolvedCts    = solved+    , tcPluginNewCts       = new+    }+  )+    | null insols+    = pure $ GHC.TcPluginOk solved new+    | null solved && null new+    = pure $ GHC.TcPluginContradiction insols+    | otherwise+    = do+      evBinds <- getEvBindsTcPluginM+      unsafeTcPluginTcM . runTcSWithEvBinds evBinds $ do+        unless doingGivens $ traverse_ ( uncurry setEv ) solved+        --updInertCans (removeInertCts $ fmap snd solved) -- These don't do anything, as the inert set and work list+        --emitWork new                                    -- are confined to this run of the plugin.+      pure $ GHC.TcPluginContradiction insols+  where+    setEv :: EvTerm -> Ct -> TcS ()+    setEv ev ( ctEvidence -> CtWanted { ctev_dest = dest } )+      = setWantedEvTerm dest ev+    setEv _ _+      = pure ()++data TcPluginRewriteResult+  =+  -- | The plugin does not rewrite the type family application.+    TcPluginNoRewrite++  -- | The plugin rewrites the type family application+  -- providing a rewriting together with evidence.+  --+  -- The plugin can also emit additional wanted constraints.+  | TcPluginRewriteTo+    { tcPluginReduction :: !Reduction+    , tcRewriterWanteds :: [Ct]+    }++type Rewriter = RewriteEnv -> [Ct] -> [Type] -> TcPluginM TcPluginRewriteResult++type Rewriters =+  UniqFM+#if MIN_VERSION_ghc(9,0,0)+    TyCon+#endif+    Rewriter++-- | Emulate type-family rewriting functionality in a constraint solving plugin,+-- by traversing through all the constraints and rewriting any type-family applications+-- inside them.+shimRewriter :: [Ct] -> [Ct] -> [Ct]+             -> Rewriters+             -> ( [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginSolveResult )+             -> TcPluginM GHC.TcPluginResult+shimRewriter givens deriveds wanteds rws solver+  | isNullUFM rws+  = adaptSolveResult (null wanteds) =<< solver givens deriveds wanteds+  | otherwise+  = do+    TcPluginSolveResult+      { tcPluginInsolubleCts = contras+      , tcPluginSolvedCts    = solved+      , tcPluginNewCts       = new+      } <- solver givens deriveds wanteds+    ( rewrittenDeriveds, solvedDeriveds, newCts1 ) <- traverseCts ( reduceCt rws givens ) deriveds+    ( rewrittenWanteds , solvedWanteds , newCts2 ) <- traverseCts ( reduceCt rws givens ) wanteds+    adaptSolveResult (null wanteds) $+      TcPluginSolveResult+        { tcPluginInsolubleCts = contras+        , tcPluginSolvedCts    = solved ++ solvedDeriveds ++ solvedWanteds+        , tcPluginNewCts       = new ++ newCts1 ++ rewrittenDeriveds ++ newCts2 ++ rewrittenWanteds+        }++reduceCt :: Rewriters+         -> [Ct]+         -> Ct+         -> TcPluginM ( Maybe ( Ct, (EvTerm, Ct) ), [Ct] )+reduceCt rws givens ct = do+  let+    predTy :: Type+    predTy = ctEvPred ( ctEvidence ct )+    rwEnv :: RewriteEnv+    rwEnv = FE ( ctLoc ct ) ( ctFlavour ct ) ( ctEqRel ct )+    shimRewriteEnv :: ShimRewriteEnv+    shimRewriteEnv = ShimRewriteEnv rws rwEnv givens+  ( res, newCts ) <- runRewritePluginM shimRewriteEnv ( rewrite_one predTy )+  case res of+    Nothing -> pure ( Nothing, newCts )+    Just ( Reduction co predTy' ) -> do+      ctEv' <- case ctFlavour ct of+        Given     -> error "ghc-tcplugin-api: unexpected Given in reduceCt"+        Wanted {} -> newWanted  ( ctLoc ct ) predTy'+        Derived   -> newDerived ( ctLoc ct ) predTy'+      let+        role :: Role+        role = coercionRole co+        cast_co :: Coercion+        cast_co = mkSymCo $ case role of+          Nominal -> mkSubCo co+          _       -> co+      pure ( Just+              ( mkNonCanonical ctEv'+              , ( evCast ( ctEvExpr ctEv' ) cast_co, ct )+              )+           , newCts+           )++traverseCts :: Monad m+            => ( a -> m ( Maybe (b, c), [d] ) )+            -> [a]+            -> m ( [b], [c], [d] )+traverseCts _ [] = pure ( [], [], [] )+traverseCts f (a : as) = do+  ( mb_bc, ds ) <- f a+  ( bs, cs, dss ) <- traverseCts f as+  case mb_bc of+    Nothing    -> pure ( bs, cs, ds ++ dss )+    Just (b,c) -> pure ( b : bs, c : cs, ds ++ dss )++--------------------------------------------------------------------------------+-- The following is (mostly) copied from GHC 9.4's GHC.Tc.Solver.Rewrite module.++rewrite_one :: Type -> RewriteM Reduction+rewrite_one ty+  | Just ty' <- rewriterView ty  -- See Note [Rewriting synonyms]+  = rewrite_one ty'++rewrite_one xi@(LitTy {})+  = do { role <- getRole+       ; return $ mkReflRedn role xi }++rewrite_one (TyVarTy tv)+  = rewriteTyVar tv++rewrite_one (AppTy ty1 ty2)+  = rewrite_app_tys ty1 [ty2]++rewrite_one (TyConApp tc tys)+  | isTypeFamilyTyCon tc+  = rewrite_fam_app tc tys++  | otherwise+  = rewrite_ty_con_app tc tys++rewrite_one+  (FunTy+#if MIN_VERSION_ghc(8,10,0)+    vis+#endif+#if MIN_VERSION_ghc(9,0,0)+    mult+#endif+    ty1+    ty2+  )+  = do { arg_redn <- rewrite_one ty1+       ; res_redn <- rewrite_one ty2+#if MIN_VERSION_ghc(9,0,0)+       ; w_redn <- setEqRel NomEq $ rewrite_one mult+#endif+       ; role <- getRole+       ; return $+           mkFunRedn+             role+#if MIN_VERSION_ghc(8,10,0)+             vis+#endif+#if MIN_VERSION_ghc(9,0,0)+             w_redn+#endif+             arg_redn+             res_redn+        }++rewrite_one ty@(ForAllTy {})+  = do { let (bndrs, rho) = tcSplitForAllTyVarBinders ty+       ; redn <- rewrite_one rho+       ; return $ mkHomoForAllRedn bndrs redn }++rewrite_one (CastTy ty g)+  = do { redn <- rewrite_one ty+       ; g'   <- rewrite_co g+       ; role <- getRole+       ; return $ mkCastRedn1 role ty g' redn }++rewrite_one (CoercionTy co)+  = do { co' <- rewrite_co co+       ; role <- getRole+       ; return $ mkReflCoRedn role co' }++rewrite_reduction :: Reduction -> RewriteM Reduction+rewrite_reduction (Reduction co xi) = do+  redn <- bumpDepth $ rewrite_one xi+  pure $ co `mkTransRedn` redn++rewrite_app_tys :: Type -> [Type] -> RewriteM Reduction+rewrite_app_tys (AppTy ty1 ty2) tys = rewrite_app_tys ty1 (ty2:tys)+rewrite_app_tys fun_ty arg_tys+  = do { redn <- rewrite_one fun_ty+       ; rewrite_app_ty_args redn arg_tys }++rewrite_app_ty_args :: Reduction -> [Type] -> RewriteM Reduction+rewrite_app_ty_args redn []+  = return redn+rewrite_app_ty_args fun_redn@(Reduction fun_co fun_xi) arg_tys+  = do { het_redn <- case tcSplitTyConApp_maybe fun_xi of+           Just (tc, xis) ->+             do { let tc_roles  = tyConRolesRepresentational tc+                      arg_roles = dropList xis tc_roles+                ; ArgsReductions (Reductions arg_cos arg_xis) kind_co+                    <- rewrite_vector (tcTypeKind fun_xi) arg_roles arg_tys++                ; eq_rel <- getEqRel+                ; let app_xi = mkTyConApp tc (xis ++ arg_xis)+                      app_co = case eq_rel of+                        NomEq  -> mkAppCos fun_co arg_cos+                        ReprEq -> mkAppCos fun_co (map mkNomReflCo arg_tys)+                                  `mkTcTransCo`+                                  mkTcTyConAppCo Representational tc+                                    (zipWith mkReflCo tc_roles xis ++ arg_cos)++                ; return $+                    mkHetReduction+                      (mkReduction app_co app_xi )+                      kind_co }+           Nothing ->+             do { ArgsReductions redns kind_co+                    <- rewrite_vector (tcTypeKind fun_xi) (repeat Nominal) arg_tys+                ; return $ mkHetReduction (mkAppRedns fun_redn redns) kind_co }++       ; role <- getRole+       ; return (homogeniseHetRedn role het_redn) }++{-# INLINE rewrite_args_tc #-}+rewrite_args_tc :: TyCon -> Maybe [Role] -> [Type] -> RewriteM ArgsReductions+rewrite_args_tc tc = rewrite_args all_bndrs any_named_bndrs inner_ki emptyVarSet+  -- NB: TyCon kinds are always closed+  where+  -- There are many bang patterns in here. It's been observed that they+  -- greatly improve performance of an optimized build.+  -- The T9872 test cases are good witnesses of this fact.++    (bndrs, named)+      = ty_con_binders_ty_binders' (tyConBinders tc)+    -- it's possible that the result kind has arrows (for, e.g., a type family)+    -- so we must split it+    (inner_bndrs, inner_ki, inner_named) = split_pi_tys' (tyConResKind tc)+    !all_bndrs                           = bndrs `chkAppend` inner_bndrs+    !any_named_bndrs                     = named || inner_named+    -- NB: Those bangs there drop allocations in T9872{a,c,d} by 8%.++rewrite_fam_app :: TyCon -> [Type] -> RewriteM Reduction+rewrite_fam_app tc tys = do+  let (tys1, tys_rest) = splitAt (tyConArity tc) tys+  redn <- rewrite_exact_fam_app tc tys1+  rewrite_app_ty_args redn tys_rest++rewrite_exact_fam_app :: TyCon -> [Type] -> RewriteM Reduction+rewrite_exact_fam_app tc tys = do+  checkStackDepth $ mkTyConApp tc tys+  rws <- getRewriters+  let+    mbRewriter :: Maybe Rewriter+    mbRewriter = lookupUFM rws tc+  result1 <- try_to_reduce tc tys mbRewriter+  case result1 of+    Just redn -> finish False redn+    _ -> do+      eq_rel <- getEqRel+      ArgsReductions (Reductions cos xis) kind_co <-+        if eq_rel == NomEq+        then rewrite_args_tc tc Nothing tys+        else setEqRel NomEq $+             rewrite_args_tc tc Nothing tys+      let+        role    = eqRelRole eq_rel+        args_co = mkTyConAppCo role tc cos+        homogenise :: Reduction -> Reduction+        homogenise redn+          = homogeniseHetRedn role+          $ mkHetReduction+              (args_co `mkTransRedn` redn)+              kind_co+        give_up :: Reduction+        give_up = homogenise $ mkReflRedn role (mkTyConApp tc xis)++      result2 <- liftTcS $ lookupFamAppInert tc xis+      flavour <- getFlavour+      case result2 of+        Just (co, xi, fr@(_, inert_eq_rel))+          | fr `eqCanRewriteFR` (flavour, eq_rel)+          , let+              redn :: Reduction+              redn = Reduction (mkSymCo co) xi -- inerts use a different orientation in GHC 9.0 and 9.2+          -> finish True (homogenise $ downgradeRedn role' inert_role redn)+          where+            inert_role      = eqRelRole inert_eq_rel+            role'           = eqRelRole eq_rel+        _ -> do+          result3 <- try_to_reduce tc xis mbRewriter+          case result3 of+            Just redn -> finish True (homogenise redn)+            _         -> return give_up+  where+    finish :: Bool -> Reduction -> RewriteM Reduction+    finish use_cache (Reduction co xi) = do+      Reduction fully_co fully <- bumpDepth $ rewrite_one xi+      let final_redn@(Reduction final_co final_xi) = Reduction (co `mkTcTransCo` fully_co) fully+      eq_rel <- getEqRel+      flavour <- getFlavour+      when (use_cache && eq_rel == NomEq && flavour /= Derived) $+        liftTcS $+          extendFamAppCache tc tys+            ( mkSymCo final_co, final_xi ) -- different orientation in GHC 9.0 and 9.2+#if !MIN_VERSION_ghc(9,2,0)+            flavour+#endif+      return final_redn+    {-# INLINE finish #-}++-- Returned coercion is output ~r input, where r is the role in the RewriteM monad+-- See Note [How to normalise a family application]+try_to_reduce :: TyCon -> [Type] -> Maybe Rewriter+              -> RewriteM (Maybe Reduction)+try_to_reduce tc tys mb_rewriter = do+  result <-+    firstJustsM+      [ runTcPluginRewriter mb_rewriter tys+      , liftTcS $ mkRed <$> lookupFamAppCache tc tys+      , liftTcS $ mkRed <$> matchFam tc tys ]+  forM result downgrade+    where+      mkRed :: Maybe (Coercion, Type) -> Maybe Reduction+      mkRed = fmap $ \ (co, ty) -> Reduction (mkSymCo co) ty+      downgrade :: Reduction -> RewriteM Reduction+      downgrade redn@(Reduction co xi) = do+        eq_rel <- getEqRel+        case eq_rel of+          NomEq  -> return redn+          ReprEq -> return $ Reduction (mkSubCo co) xi++runTcPluginRewriter :: Maybe Rewriter+                    -> [Type]+                    -> RewriteM (Maybe Reduction)+runTcPluginRewriter mbRewriter tys =+  case mbRewriter of+    Nothing -> return Nothing+    Just rewriter -> do+      traceRewriteM "runTcPluginRewriter { " empty+      res <- runRewriter rewriter+      traceRewriteM "runTcPluginRewriter }" ( ppr res )+      pure res+  where+  runRewriter :: Rewriter -> RewriteM (Maybe Reduction)+  runRewriter rewriter = do+    rewriteResult <- RewriteM \ env s -> do+      res <- runTcPluginTcS ( rewriter ( rewriteEnv env ) ( rewriteGivens env ) tys )+      pure ( res, s )+    case rewriteResult of+      TcPluginRewriteTo+        { tcPluginReduction = redn+        , tcRewriterWanteds = wanteds+        } -> addRewriting ( Just redn ) wanteds+      TcPluginNoRewrite { }+          -> addRewriting Nothing []++rewrite_ty_con_app :: TyCon -> [Type] -> RewriteM Reduction+rewrite_ty_con_app tc tys+  = do { role <- getRole+       ; let m_roles | Nominal <- role = Nothing+                     | otherwise       = Just $ tyConRolesX role tc+       ; ArgsReductions redns kind_co <- rewrite_args_tc tc m_roles tys+       ; let tyconapp_redn+                = mkHetReduction+                    (mkTyConAppRedn role tc redns)+                    kind_co+       ; return $ homogeniseHetRedn role tyconapp_redn }++rewrite_co :: Coercion -> RewriteM Coercion+rewrite_co co = liftTcS $ zonkCo co++rewriterView :: Type -> Maybe Type+rewriterView ty@(TyConApp tc _)+  | ( isTypeSynonymTyCon tc && not (isFamFreeTyCon tc) )+#if MIN_VERSION_ghc(9,2,0)+  || isForgetfulSynTyCon tc+#endif+  = tcView ty+rewriterView _other = Nothing++rewriteTyVar :: TyVar -> RewriteM Reduction+rewriteTyVar tv = do+  mb_yes <- rewrite_tyvar1 tv+  case mb_yes of+    RTRFollowed redn -> rewrite_reduction redn+    RTRNotFollowed -> do+      tv' <- liftTcS $ updateTyVarKindM zonkTcType tv+      role <- getRole+      let ty' = mkTyVarTy tv'+      pure $ mkReflRedn role ty'++data RewriteTvResult+  = RTRNotFollowed+  | RTRFollowed !Reduction++rewrite_tyvar1 :: TcTyVar -> RewriteM RewriteTvResult+rewrite_tyvar1 tv = do+  mb_ty <- liftTcS $ isFilledMetaTyVar_maybe tv+  case mb_ty of+    Just ty -> do+      role <- getRole+      return $ RTRFollowed $ mkReflRedn role ty+    Nothing -> do+      fr <- getFlavourRole+      rewrite_tyvar2 tv fr++rewrite_tyvar2 :: TcTyVar -> CtFlavourRole -> RewriteM RewriteTvResult+rewrite_tyvar2 tv fr@(_, eq_rel) = do+  ieqs <- liftTcS $ getInertEqs+  case lookupDVarEnv ieqs tv of+#if MIN_VERSION_ghc(9,2,0)+    Just (EqualCtList (ct :| _))+      | CEqCan { cc_ev = ctev, cc_lhs = TyVarLHS {}+               , cc_rhs = rhs_ty, cc_eq_rel = ct_eq_rel } <- ct+#else+    Just (ct : _)+      | CTyEqCan { cc_ev = ctev+                 , cc_rhs = rhs_ty, cc_eq_rel = ct_eq_rel } <- ct+#endif+      , let ct_fr = (ctEvFlavour ctev, ct_eq_rel)+      , ct_fr `eqCanRewriteFR` fr+      -> do+          let rewriting_co1 = ctEvCoercion ctev+              rewriting_co  = case (ct_eq_rel, eq_rel) of+                (ReprEq, _rel)  -> rewriting_co1+                (NomEq, NomEq)  -> rewriting_co1+                (NomEq, ReprEq) -> mkSubCo rewriting_co1+          return $ RTRFollowed $ mkReduction rewriting_co rhs_ty +    _other -> return RTRNotFollowed++rewrite_vector :: Kind+               -> [Role]+               -> [Type]+               -> RewriteM ArgsReductions+rewrite_vector ki roles tys+  = do { eq_rel <- getEqRel+       ; let mb_roles = case eq_rel of { NomEq -> Nothing; ReprEq -> Just roles }+       ; rewrite_args bndrs any_named_bndrs inner_ki fvs mb_roles tys+       }+  where+    (bndrs, inner_ki, any_named_bndrs) = split_pi_tys' ki+    fvs                                = tyCoVarsOfType ki+{-# INLINE rewrite_vector #-}++split_pi_tys' :: Type -> ([TyCoBinder], Type, Bool)+split_pi_tys' ty = split ty ty+  where+  split _ (ForAllTy b res) =+    let !(bs, ty', _) = split res res+    in  (Named b : bs, ty', True)+  split _+    (FunTy+#if MIN_VERSION_ghc(8,10,0)+      af+#endif+#if MIN_VERSION_ghc(9,0,0)+      w+#endif+      arg+      res+    ) =+    let !(bs, ty', named) = split res res+    in  ( Anon+#if MIN_VERSION_ghc(8,10,0)+          af+#endif+#if MIN_VERSION_ghc(9,0,0)+          (mkScaled w arg)+#else+          arg+#endif+          : bs+        , ty', named+        )+  split orig_ty ty' | Just ty'' <- coreView ty' = split orig_ty ty''+  split orig_ty _ = ([], orig_ty, False)+{-# INLINE split_pi_tys' #-}++ty_con_binders_ty_binders' :: [TyConBinder] -> ([TyCoBinder], Bool)+ty_con_binders_ty_binders' = foldr go ([], False)+  where+    go (Bndr tv (NamedTCB vis)) (bndrs, _)+      = (Named (Bndr tv vis) : bndrs, True)+    go (Bndr tv+         (AnonTCB+#if MIN_VERSION_ghc(8,10,0)+           af+#endif+         )+       )   (bndrs, n)+      = (Anon+#if MIN_VERSION_ghc(8,10,0)+          af+#endif+          (+#if MIN_VERSION_ghc(9,0,0)+            tymult+#endif+             (tyVarKind tv)+          )+          : bndrs+        , n)+    {-# INLINE go #-}+{-# INLINE ty_con_binders_ty_binders' #-}++{-# INLINE rewrite_args #-}+rewrite_args :: [TyCoBinder] -> Bool+             -> Kind -> TcTyCoVarSet+             -> Maybe [Role] -> [Type]+             -> RewriteM ArgsReductions+rewrite_args orig_binders+             any_named_bndrs+             orig_inner_ki+             orig_fvs+             orig_m_roles+             orig_tys+  = case (orig_m_roles, any_named_bndrs) of+      (Nothing, False) -> rewrite_args_fast orig_tys+      _ -> rewrite_args_slow orig_binders orig_inner_ki orig_fvs orig_roles orig_tys+        where orig_roles = fromMaybe (repeat Nominal) orig_m_roles++{-# INLINE rewrite_args_fast #-}+rewrite_args_fast :: [Type] -> RewriteM ArgsReductions+rewrite_args_fast orig_tys+  = fmap finish (iterate orig_tys)+  where++    iterate :: [Type] -> RewriteM Reductions+    iterate (ty : tys) = do+      Reduction  co  xi  <- rewrite_one ty+      Reductions cos xis <- iterate tys+      pure $ Reductions (co : cos) (xi : xis)+    iterate [] = pure $ Reductions [] []++    {-# INLINE finish #-}+    finish :: Reductions -> ArgsReductions+    finish redns = ArgsReductions redns MRefl++{-# INLINE rewrite_args_slow #-}+rewrite_args_slow :: [TyCoBinder] -> Kind -> TcTyCoVarSet+                  -> [Role] -> [Type]+                  -> RewriteM ArgsReductions+rewrite_args_slow binders inner_ki fvs roles tys+  = do { rewritten_args <- zipWith3M fl (map isNamedBinder binders ++ repeat True)+                                        roles tys+       ; return $ simplifyArgsWorker binders inner_ki fvs roles rewritten_args }+  where+    {-# INLINE fl #-}+    fl :: Bool   -- must we ensure to produce a real coercion here?+                 -- see comment at top of function+       -> Role -> Type -> RewriteM Reduction+    fl True  r ty = noBogusCoercions $ fl1 r ty+    fl False r ty =                    fl1 r ty++    {-# INLINE fl1 #-}+    fl1 :: Role -> Type -> RewriteM Reduction+    fl1 Nominal ty+      = setEqRel NomEq $+        rewrite_one ty++    fl1 Representational ty+      = setEqRel ReprEq $+        rewrite_one ty++    fl1 Phantom ty+      = do { ty' <- liftTcS $ zonkTcType ty+           ; return $ mkReflRedn Phantom ty' }++noBogusCoercions :: RewriteM a -> RewriteM a+noBogusCoercions thing_inside+  = RewriteM \ env s ->+    let !renv  = rewriteEnv env+        !renv' = case fe_flavour renv of+          Derived -> renv { fe_flavour = Wanted WDeriv }+          _       -> renv+        !env' = env { rewriteEnv = renv' }+    in+    runRewriteM thing_inside env' s++chkAppend :: [a] -> [a] -> [a]+chkAppend xs ys+  | null ys   = xs+  | otherwise = xs ++ ys++--------------------------------------------------------------------------------++data ReduceQ = NoReduction | DidReduce+instance Semigroup ReduceQ where+  NoReduction <> NoReduction = NoReduction+  _ <> _ = DidReduce+instance Monoid ReduceQ where+  mempty = NoReduction++data RewriteState =+  RewriteState+   { rewrittenCts      :: ![ Ct ]+   , reductionOccurred :: !ReduceQ+   }++data ShimRewriteEnv+  = ShimRewriteEnv+  { rewriters     :: !Rewriters+  , rewriteEnv    :: !RewriteEnv+  , rewriteGivens :: ![ Ct ]+  }++newtype RewriteM a+  = RewriteM+  { runRewriteM+    :: ShimRewriteEnv+    -> RewriteState+    -> TcS ( a, RewriteState )+  }+  deriving ( Functor, Applicative, Monad )+    via ( ReaderT ShimRewriteEnv+          ( StateT RewriteState TcS )+        )++runRewritePluginM :: ShimRewriteEnv+                  -> RewriteM a+                  -> TcPluginM ( Maybe a, [Ct] )+runRewritePluginM env ( RewriteM { runRewriteM = run } ) = do++  evBindsVar <- getEvBindsTcPluginM+  ( a, RewriteState { rewrittenCts, reductionOccurred } )+    <- unsafeTcPluginTcM+     $ runTcSWithEvBinds evBindsVar+     $ run env ( RewriteState [] NoReduction )+  let+    mb_a = case reductionOccurred of+      NoReduction -> Nothing+      DidReduce   -> Just a+  pure ( mb_a, rewrittenCts )++addRewriting :: Maybe Reduction -> [Ct] -> RewriteM ( Maybe Reduction )+addRewriting mbRedn newCts = RewriteM \ _ ( RewriteState cts s ) ->+  let+    s' :: ReduceQ+    s'+      | Just _ <- mbRedn+      = DidReduce+      | otherwise+      = s+  in pure ( mbRedn , RewriteState ( cts <> newCts ) s' )++getRewriters :: RewriteM Rewriters+getRewriters = RewriteM \ env s -> pure ( rewriters env, s )++getRewriteEnvField :: (RewriteEnv -> a) -> RewriteM a+getRewriteEnvField accessor = RewriteM \ env s ->+  pure ( accessor ( rewriteEnv env ), s )++getEqRel :: RewriteM EqRel+getEqRel = getRewriteEnvField fe_eq_rel++getRole :: RewriteM Role+getRole = eqRelRole <$> getEqRel++getFlavour :: RewriteM CtFlavour+getFlavour = getRewriteEnvField fe_flavour++getFlavourRole :: RewriteM CtFlavourRole+getFlavourRole = do+  flavour <- getFlavour+  eq_rel <- getEqRel+  return (flavour, eq_rel)++setEqRel :: EqRel -> RewriteM a -> RewriteM a+setEqRel new_eq_rel thing_inside = RewriteM \ env s ->+  if new_eq_rel == fe_eq_rel ( rewriteEnv env )+  then runRewriteM thing_inside env s+  else runRewriteM thing_inside ( setEqRel' env ) s+    where+      setEqRel' :: ShimRewriteEnv -> ShimRewriteEnv+      setEqRel' env = env { rewriteEnv = ( rewriteEnv env ) { fe_eq_rel = new_eq_rel } }+{-# INLINE setEqRel #-}++liftTcS :: TcS a -> RewriteM a+liftTcS thing_inside = RewriteM \ _env s -> do+  a <- thing_inside+  pure ( a, s )++traceRewriteM :: String -> SDoc -> RewriteM ()+traceRewriteM herald doc = liftTcS $ traceTcS herald doc+{-# INLINE traceRewriteM #-}++getLoc :: RewriteM CtLoc+getLoc = getRewriteEnvField fe_loc++checkStackDepth :: Type -> RewriteM ()+checkStackDepth ty = do+  loc <- getLoc+  liftTcS $ checkReductionDepth loc ty++bumpDepth :: RewriteM a -> RewriteM a+bumpDepth (RewriteM thing_inside) = RewriteM \ env s -> do+  let !renv  = rewriteEnv env+      !renv' = renv { fe_loc = bumpCtLocDepth ( fe_loc renv ) }+      !env'  = env { rewriteEnv = renv' }+  thing_inside env' s++#if !MIN_VERSION_ghc(9,2,0)+--------------------------------------------------------------------------------+-- GHC 9.0 compatibility.++firstJustsM :: (Monad m, Foldable f) => f (m (Maybe a)) -> m (Maybe a)+firstJustsM = foldlM go Nothing where+  go :: Monad m => Maybe a -> m (Maybe a) -> m (Maybe a)+  go Nothing         action  = action+  go result@(Just _) _action = return result++lookupFamAppCache :: TyCon -> [Type] -> TcS (Maybe (Coercion, Type))+lookupFamAppCache fam_tc tys = do+  res <- lookupFlatCache fam_tc tys+  pure $ case res of+    Nothing -> Nothing+    Just  ( co, ty, _ ) -> Just ( co, ty )++extendFamAppCache :: TyCon -> [Type] -> (Coercion, Type) -> CtFlavour -> TcS ()+extendFamAppCache tc xi_args (co, ty) f = extendFlatCache tc xi_args (co, ty, f)++lookupFamAppInert :: TyCon -> [Type] -> TcS (Maybe (Coercion, Type, CtFlavourRole))+lookupFamAppInert tc tys = do+  res <- lookupFlatCache tc tys+  pure $ case res of+    Nothing -> Nothing+    Just ( co, ty, f ) -> Just ( co, ty, (f, NomEq) )++tcSplitForAllTyVarBinders :: Type -> ([TyVarBinder], Type)+tcSplitForAllTyVarBinders = tcSplitForAllVarBndrs++#endif

@@ -1,604 +1,604 @@-{-# LANGUAGE BangPatterns #-}
-{-# LANGUAGE CPP #-}
-
-module GHC.TcPlugin.API.Internal.Shim.Reduction where
-
--- base
-import Prelude
-  hiding (Floating(cos))
-
--- ghc
-import GHC.Core.Class
-  ( Class(classTyCon) )
-import GHC.Core.Coercion
-  ( Coercion, CoercionN, MCoercion(..)
-  , Role(Nominal), LiftingContext
-#if MIN_VERSION_ghc(9,0,0)
-  , castCoercionKind1, castCoercionKind2
-  , coercionLKind, coercionRKind
-#else
-  , mkCoherenceLeftCo, mkNomReflCo
-#endif
-  , coercionKind
-#if MIN_VERSION_ghc(8,10,0)
-  , coToMCo
-#else
-  , isReflCo
-#endif
-  , decomposePiCos, downgradeRole
-  , liftCoSubst, emptyLiftingContext, extendLiftingContextAndInScope, zapLiftingContext
-  , mkAppCo, mkAppCos
-  , mkCoherenceRightCo
-  , mkForAllCo, mkFunCo
-  , mkGReflLeftCo, mkGReflRightCo
-  , mkHomoForAllCos, mkProofIrrelCo
-  , mkReflCo, mkSubCo, mkSymCo, mkTransCo, mkTyConAppCo
-  )
-import GHC.Core.Predicate
-  ( mkClassPred )
-import GHC.Core.TyCo.Rep
-  ( TyCoBinder, mkFunTy
-#if !MIN_VERSION_ghc(9,0,0)
-  , Coercion(..)
-#endif
-  )
-import GHC.Core.TyCon
-  ( TyCon )
-import GHC.Core.Type
-  ( ArgFlag, Kind, Type, TyVar, TyVarBinder
-#if MIN_VERSION_ghc(8,10,0)
-  , AnonArgFlag
-#endif
-  , binderVars
-  , mkAppTy, mkAppTys, mkCastTy, mkCoercionTy, mkForAllTy, mkForAllTys
-  , mkTyConApp, mkPiTys
-  , noFreeVarsOfType
-  , splitPiTys, tyCoBinderType, tyCoBinderVar_maybe
-  )
-import GHC.Data.Pair
-  ( Pair(Pair) )
-import GHC.Types.Var
-  ( setTyVarKind )
-import GHC.Types.Var.Env
-  ( mkInScopeSet )
-import GHC.Types.Var.Set
-  ( TyCoVarSet )
-import GHC.Utils.Outputable
-  ( Outputable(ppr), (<+>)
-  , braces, text, vcat
-  )
-
---------------------------------------------------------------------------------
-
-
--- | A 'Reduction' is the result of an operation that rewrites a type @ty_in@.
--- The 'Reduction' includes the rewritten type @ty_out@ and a 'Coercion' @co@
--- such that @co :: ty_in ~ ty_out@, where the role of the coercion is determined
--- by the context. That is, the LHS type of the coercion is the original type
--- @ty_in@, while its RHS type is the rewritten type @ty_out@.
---
--- A Reduction is always homogeneous, unless it is wrapped inside a 'HetReduction',
--- which separately stores the kind coercion.
-data Reduction =
-  Reduction
-    { reductionCoercion    :: Coercion
-    , reductionReducedType :: !Type
-    }
-
--- | Stores a heterogeneous reduction.
---
--- The stored kind coercion must relate the kinds of the
--- stored reduction. That is, in @HetReduction (Reduction co xi) kco@,
--- we must have:
---
--- >  co :: ty ~ xi
--- > kco :: typeKind ty ~ typeKind xi
-data HetReduction =
-  HetReduction
-    Reduction
-    MCoercion
-
--- | Create a heterogeneous reduction.
---
--- Pre-condition: the provided kind coercion (second argument)
--- relates the kinds of the stored reduction.
--- That is, if the coercion stored in the 'Reduction' is of the form
---
--- > co :: ty ~ xi
---
--- Then the kind coercion supplied must be of the form:
---
--- > kco :: typeKind ty ~ typeKind xi
-mkHetReduction :: Reduction  -- ^ heterogeneous reduction
-               -> MCoercion  -- ^ kind coercion
-               -> HetReduction
-mkHetReduction redn mco = HetReduction redn mco
-{-# INLINE mkHetReduction #-}
-
--- | Homogenise a heterogeneous reduction.
---
--- Given @HetReduction (Reduction co xi) kco@, with
---
--- >  co :: ty ~ xi
--- > kco :: typeKind(ty) ~ typeKind(xi)
---
--- this returns the homogeneous reduction:
---
--- > hco :: ty ~ ( xi |> sym kco )
-homogeniseHetRedn :: Role -> HetReduction -> Reduction
-homogeniseHetRedn role (HetReduction redn kco)
-  = mkCoherenceRightMRedn role redn (mkSymMCo kco)
-{-# INLINE homogeniseHetRedn #-}
-
--- | Create a 'Reduction' from a pair of a 'Coercion' and a 'Type.
---
--- Pre-condition: the RHS type of the coercion matches the provided type
--- (perhaps up to zonking).
---
--- Use 'coercionRedn' when you only have the coercion.
-mkReduction :: Coercion -> Type -> Reduction
-mkReduction co ty = Reduction co ty
-{-# INLINE mkReduction #-}
-
-instance Outputable Reduction where
-  ppr redn =
-    braces $ vcat
-      [ text "reductionOriginalType:" <+> ppr (reductionOriginalType redn)
-      , text " reductionReducedType:" <+> ppr (reductionReducedType redn)
-      , text "    reductionCoercion:" <+> ppr (reductionCoercion redn)
-      ]
-
--- | A 'Reduction' in which the 'Coercion' has 'Nominal' role.
-type ReductionN = Reduction
-
--- | A 'Reduction' in which the 'Coercion' has 'Representational' role.
-type ReductionR = Reduction
-
--- | Get the original, unreduced type corresponding to a 'Reduction'.
---
--- This is obtained by computing the LHS kind of the stored coercion,
--- which may be slow.
-reductionOriginalType :: Reduction -> Type
-reductionOriginalType = coercionLKind . reductionCoercion
-{-# INLINE reductionOriginalType #-}
-
--- | Turn a 'Coercion' into a 'Reduction'
--- by inspecting the RHS type of the coercion.
---
--- Prefer using 'mkReduction' when you already know
--- the RHS type of the coercion, to avoid computing it anew.
-coercionRedn :: Coercion -> Reduction
-coercionRedn co = Reduction co (coercionRKind co)
-{-# INLINE coercionRedn #-}
-
--- | Downgrade the role of the coercion stored in the 'Reduction'.
-downgradeRedn :: Role -- ^ desired role
-              -> Role -- ^ current role
-              -> Reduction
-              -> Reduction
-downgradeRedn new_role old_role redn@(Reduction co _)
-  = redn { reductionCoercion = downgradeRole new_role old_role co }
-{-# INLINE downgradeRedn #-}
-
--- | Downgrade the role of the coercion stored in the 'Reduction',
--- from 'Nominal' to 'Representational'.
-mkSubRedn :: Reduction -> Reduction
-mkSubRedn redn@(Reduction co _) = redn { reductionCoercion = mkSubCo co }
-{-# INLINE mkSubRedn #-}
-
--- | Compose a reduction with a coercion on the left.
---
--- Pre-condition: the provided coercion's RHS type must match the LHS type
--- of the coercion that is stored in the reduction.
-mkTransRedn :: Coercion -> Reduction -> Reduction
-mkTransRedn co1 redn@(Reduction co2 _)
-  = redn { reductionCoercion = co1 `mkTransCo` co2 }
-{-# INLINE mkTransRedn #-}
-
--- | The reflexive reduction.
-mkReflRedn :: Role -> Type -> Reduction
-mkReflRedn r ty = mkReduction (mkReflCo r ty) ty
-
--- | Create a 'Reduction' from a kind cast, in which
--- the casted type is the rewritten type.
---
--- Given @ty :: k1@, @mco :: k1 ~ k2@,
--- produces the 'Reduction' @ty ~res_co~> (ty |> mco)@
--- at the given 'Role'.
-mkGReflRightRedn :: Role -> Type -> CoercionN -> Reduction
-mkGReflRightRedn role ty co
-  = mkReduction
-      (mkGReflRightCo role ty co)
-      (mkCastTy ty co)
-{-# INLINE mkGReflRightRedn #-}
-
--- | Create a 'Reduction' from a kind cast, in which
--- the casted type is the rewritten type.
---
--- Given @ty :: k1@, @mco :: k1 ~ k2@,
--- produces the 'Reduction' @ty ~res_co~> (ty |> mco)@
--- at the given 'Role'.
-mkGReflRightMRedn :: Role -> Type -> MCoercion -> Reduction
-mkGReflRightMRedn role ty mco
-  = mkReduction
-      (mkGReflRightMCo role ty mco)
-      (mkCastTyMCo ty mco)
-{-# INLINE mkGReflRightMRedn #-}
-
--- | Create a 'Reduction' from a kind cast, in which
--- the casted type is the original (non-rewritten) type.
---
--- Given @ty :: k1@, @mco :: k1 ~ k2@,
--- produces the 'Reduction' @(ty |> mco) ~res_co~> ty@
--- at the given 'Role'.
-mkGReflLeftRedn :: Role -> Type -> CoercionN -> Reduction
-mkGReflLeftRedn role ty co
-  = mkReduction
-      (mkGReflLeftCo role ty co)
-      ty
-{-# INLINE mkGReflLeftRedn #-}
-
--- | Create a 'Reduction' from a kind cast, in which
--- the casted type is the original (non-rewritten) type.
---
--- Given @ty :: k1@, @mco :: k1 ~ k2@,
--- produces the 'Reduction' @(ty |> mco) ~res_co~> ty@
--- at the given 'Role'.
-mkGReflLeftMRedn :: Role -> Type -> MCoercion -> Reduction
-mkGReflLeftMRedn role ty mco
-  = mkReduction
-      (mkGReflLeftMCo role ty mco)
-      ty
-{-# INLINE mkGReflLeftMRedn #-}
-
--- | Apply a cast to the result of a 'Reduction'.
---
--- Given a 'Reduction' @ty1 ~co1~> (ty2 :: k2)@ and a kind coercion @kco@
--- with LHS kind @k2@, produce a new 'Reduction' @ty1 ~co2~> ( ty2 |> kco )@
--- of the given 'Role' (which must match the role of the coercion stored
--- in the 'Reduction' argument).
-mkCoherenceRightRedn :: Role -> Reduction -> CoercionN -> Reduction
-mkCoherenceRightRedn r (Reduction co1 ty2) kco
-  = mkReduction
-      (mkCoherenceRightCo r ty2 kco co1)
-      (mkCastTy ty2 kco)
-{-# INLINE mkCoherenceRightRedn #-}
-
--- | Apply a cast to the result of a 'Reduction', using an 'MCoercionN'.
---
--- Given a 'Reduction' @ty1 ~co1~> (ty2 :: k2)@ and a kind coercion @mco@
--- with LHS kind @k2@, produce a new 'Reduction' @ty1 ~co2~> ( ty2 |> mco )@
--- of the given 'Role' (which must match the role of the coercion stored
--- in the 'Reduction' argument).
-mkCoherenceRightMRedn :: Role -> Reduction -> MCoercion -> Reduction
-mkCoherenceRightMRedn r (Reduction co1 ty2) kco
-  = mkReduction
-      (mkCoherenceRightMCo r ty2 kco co1)
-      (mkCastTyMCo ty2 kco)
-{-# INLINE mkCoherenceRightMRedn #-}
-
--- | Apply a cast to a 'Reduction', casting both the original and the reduced type.
---
--- Given @cast_co@ and 'Reduction' @ty ~co~> xi@, this function returns
--- the 'Reduction' @(ty |> cast_co) ~return_co~> (xi |> cast_co)@
--- of the given 'Role' (which must match the role of the coercion stored
--- in the 'Reduction' argument).
---
--- Pre-condition: the 'Type' passed in is the same as the LHS type
--- of the coercion stored in the 'Reduction'.
-mkCastRedn1 :: Role
-            -> Type      -- ^ original type
-            -> CoercionN -- ^ coercion to cast with
-            -> Reduction -- ^ rewritten type, with rewriting coercion
-            -> Reduction
-mkCastRedn1 r ty cast_co (Reduction co xi)
-  -- co :: ty ~r ty'
-  -- return_co :: (ty |> cast_co) ~r (ty' |> cast_co)
-  = mkReduction
-      (castCoercionKind1 co r ty xi cast_co)
-      (mkCastTy xi cast_co)
-{-# INLINE mkCastRedn1 #-}
-
--- | Apply casts on both sides of a 'Reduction' (of the given 'Role').
---
--- Use 'mkCastRedn1' when you want to cast both the original and reduced types
--- in a 'Reduction' using the same coercion.
---
--- Pre-condition: the 'Type' passed in is the same as the LHS type
--- of the coercion stored in the 'Reduction'.
-mkCastRedn2 :: Role
-            -> Type      -- ^ original type
-            -> CoercionN -- ^ coercion to cast with on the left
-            -> Reduction -- ^ rewritten type, with rewriting coercion
-            -> CoercionN -- ^ coercion to cast with on the right
-            -> Reduction
-mkCastRedn2 r ty cast_co (Reduction nco nty) cast_co'
-  = mkReduction
-      (castCoercionKind2 nco r ty nty cast_co cast_co')
-      (mkCastTy nty cast_co')
-{-# INLINE mkCastRedn2 #-}
-
--- | Apply one 'Reduction' to another.
---
--- Combines 'mkAppCo' and 'mkAppTy`.
-mkAppRedn :: Reduction -> Reduction -> Reduction
-mkAppRedn (Reduction co1 ty1) (Reduction co2 ty2)
-  = mkReduction (mkAppCo co1 co2) (mkAppTy ty1 ty2)
-{-# INLINE mkAppRedn #-}
-
--- | Create a function 'Reduction'.
---
--- Combines 'mkFunCo' and 'mkFunTy'.
-mkFunRedn :: Role
-#if MIN_VERSION_ghc(8,10,0)
-          -> AnonArgFlag
-#endif
-#if MIN_VERSION_ghc(9,0,0)
-          -> ReductionN -- ^ multiplicity reduction
-#endif
-          -> Reduction  -- ^ argument reduction
-          -> Reduction  -- ^ result reduction
-          -> Reduction
-mkFunRedn r
-#if MIN_VERSION_ghc(8,10,0)
-  vis
-#endif
-#if MIN_VERSION_ghc(9,0,0)
-  (Reduction w_co w_ty)
-#endif
-  (Reduction arg_co arg_ty)
-  (Reduction res_co res_ty)
-    = mkReduction
-        ( mkFunCo
-            r
-#if MIN_VERSION_ghc(9,0,0)
-            w_co
-#endif
-            arg_co
-            res_co
-        )
-        ( mkFunTy
-#if MIN_VERSION_ghc(8,10,0)
-            vis
-#endif
-#if MIN_VERSION_ghc(9,0,0)
-            w_ty
-#endif
-            arg_ty
-            res_ty
-        )
-{-# INLINE mkFunRedn #-}
-
--- | Create a 'Reduction' associated to a Π type,
--- from a kind 'Reduction' and a body 'Reduction'.
---
--- Combines 'mkForAllCo' and 'mkForAllTy'.
-mkForAllRedn :: ArgFlag
-             -> TyVar
-             -> ReductionN -- ^ kind reduction
-             -> Reduction  -- ^ body reduction
-             -> Reduction
-mkForAllRedn vis tv1 (Reduction h ki') (Reduction co ty)
-  = mkReduction
-      (mkForAllCo tv1 h co)
-      (mkForAllTy tv2 vis ty)
-  where
-    tv2 = setTyVarKind tv1 ki'
-{-# INLINE mkForAllRedn #-}
-
--- | Create a 'Reduction' of a quantified type from a
--- 'Reduction' of the body.
---
--- Combines 'mkHomoForAllCos' and 'mkForAllTys'.
-mkHomoForAllRedn :: [TyVarBinder] -> Reduction -> Reduction
-mkHomoForAllRedn bndrs (Reduction co ty)
-  = mkReduction
-      (mkHomoForAllCos (binderVars bndrs) co)
-      (mkForAllTys bndrs ty)
-{-# INLINE mkHomoForAllRedn #-}
-
--- | Create a 'Reduction' from a coercion between coercions.
---
--- Combines 'mkProofIrrelCo' and 'mkCoercionTy'.
-mkProofIrrelRedn :: Role      -- ^ role of the created coercion, "r"
-                 -> CoercionN -- ^ co :: phi1 ~N phi2
-                 -> Coercion  -- ^ g1 :: phi1
-                 -> Coercion  -- ^ g2 :: phi2
-                 -> Reduction -- ^ res_co :: g1 ~r g2
-mkProofIrrelRedn role co g1 g2
-  = mkReduction
-      (mkProofIrrelCo role co g1 g2)
-      (mkCoercionTy g2)
-{-# INLINE mkProofIrrelRedn #-}
-
--- | Create a reflexive 'Reduction' whose RHS is the given 'Coercion',
--- with the specified 'Role'.
-mkReflCoRedn :: Role -> Coercion -> Reduction
-mkReflCoRedn role co
-  = mkReduction
-      (mkReflCo role co_ty)
-      co_ty
-  where
-    co_ty = mkCoercionTy co
-{-# INLINE mkReflCoRedn #-}
-
--- | A collection of 'Reduction's where the coercions and the types are stored separately.
---
--- Use 'unzipRedns' to obtain 'Reductions' from a list of 'Reduction's.
---
--- This datatype is used in 'mkAppRedns', 'mkClassPredRedns' and 'mkTyConAppRedn',
--- which expect separate types and coercions.
---
--- Invariant: the two stored lists are of the same length,
--- and the RHS type of each coercion is the corresponding type.
-data Reductions = Reductions [Coercion] [Type]
-
--- | Create 'Reductions' from individual lists of coercions and types.
---
--- The lists should be of the same length, and the RHS type of each coercion
--- should match the specified type in the other list.
-mkReductions :: [Coercion] -> [Type] -> Reductions
-mkReductions cos tys = Reductions cos tys
-{-# INLINE mkReductions #-}
-
--- | Combines 'mkAppCos' and 'mkAppTys'.
-mkAppRedns :: Reduction -> Reductions -> Reduction
-mkAppRedns (Reduction co ty) (Reductions cos tys)
-  = mkReduction (mkAppCos co cos) (mkAppTys ty tys)
-{-# INLINE mkAppRedns #-}
-
--- | 'TyConAppCo' for 'Reduction's: combines 'mkTyConAppCo' and `mkTyConApp`.
-mkTyConAppRedn :: Role -> TyCon -> Reductions -> Reduction
-mkTyConAppRedn role tc (Reductions cos tys)
-  = mkReduction (mkTyConAppCo role tc cos) (mkTyConApp tc tys)
-{-# INLINE mkTyConAppRedn #-}
-
--- | Reduce the arguments of a 'Class' 'TyCon'.
-mkClassPredRedn :: Class -> Reductions -> Reduction
-mkClassPredRedn cls (Reductions cos tys)
-  = mkReduction
-      (mkTyConAppCo Nominal (classTyCon cls) cos)
-      (mkClassPred cls tys)
-{-# INLINE mkClassPredRedn #-}
-
--- | Obtain 'Reductions' from a list of 'Reduction's by unzipping.
-unzipRedns :: [Reduction] -> Reductions
-unzipRedns = foldr accRedn (Reductions [] [])
-  where
-    accRedn :: Reduction -> Reductions -> Reductions
-    accRedn (Reduction co xi) (Reductions cos xis)
-      = Reductions (co:cos) (xi:xis)
-{-# INLINE unzipRedns #-}
-
---------------------------------------------------------------------------------
-
-data ArgsReductions =
-  ArgsReductions
-    {-# UNPACK #-} !Reductions
-    !MCoercion
-
-{-# INLINE simplifyArgsWorker #-}
-simplifyArgsWorker :: [TyCoBinder] -> Kind -> TyCoVarSet -> [Role] -> [Reduction] -> ArgsReductions
-simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs
-                   orig_roles orig_simplified_args
-  = go orig_lc
-       orig_ki_binders orig_inner_ki
-       orig_roles orig_simplified_args
-  where
-    orig_lc = emptyLiftingContext $ mkInScopeSet $ orig_fvs
-
-    go :: LiftingContext -> [TyCoBinder] -> Kind -> [Role] -> [Reduction] -> ArgsReductions
-    go !lc binders inner_ki _ []
-      = ArgsReductions
-          (mkReductions [] [])
-          kind_co
-      where
-        final_kind = mkPiTys binders inner_ki
-        kind_co | noFreeVarsOfType final_kind = MRefl
-                | otherwise                   = MCo $ liftCoSubst Nominal lc final_kind
-
-    go lc (binder:binders) inner_ki (role:roles) (arg_redn:arg_redns)
-      =  let !kind_co = liftCoSubst Nominal lc (tyCoBinderType binder)
-             !(Reduction casted_co casted_xi)
-                      = mkCoherenceRightRedn role arg_redn kind_co
-         -- now, extend the lifting context with the new binding
-             !new_lc | Just tv <- tyCoBinderVar_maybe binder
-                     = extendLiftingContextAndInScope lc tv casted_co
-                     | otherwise
-                     = lc
-             !(ArgsReductions (Reductions cos xis) final_kind_co)
-               = go new_lc binders inner_ki roles arg_redns
-         in ArgsReductions
-              (Reductions (casted_co:cos) (casted_xi:xis))
-              final_kind_co
-
-    -- See Note [Last case in simplifyArgsWorker]
-    go lc [] inner_ki roles arg_redns
-      = let co1 = liftCoSubst Nominal lc inner_ki
-            co1_kind              = coercionKind co1
-            unrewritten_tys       = map reductionOriginalType arg_redns
-            (arg_cos, res_co)     = decomposePiCos co1 co1_kind unrewritten_tys
-            casted_args           = zipWith3 mkCoherenceRightRedn roles arg_redns arg_cos
-            zapped_lc             = zapLiftingContext lc
-            Pair rewritten_kind _ = co1_kind
-            (bndrs, new_inner)    = splitPiTys rewritten_kind
-
-            ArgsReductions redns_out res_co_out
-              = go zapped_lc bndrs new_inner roles casted_args
-        in
-          ArgsReductions redns_out (res_co `mkTransMCoR` res_co_out)
-
-    go _ _ _ _ _ = error "simplifyArgsWorker wandered into deeper water than usual"
-
---------------------------------------------------------------------------------
-
--- | Get the reverse of an 'MCoercion'
-mkSymMCo :: MCoercion -> MCoercion
-mkSymMCo MRefl    = MRefl
-mkSymMCo (MCo co) = MCo (mkSymCo co)
-
-mkGReflLeftMCo :: Role -> Type -> MCoercion -> Coercion
-mkGReflLeftMCo r ty MRefl    = mkReflCo r ty
-mkGReflLeftMCo r ty (MCo co) = mkGReflLeftCo r ty co
-
-mkGReflRightMCo :: Role -> Type -> MCoercion -> Coercion
-mkGReflRightMCo r ty MRefl    = mkReflCo r ty
-mkGReflRightMCo r ty (MCo co) = mkGReflRightCo r ty co
-
--- | Cast a type by an 'MCoercion'
-mkCastTyMCo :: Type -> MCoercion -> Type
-mkCastTyMCo ty MRefl    = ty
-mkCastTyMCo ty (MCo co) = ty `mkCastTy` co
-
--- | Like 'mkCoherenceRightCo', but with an 'MCoercion'
-mkCoherenceRightMCo :: Role -> Type -> MCoercion -> Coercion -> Coercion
-mkCoherenceRightMCo _ _  MRefl    co2 = co2
-mkCoherenceRightMCo r ty (MCo co) co2 = mkCoherenceRightCo r ty co co2
-
-mkTransMCoR :: Coercion -> MCoercion -> MCoercion
-mkTransMCoR co1 MRefl     = coToMCo co1
-mkTransMCoR co1 (MCo co2) = MCo (mkTransCo co1 co2)
-
---------------------------------------------------------------------------------
-
-#if !MIN_VERSION_ghc(9,0,0)
-
-coercionLKind, coercionRKind :: Coercion -> Type
-coercionLKind co = case coercionKind co of { Pair lco _ -> lco }
-coercionRKind co = case coercionKind co of { Pair _ rco -> rco }
-
--- | Creates a new coercion with both of its types casted by different casts
--- @castCoercionKind2 g r t1 t2 h1 h2@, where @g :: t1 ~r t2@,
--- has type @(t1 |> h1) ~r (t2 |> h2)@.
--- @h1@ and @h2@ must be nominal.
-castCoercionKind2 :: Coercion -> Role -> Type -> Type
-                 -> CoercionN -> CoercionN -> Coercion
-castCoercionKind2 g r t1 t2 h1 h2
-  = mkCoherenceRightCo r t2 h2 (mkCoherenceLeftCo r t1 h1 g)
-
--- | @castCoercionKind1 g r t1 t2 h@ = @coercionKind g r t1 t2 h h@
--- That is, it's a specialised form of castCoercionKind, where the two
---          kind coercions are identical
--- @castCoercionKind1 g r t1 t2 h@, where @g :: t1 ~r t2@,
--- has type @(t1 |> h) ~r (t2 |> h)@.
--- @h@ must be nominal.
--- See Note [castCoercionKind1]
-castCoercionKind1 :: Coercion -> Role -> Type -> Type
-                  -> CoercionN -> Coercion
-castCoercionKind1 g r t1 t2 h
-  = case g of
-      Refl {} -> mkNomReflCo (mkCastTy t2 h)
-      GRefl _ _ mco -> case mco of
-           MRefl       -> mkReflCo r (mkCastTy t2 h)
-           MCo kind_co -> GRefl r (mkCastTy t1 h) $
-                          MCo (mkSymCo h `mkTransCo` kind_co `mkTransCo` h)
-      _ -> castCoercionKind2 g r t1 t2 h h
-#endif
-
-#if !MIN_VERSION_ghc(8,10,0)
-
-coToMCo :: Coercion -> MCoercion
-coToMCo co | isReflCo co = MRefl
-           | otherwise   = MCo co
-
-#endif
+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE CPP #-}++module GHC.TcPlugin.API.Internal.Shim.Reduction where++-- base+import Prelude+  hiding (Floating(cos))++-- ghc+import GHC.Core.Class+  ( Class(classTyCon) )+import GHC.Core.Coercion+  ( Coercion, CoercionN, MCoercion(..)+  , Role(Nominal), LiftingContext+#if MIN_VERSION_ghc(9,0,0)+  , castCoercionKind1, castCoercionKind2+  , coercionLKind, coercionRKind+#else+  , mkCoherenceLeftCo, mkNomReflCo+#endif+  , coercionKind+#if MIN_VERSION_ghc(8,10,0)+  , coToMCo+#else+  , isReflCo+#endif+  , decomposePiCos, downgradeRole+  , liftCoSubst, emptyLiftingContext, extendLiftingContextAndInScope, zapLiftingContext+  , mkAppCo, mkAppCos+  , mkCoherenceRightCo+  , mkForAllCo, mkFunCo+  , mkGReflLeftCo, mkGReflRightCo+  , mkHomoForAllCos, mkProofIrrelCo+  , mkReflCo, mkSubCo, mkSymCo, mkTransCo, mkTyConAppCo+  )+import GHC.Core.Predicate+  ( mkClassPred )+import GHC.Core.TyCo.Rep+  ( TyCoBinder, mkFunTy+#if !MIN_VERSION_ghc(9,0,0)+  , Coercion(..)+#endif+  )+import GHC.Core.TyCon+  ( TyCon )+import GHC.Core.Type+  ( ArgFlag, Kind, Type, TyVar, TyVarBinder+#if MIN_VERSION_ghc(8,10,0)+  , AnonArgFlag+#endif+  , binderVars+  , mkAppTy, mkAppTys, mkCastTy, mkCoercionTy, mkForAllTy, mkForAllTys+  , mkTyConApp, mkPiTys+  , noFreeVarsOfType+  , splitPiTys, tyCoBinderType, tyCoBinderVar_maybe+  )+import GHC.Data.Pair+  ( Pair(Pair) )+import GHC.Types.Var+  ( setTyVarKind )+import GHC.Types.Var.Env+  ( mkInScopeSet )+import GHC.Types.Var.Set+  ( TyCoVarSet )+import GHC.Utils.Outputable+  ( Outputable(ppr), (<+>)+  , braces, text, vcat+  )++--------------------------------------------------------------------------------+++-- | A 'Reduction' is the result of an operation that rewrites a type @ty_in@.+-- The 'Reduction' includes the rewritten type @ty_out@ and a 'Coercion' @co@+-- such that @co :: ty_in ~ ty_out@, where the role of the coercion is determined+-- by the context. That is, the LHS type of the coercion is the original type+-- @ty_in@, while its RHS type is the rewritten type @ty_out@.+--+-- A Reduction is always homogeneous, unless it is wrapped inside a 'HetReduction',+-- which separately stores the kind coercion.+data Reduction =+  Reduction+    { reductionCoercion    :: Coercion+    , reductionReducedType :: !Type+    }++-- | Stores a heterogeneous reduction.+--+-- The stored kind coercion must relate the kinds of the+-- stored reduction. That is, in @HetReduction (Reduction co xi) kco@,+-- we must have:+--+-- >  co :: ty ~ xi+-- > kco :: typeKind ty ~ typeKind xi+data HetReduction =+  HetReduction+    Reduction+    MCoercion++-- | Create a heterogeneous reduction.+--+-- Pre-condition: the provided kind coercion (second argument)+-- relates the kinds of the stored reduction.+-- That is, if the coercion stored in the 'Reduction' is of the form+--+-- > co :: ty ~ xi+--+-- Then the kind coercion supplied must be of the form:+--+-- > kco :: typeKind ty ~ typeKind xi+mkHetReduction :: Reduction  -- ^ heterogeneous reduction+               -> MCoercion  -- ^ kind coercion+               -> HetReduction+mkHetReduction redn mco = HetReduction redn mco+{-# INLINE mkHetReduction #-}++-- | Homogenise a heterogeneous reduction.+--+-- Given @HetReduction (Reduction co xi) kco@, with+--+-- >  co :: ty ~ xi+-- > kco :: typeKind(ty) ~ typeKind(xi)+--+-- this returns the homogeneous reduction:+--+-- > hco :: ty ~ ( xi |> sym kco )+homogeniseHetRedn :: Role -> HetReduction -> Reduction+homogeniseHetRedn role (HetReduction redn kco)+  = mkCoherenceRightMRedn role redn (mkSymMCo kco)+{-# INLINE homogeniseHetRedn #-}++-- | Create a 'Reduction' from a pair of a 'Coercion' and a 'Type.+--+-- Pre-condition: the RHS type of the coercion matches the provided type+-- (perhaps up to zonking).+--+-- Use 'coercionRedn' when you only have the coercion.+mkReduction :: Coercion -> Type -> Reduction+mkReduction co ty = Reduction co ty+{-# INLINE mkReduction #-}++instance Outputable Reduction where+  ppr redn =+    braces $ vcat+      [ text "reductionOriginalType:" <+> ppr (reductionOriginalType redn)+      , text " reductionReducedType:" <+> ppr (reductionReducedType redn)+      , text "    reductionCoercion:" <+> ppr (reductionCoercion redn)+      ]++-- | A 'Reduction' in which the 'Coercion' has 'Nominal' role.+type ReductionN = Reduction++-- | A 'Reduction' in which the 'Coercion' has 'Representational' role.+type ReductionR = Reduction++-- | Get the original, unreduced type corresponding to a 'Reduction'.+--+-- This is obtained by computing the LHS kind of the stored coercion,+-- which may be slow.+reductionOriginalType :: Reduction -> Type+reductionOriginalType = coercionLKind . reductionCoercion+{-# INLINE reductionOriginalType #-}++-- | Turn a 'Coercion' into a 'Reduction'+-- by inspecting the RHS type of the coercion.+--+-- Prefer using 'mkReduction' when you already know+-- the RHS type of the coercion, to avoid computing it anew.+coercionRedn :: Coercion -> Reduction+coercionRedn co = Reduction co (coercionRKind co)+{-# INLINE coercionRedn #-}++-- | Downgrade the role of the coercion stored in the 'Reduction'.+downgradeRedn :: Role -- ^ desired role+              -> Role -- ^ current role+              -> Reduction+              -> Reduction+downgradeRedn new_role old_role redn@(Reduction co _)+  = redn { reductionCoercion = downgradeRole new_role old_role co }+{-# INLINE downgradeRedn #-}++-- | Downgrade the role of the coercion stored in the 'Reduction',+-- from 'Nominal' to 'Representational'.+mkSubRedn :: Reduction -> Reduction+mkSubRedn redn@(Reduction co _) = redn { reductionCoercion = mkSubCo co }+{-# INLINE mkSubRedn #-}++-- | Compose a reduction with a coercion on the left.+--+-- Pre-condition: the provided coercion's RHS type must match the LHS type+-- of the coercion that is stored in the reduction.+mkTransRedn :: Coercion -> Reduction -> Reduction+mkTransRedn co1 redn@(Reduction co2 _)+  = redn { reductionCoercion = co1 `mkTransCo` co2 }+{-# INLINE mkTransRedn #-}++-- | The reflexive reduction.+mkReflRedn :: Role -> Type -> Reduction+mkReflRedn r ty = mkReduction (mkReflCo r ty) ty++-- | Create a 'Reduction' from a kind cast, in which+-- the casted type is the rewritten type.+--+-- Given @ty :: k1@, @mco :: k1 ~ k2@,+-- produces the 'Reduction' @ty ~res_co~> (ty |> mco)@+-- at the given 'Role'.+mkGReflRightRedn :: Role -> Type -> CoercionN -> Reduction+mkGReflRightRedn role ty co+  = mkReduction+      (mkGReflRightCo role ty co)+      (mkCastTy ty co)+{-# INLINE mkGReflRightRedn #-}++-- | Create a 'Reduction' from a kind cast, in which+-- the casted type is the rewritten type.+--+-- Given @ty :: k1@, @mco :: k1 ~ k2@,+-- produces the 'Reduction' @ty ~res_co~> (ty |> mco)@+-- at the given 'Role'.+mkGReflRightMRedn :: Role -> Type -> MCoercion -> Reduction+mkGReflRightMRedn role ty mco+  = mkReduction+      (mkGReflRightMCo role ty mco)+      (mkCastTyMCo ty mco)+{-# INLINE mkGReflRightMRedn #-}++-- | Create a 'Reduction' from a kind cast, in which+-- the casted type is the original (non-rewritten) type.+--+-- Given @ty :: k1@, @mco :: k1 ~ k2@,+-- produces the 'Reduction' @(ty |> mco) ~res_co~> ty@+-- at the given 'Role'.+mkGReflLeftRedn :: Role -> Type -> CoercionN -> Reduction+mkGReflLeftRedn role ty co+  = mkReduction+      (mkGReflLeftCo role ty co)+      ty+{-# INLINE mkGReflLeftRedn #-}++-- | Create a 'Reduction' from a kind cast, in which+-- the casted type is the original (non-rewritten) type.+--+-- Given @ty :: k1@, @mco :: k1 ~ k2@,+-- produces the 'Reduction' @(ty |> mco) ~res_co~> ty@+-- at the given 'Role'.+mkGReflLeftMRedn :: Role -> Type -> MCoercion -> Reduction+mkGReflLeftMRedn role ty mco+  = mkReduction+      (mkGReflLeftMCo role ty mco)+      ty+{-# INLINE mkGReflLeftMRedn #-}++-- | Apply a cast to the result of a 'Reduction'.+--+-- Given a 'Reduction' @ty1 ~co1~> (ty2 :: k2)@ and a kind coercion @kco@+-- with LHS kind @k2@, produce a new 'Reduction' @ty1 ~co2~> ( ty2 |> kco )@+-- of the given 'Role' (which must match the role of the coercion stored+-- in the 'Reduction' argument).+mkCoherenceRightRedn :: Role -> Reduction -> CoercionN -> Reduction+mkCoherenceRightRedn r (Reduction co1 ty2) kco+  = mkReduction+      (mkCoherenceRightCo r ty2 kco co1)+      (mkCastTy ty2 kco)+{-# INLINE mkCoherenceRightRedn #-}++-- | Apply a cast to the result of a 'Reduction', using an 'MCoercionN'.+--+-- Given a 'Reduction' @ty1 ~co1~> (ty2 :: k2)@ and a kind coercion @mco@+-- with LHS kind @k2@, produce a new 'Reduction' @ty1 ~co2~> ( ty2 |> mco )@+-- of the given 'Role' (which must match the role of the coercion stored+-- in the 'Reduction' argument).+mkCoherenceRightMRedn :: Role -> Reduction -> MCoercion -> Reduction+mkCoherenceRightMRedn r (Reduction co1 ty2) kco+  = mkReduction+      (mkCoherenceRightMCo r ty2 kco co1)+      (mkCastTyMCo ty2 kco)+{-# INLINE mkCoherenceRightMRedn #-}++-- | Apply a cast to a 'Reduction', casting both the original and the reduced type.+--+-- Given @cast_co@ and 'Reduction' @ty ~co~> xi@, this function returns+-- the 'Reduction' @(ty |> cast_co) ~return_co~> (xi |> cast_co)@+-- of the given 'Role' (which must match the role of the coercion stored+-- in the 'Reduction' argument).+--+-- Pre-condition: the 'Type' passed in is the same as the LHS type+-- of the coercion stored in the 'Reduction'.+mkCastRedn1 :: Role+            -> Type      -- ^ original type+            -> CoercionN -- ^ coercion to cast with+            -> Reduction -- ^ rewritten type, with rewriting coercion+            -> Reduction+mkCastRedn1 r ty cast_co (Reduction co xi)+  -- co :: ty ~r ty'+  -- return_co :: (ty |> cast_co) ~r (ty' |> cast_co)+  = mkReduction+      (castCoercionKind1 co r ty xi cast_co)+      (mkCastTy xi cast_co)+{-# INLINE mkCastRedn1 #-}++-- | Apply casts on both sides of a 'Reduction' (of the given 'Role').+--+-- Use 'mkCastRedn1' when you want to cast both the original and reduced types+-- in a 'Reduction' using the same coercion.+--+-- Pre-condition: the 'Type' passed in is the same as the LHS type+-- of the coercion stored in the 'Reduction'.+mkCastRedn2 :: Role+            -> Type      -- ^ original type+            -> CoercionN -- ^ coercion to cast with on the left+            -> Reduction -- ^ rewritten type, with rewriting coercion+            -> CoercionN -- ^ coercion to cast with on the right+            -> Reduction+mkCastRedn2 r ty cast_co (Reduction nco nty) cast_co'+  = mkReduction+      (castCoercionKind2 nco r ty nty cast_co cast_co')+      (mkCastTy nty cast_co')+{-# INLINE mkCastRedn2 #-}++-- | Apply one 'Reduction' to another.+--+-- Combines 'mkAppCo' and 'mkAppTy`.+mkAppRedn :: Reduction -> Reduction -> Reduction+mkAppRedn (Reduction co1 ty1) (Reduction co2 ty2)+  = mkReduction (mkAppCo co1 co2) (mkAppTy ty1 ty2)+{-# INLINE mkAppRedn #-}++-- | Create a function 'Reduction'.+--+-- Combines 'mkFunCo' and 'mkFunTy'.+mkFunRedn :: Role+#if MIN_VERSION_ghc(8,10,0)+          -> AnonArgFlag+#endif+#if MIN_VERSION_ghc(9,0,0)+          -> ReductionN -- ^ multiplicity reduction+#endif+          -> Reduction  -- ^ argument reduction+          -> Reduction  -- ^ result reduction+          -> Reduction+mkFunRedn r+#if MIN_VERSION_ghc(8,10,0)+  vis+#endif+#if MIN_VERSION_ghc(9,0,0)+  (Reduction w_co w_ty)+#endif+  (Reduction arg_co arg_ty)+  (Reduction res_co res_ty)+    = mkReduction+        ( mkFunCo+            r+#if MIN_VERSION_ghc(9,0,0)+            w_co+#endif+            arg_co+            res_co+        )+        ( mkFunTy+#if MIN_VERSION_ghc(8,10,0)+            vis+#endif+#if MIN_VERSION_ghc(9,0,0)+            w_ty+#endif+            arg_ty+            res_ty+        )+{-# INLINE mkFunRedn #-}++-- | Create a 'Reduction' associated to a Π type,+-- from a kind 'Reduction' and a body 'Reduction'.+--+-- Combines 'mkForAllCo' and 'mkForAllTy'.+mkForAllRedn :: ArgFlag+             -> TyVar+             -> ReductionN -- ^ kind reduction+             -> Reduction  -- ^ body reduction+             -> Reduction+mkForAllRedn vis tv1 (Reduction h ki') (Reduction co ty)+  = mkReduction+      (mkForAllCo tv1 h co)+      (mkForAllTy tv2 vis ty)+  where+    tv2 = setTyVarKind tv1 ki'+{-# INLINE mkForAllRedn #-}++-- | Create a 'Reduction' of a quantified type from a+-- 'Reduction' of the body.+--+-- Combines 'mkHomoForAllCos' and 'mkForAllTys'.+mkHomoForAllRedn :: [TyVarBinder] -> Reduction -> Reduction+mkHomoForAllRedn bndrs (Reduction co ty)+  = mkReduction+      (mkHomoForAllCos (binderVars bndrs) co)+      (mkForAllTys bndrs ty)+{-# INLINE mkHomoForAllRedn #-}++-- | Create a 'Reduction' from a coercion between coercions.+--+-- Combines 'mkProofIrrelCo' and 'mkCoercionTy'.+mkProofIrrelRedn :: Role      -- ^ role of the created coercion, "r"+                 -> CoercionN -- ^ co :: phi1 ~N phi2+                 -> Coercion  -- ^ g1 :: phi1+                 -> Coercion  -- ^ g2 :: phi2+                 -> Reduction -- ^ res_co :: g1 ~r g2+mkProofIrrelRedn role co g1 g2+  = mkReduction+      (mkProofIrrelCo role co g1 g2)+      (mkCoercionTy g2)+{-# INLINE mkProofIrrelRedn #-}++-- | Create a reflexive 'Reduction' whose RHS is the given 'Coercion',+-- with the specified 'Role'.+mkReflCoRedn :: Role -> Coercion -> Reduction+mkReflCoRedn role co+  = mkReduction+      (mkReflCo role co_ty)+      co_ty+  where+    co_ty = mkCoercionTy co+{-# INLINE mkReflCoRedn #-}++-- | A collection of 'Reduction's where the coercions and the types are stored separately.+--+-- Use 'unzipRedns' to obtain 'Reductions' from a list of 'Reduction's.+--+-- This datatype is used in 'mkAppRedns', 'mkClassPredRedns' and 'mkTyConAppRedn',+-- which expect separate types and coercions.+--+-- Invariant: the two stored lists are of the same length,+-- and the RHS type of each coercion is the corresponding type.+data Reductions = Reductions [Coercion] [Type]++-- | Create 'Reductions' from individual lists of coercions and types.+--+-- The lists should be of the same length, and the RHS type of each coercion+-- should match the specified type in the other list.+mkReductions :: [Coercion] -> [Type] -> Reductions+mkReductions cos tys = Reductions cos tys+{-# INLINE mkReductions #-}++-- | Combines 'mkAppCos' and 'mkAppTys'.+mkAppRedns :: Reduction -> Reductions -> Reduction+mkAppRedns (Reduction co ty) (Reductions cos tys)+  = mkReduction (mkAppCos co cos) (mkAppTys ty tys)+{-# INLINE mkAppRedns #-}++-- | 'TyConAppCo' for 'Reduction's: combines 'mkTyConAppCo' and `mkTyConApp`.+mkTyConAppRedn :: Role -> TyCon -> Reductions -> Reduction+mkTyConAppRedn role tc (Reductions cos tys)+  = mkReduction (mkTyConAppCo role tc cos) (mkTyConApp tc tys)+{-# INLINE mkTyConAppRedn #-}++-- | Reduce the arguments of a 'Class' 'TyCon'.+mkClassPredRedn :: Class -> Reductions -> Reduction+mkClassPredRedn cls (Reductions cos tys)+  = mkReduction+      (mkTyConAppCo Nominal (classTyCon cls) cos)+      (mkClassPred cls tys)+{-# INLINE mkClassPredRedn #-}++-- | Obtain 'Reductions' from a list of 'Reduction's by unzipping.+unzipRedns :: [Reduction] -> Reductions+unzipRedns = foldr accRedn (Reductions [] [])+  where+    accRedn :: Reduction -> Reductions -> Reductions+    accRedn (Reduction co xi) (Reductions cos xis)+      = Reductions (co:cos) (xi:xis)+{-# INLINE unzipRedns #-}++--------------------------------------------------------------------------------++data ArgsReductions =+  ArgsReductions+    {-# UNPACK #-} !Reductions+    !MCoercion++{-# INLINE simplifyArgsWorker #-}+simplifyArgsWorker :: [TyCoBinder] -> Kind -> TyCoVarSet -> [Role] -> [Reduction] -> ArgsReductions+simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs+                   orig_roles orig_simplified_args+  = go orig_lc+       orig_ki_binders orig_inner_ki+       orig_roles orig_simplified_args+  where+    orig_lc = emptyLiftingContext $ mkInScopeSet $ orig_fvs++    go :: LiftingContext -> [TyCoBinder] -> Kind -> [Role] -> [Reduction] -> ArgsReductions+    go !lc binders inner_ki _ []+      = ArgsReductions+          (mkReductions [] [])+          kind_co+      where+        final_kind = mkPiTys binders inner_ki+        kind_co | noFreeVarsOfType final_kind = MRefl+                | otherwise                   = MCo $ liftCoSubst Nominal lc final_kind++    go lc (binder:binders) inner_ki (role:roles) (arg_redn:arg_redns)+      =  let !kind_co = liftCoSubst Nominal lc (tyCoBinderType binder)+             !(Reduction casted_co casted_xi)+                      = mkCoherenceRightRedn role arg_redn kind_co+         -- now, extend the lifting context with the new binding+             !new_lc | Just tv <- tyCoBinderVar_maybe binder+                     = extendLiftingContextAndInScope lc tv casted_co+                     | otherwise+                     = lc+             !(ArgsReductions (Reductions cos xis) final_kind_co)+               = go new_lc binders inner_ki roles arg_redns+         in ArgsReductions+              (Reductions (casted_co:cos) (casted_xi:xis))+              final_kind_co++    -- See Note [Last case in simplifyArgsWorker]+    go lc [] inner_ki roles arg_redns+      = let co1 = liftCoSubst Nominal lc inner_ki+            co1_kind              = coercionKind co1+            unrewritten_tys       = map reductionOriginalType arg_redns+            (arg_cos, res_co)     = decomposePiCos co1 co1_kind unrewritten_tys+            casted_args           = zipWith3 mkCoherenceRightRedn roles arg_redns arg_cos+            zapped_lc             = zapLiftingContext lc+            Pair rewritten_kind _ = co1_kind+            (bndrs, new_inner)    = splitPiTys rewritten_kind++            ArgsReductions redns_out res_co_out+              = go zapped_lc bndrs new_inner roles casted_args+        in+          ArgsReductions redns_out (res_co `mkTransMCoR` res_co_out)++    go _ _ _ _ _ = error "simplifyArgsWorker wandered into deeper water than usual"++--------------------------------------------------------------------------------++-- | Get the reverse of an 'MCoercion'+mkSymMCo :: MCoercion -> MCoercion+mkSymMCo MRefl    = MRefl+mkSymMCo (MCo co) = MCo (mkSymCo co)++mkGReflLeftMCo :: Role -> Type -> MCoercion -> Coercion+mkGReflLeftMCo r ty MRefl    = mkReflCo r ty+mkGReflLeftMCo r ty (MCo co) = mkGReflLeftCo r ty co++mkGReflRightMCo :: Role -> Type -> MCoercion -> Coercion+mkGReflRightMCo r ty MRefl    = mkReflCo r ty+mkGReflRightMCo r ty (MCo co) = mkGReflRightCo r ty co++-- | Cast a type by an 'MCoercion'+mkCastTyMCo :: Type -> MCoercion -> Type+mkCastTyMCo ty MRefl    = ty+mkCastTyMCo ty (MCo co) = ty `mkCastTy` co++-- | Like 'mkCoherenceRightCo', but with an 'MCoercion'+mkCoherenceRightMCo :: Role -> Type -> MCoercion -> Coercion -> Coercion+mkCoherenceRightMCo _ _  MRefl    co2 = co2+mkCoherenceRightMCo r ty (MCo co) co2 = mkCoherenceRightCo r ty co co2++mkTransMCoR :: Coercion -> MCoercion -> MCoercion+mkTransMCoR co1 MRefl     = coToMCo co1+mkTransMCoR co1 (MCo co2) = MCo (mkTransCo co1 co2)++--------------------------------------------------------------------------------++#if !MIN_VERSION_ghc(9,0,0)++coercionLKind, coercionRKind :: Coercion -> Type+coercionLKind co = case coercionKind co of { Pair lco _ -> lco }+coercionRKind co = case coercionKind co of { Pair _ rco -> rco }++-- | Creates a new coercion with both of its types casted by different casts+-- @castCoercionKind2 g r t1 t2 h1 h2@, where @g :: t1 ~r t2@,+-- has type @(t1 |> h1) ~r (t2 |> h2)@.+-- @h1@ and @h2@ must be nominal.+castCoercionKind2 :: Coercion -> Role -> Type -> Type+                 -> CoercionN -> CoercionN -> Coercion+castCoercionKind2 g r t1 t2 h1 h2+  = mkCoherenceRightCo r t2 h2 (mkCoherenceLeftCo r t1 h1 g)++-- | @castCoercionKind1 g r t1 t2 h@ = @coercionKind g r t1 t2 h h@+-- That is, it's a specialised form of castCoercionKind, where the two+--          kind coercions are identical+-- @castCoercionKind1 g r t1 t2 h@, where @g :: t1 ~r t2@,+-- has type @(t1 |> h) ~r (t2 |> h)@.+-- @h@ must be nominal.+-- See Note [castCoercionKind1]+castCoercionKind1 :: Coercion -> Role -> Type -> Type+                  -> CoercionN -> Coercion+castCoercionKind1 g r t1 t2 h+  = case g of+      Refl {} -> mkNomReflCo (mkCastTy t2 h)+      GRefl _ _ mco -> case mco of+           MRefl       -> mkReflCo r (mkCastTy t2 h)+           MCo kind_co -> GRefl r (mkCastTy t1 h) $+                          MCo (mkSymCo h `mkTransCo` kind_co `mkTransCo` h)+      _ -> castCoercionKind2 g r t1 t2 h h+#endif++#if !MIN_VERSION_ghc(8,10,0)++coToMCo :: Coercion -> MCoercion+coToMCo co | isReflCo co = MRefl+           | otherwise   = MCo co++#endif

@@ -1,494 +1,494 @@-{-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE DerivingStrategies #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE GeneralisedNewtypeDeriving #-}
-{-# LANGUAGE InstanceSigs #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE QuantifiedConstraints #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE UndecidableInstances #-}
-
-#if MIN_VERSION_ghc(9,0,0)
-{-# LANGUAGE StandaloneKindSignatures #-}
-#endif
-
-{-|
-Module: GHC.TcPlugin.API.Names
-
-This module provides an /optional/ framework that facilitates name lookup
-in type-checking plugins, using constrained traversals (similar to the
-<https://hackage.haskell.org/package/barbies barbies library>).
-
-See the 'ResolveNames' typeclass.
-
-Before:
-
-> data PluginDefs =
->   PluginDefs
->     { myTyCon           :: TyCon
->     , myClass           :: Class
->     , myPromotedDataCon :: TyCon
->     }
->
-> findMyModule :: MonadTcPlugin m => m Module
-> findMyModule = do
->   findResult <- findImportedModule ( mkModuleName "MyModule" ) Nothing
->   case findResult of
->     Found _ res -> pure res
->     _           -> error $ "MyPlugin: could not find any module named MyModule."
->
-> pluginInit :: TcPluginM Init PluginDefs
-> pluginInit = do
->   myModule <- findMyModule
->   myTyCon           <-                       tcLookupTyCon   =<< lookupOrig myModule ( mkTcOcc   "MyTyCon"   )
->   myClass           <-                       tcLookupClass   =<< lookupOrig myModule ( mkClsOcc  "MyClass"   )
->   myPromotedDataCon <- fmap promoteDataCon . tcLookupDataCon =<< lookupOrig myModule ( mkDataOcc "MyDataCon" )
->   pure ( PluginDefs { .. } )
-
-After:
-
-> data PluginDefsHKD n =
->   PluginDefs
->     { myTyCon            :: Wear n TyCon
->     , myClass            :: Wear n Class
->     , myPromotedDataCon  :: Wear n ( Promoted DataCon )
->     }
->   deriving stock Generic
->   deriving ResolveNames
->     via Generically1 PluginDefsHKD
->
-> type PluginDefs = PluginDefsHKD Resolved
->
-> pluginInit :: TcPluginM Init PluginDefs
-> pluginInit = resolveNames pluginNames
->   where
->     pluginNames :: PluginDefsHKD Named
->     pluginNames =
->       PluginDefs
->         { myTyCon           = mkQualified "MyTyCon"
->         , myClass           = mkQualified "MyClass"
->         , myPromotedDataCon = mkQualified "MyDataCon"
->         }
->     mkQualified :: String -> QualifiedName thing
->     mkQualified str =
->       Qualified
->         { name    = str
->         , module' = mkModuleName "MyModule"
->         , package = Nothing
->         }
-
--}
-
-module GHC.TcPlugin.API.Names
-  ( ResolveNames, resolveNames
-  , Wear, QualifiedName(..), NameResolution(..)
-  , Promoted
-  , Lookupable(..)
-
-    -- * Re-export Generically1 for compatibility.
-  , Generically1(..)
-  ) where
-
--- base
-import Prelude
-  hiding ( lookup )
-import Data.Coerce
-  ( Coercible, coerce )
-import Data.Kind
-  ( Type, Constraint )
-import GHC.Generics
-  ( Generic(..)
-#if MIN_VERSION_base(4,17,0)
-  , Generically1(..)
-#endif
-  , (:+:)(..), (:*:)(..)
-  , K1(K1), M1(M1), U1(..), V1, Rec0
-  )
-import GHC.TypeLits
-  ( TypeError, ErrorMessage(..) )
-
--- transformers
-import Control.Monad.Trans.State.Strict
-  ( StateT, evalStateT, get, put )
-import Control.Monad.Trans.Class
-  ( MonadTrans(lift) )
-
--- ghc
-#if MIN_VERSION_ghc(9,3,0)
-import GHC.Iface.Errors
-  ( cannotFindModule )
-#elif MIN_VERSION_ghc(9,2,0)
-import GHC.Iface.Load
-  ( cannotFindModule )
-#else
-import GHC.Driver.Types
-  ( hsc_dflags )
-import GHC.Driver.Finder
-  ( cannotFindModule )
-import GHC.Driver.Session
-  ( DynFlags )
-#endif
-#if MIN_VERSION_ghc(9,5,0)
-import Language.Haskell.Syntax.Module.Name
-  ( moduleNameString )
-#else
-import GHC.Unit.Module.Name
-  ( moduleNameString )
-#endif
-import GHC.Unit.Types
-  ( unitIdString )
-import GHC.Utils.Panic
-  ( pgmErrorDoc )
-import GHC.Tc.Plugin
-  ( getTopEnv )
-import GHC.Types.Unique.FM
-  ( addToUFM, addToUFM_C, lookupUFM, plusUFM, unitUFM )
-
--- ghc-tcplugin-api
-import GHC.TcPlugin.API
-  hiding ( Type )
-import GHC.TcPlugin.API.Internal
-  ( MonadTcPlugin(liftTcPluginM) )
-
---------------------------------------------------------------------------------
-
--- | A 'QualifiedName' is the name of something,
--- together with the names of the module and package it comes from.
-data QualifiedName (thing :: Type)
-  = Qualified
-    { -- | Name of the thing (e.g. name of the 'TyCon' or 'Class').
-      name    :: String
-      -- | Name of the module in which the thing can be found.
-    , module' :: ModuleName
-      -- | Name of the package in which the module can be found.
-    , package :: PkgQual
-    }
-
--- | Type-level parameter to 'Wear' type family, for higher-kinded data.
---
--- @Wear Named thing@ is the identifier data passed in as an argument.
--- @Wear Resolved thing@ is the result of name resolving the thing.
---
--- This allows users to pass a record of names, of type @MyData Named@,
--- and obtain a record of looked-up things, of type @MyData Resolved@.
---
--- Refer to 'ResolveNames' for a worked example.
-data NameResolution = Named | Resolved
-
--- | Use this to refer to a @Promoted DataCon@.
-data Promoted (thing :: k) :: Type
-
--- | Type-family used for higher-kinded data pattern.
---
--- This allows the same record to be re-used,
--- as explained in the worked example for 'ResolveNames'.
---
--- For instance, if one defines:
---
--- > data MyData n
--- >   = MyData
--- >   { myClass :: !( Wear n Class )
--- >   , myTyCon :: !( Wear n TyCon )
--- >   }
---
--- then a record of type @MyData Named@ is simply a record of textual names
--- (a typeclass name and a type-constructor name, with associated module & packages),
--- whereas a record of type @MyData Resolved@ contains a typeclass's @Class@
--- as well as a type-constructor's @TyCon@.
-#if MIN_VERSION_ghc(9,0,0)
-type Wear :: forall k. NameResolution -> k -> Type
-#endif
-type family Wear (n :: NameResolution) (thing :: k) :: Type where
-#if MIN_VERSION_ghc(9,0,0)
-  Wear @Type Named thing           = QualifiedName thing
-#else
-  Wear Named thing                 = QualifiedName thing
-#endif
-  Wear Resolved (Promoted DataCon) = TyCon
-  Wear Resolved (Promoted a)
-    = TypeError
-      ( Text "Cannot promote " :<>: ShowType a :<>: Text "."
-      :$$: Text "Can only promote 'DataCon's."
-      )
-  Wear Resolved thing = thing
-
--- | Retrieve the underlying thing being referred to by inspecting
--- the type parameter of 'QualifiedName'.
-type family UnwearNamed (loc :: Type) :: Type where
-  UnwearNamed (QualifiedName thing) = thing
-
--- | Type-class overloading things that can be looked up by name:
---
--- * classes,
--- * data constructors (as well as their promotion),
--- * type-constructors.
-#if MIN_VERSION_ghc(9,0,0)
-type Lookupable :: forall {k}. k -> Constraint
-#endif
-class Lookupable (a :: k) where
-  mkOccName :: String -> OccName
-  lookup :: MonadTcPlugin m => Name -> m (Wear Resolved a)
-
-instance Lookupable TyCon where
-  mkOccName = mkTcOcc
-  lookup = tcLookupTyCon
-instance Lookupable DataCon where
-  mkOccName = mkDataOcc
-  lookup = tcLookupDataCon
-instance Lookupable Class where
-  mkOccName = mkClsOcc
-  lookup = tcLookupClass
-instance Lookupable (Promoted DataCon) where
-  mkOccName = mkDataOcc
-  lookup = fmap promoteDataCon . tcLookupDataCon
-
--- | This class exposes the method 'resolveNames' which will
--- perform name resolution for all the fields in a datatype.
---
--- Example usage: we define a record that will hold
--- the things we want to look up, using the 'Wear' type family.
---
--- For example:
---
---  > data MyData n
---  >   = MyData
---  >   { myClass       :: !( Wear n Class )
---  >   , myTyCon       :: !( Wear n TyCon )
---  >   , myDataCon     :: !( Wear n DataCon )
---  >   , myPromDataCon :: !( Wear n (Promoted DataCon) )
---  >   }
---  >   deriving stock Generic
---  >   deriving ResolveNames
---  >     via Generically1 MyData
---
--- Now we can specify the names of the things which we want to look up,
--- together with the modules and packages in which they belong:
---
--- > myNames :: MyData Named
--- > myNames = MyData
--- >  { myClass = QualifiedName "MyClass" "My.Module" ( Just "my-pkg-name" )
--- >  , ...
--- >  }
---
--- Then we can call 'resolveNames':
---
--- > resolvedNames :: MonadTcPlugin m => m (MyData Resolved)
--- > resolvedNames = resolveNames myNames
---
--- This returns a record containing the looked up things we want,
--- e.g. @myClass :: Class@, @myPromDataCon :: TyCon@, etc.
-class ResolveNames (f :: NameResolution -> Type) where
-  resolve_names :: ( Coercible res ( f Resolved ), MonadTcPlugin m )
-                => f Named -> m res
-  -- Workaround: the result is anything coercible to "f Resolved" rather than just "f Resolved",
-  -- because otherwise GHC complains when using DerivingVia that we don't know the role
-  -- of the parameter to m, despite the quantified constraint superclass to MonadTcPlugin.
-  --
-  -- This unfortunately worsens type-inference, so we export
-  -- 'resolveNames' separately.
-
--- | Resolve a collection of names.
---
--- See 'ResolveNames' for further details.
-resolveNames :: ( MonadTcPlugin m, ResolveNames f )
-             => f Named -> m ( f Resolved )
-resolveNames = resolve_names
-
-instance ( Generic (f Named)
-         , Generic (f Resolved)
-         , GTraversableC ResolveName (Rep (f Named)) (Rep (f Resolved))
-         )
-      => ResolveNames (Generically1 f) where
-  resolve_names
-    :: forall
-#if MIN_VERSION_ghc(9,0,0)
-         {m}
-#else
-          m
-#endif
-         res
-    .  ( Coercible res ( Generically1 f Resolved ), MonadTcPlugin m )
-    => Generically1 f Named -> m res
-  resolve_names ( Generically1 dat )
-    =  ( `evalStateT` emptyModules )
-    $  coerce . to @(f Resolved)
-   <$> gtraverseC @ResolveName resolveName ( from dat )
-
--- | Type-class dispatch for looking up names.
---
--- Every instance is of the form:
---
--- > ResolveName (Wear Named thing) (Wear Resolved thing)
---
--- which allows one to write 'resolveName':
---
--- > resolveName :: ... => Wear Named thing -> m ( Wear Resolved thing )
-class    ( a ~ Wear Named    ( UnwearNamed a )
-         , b ~ Wear Resolved ( UnwearNamed a )
-         , Lookupable ( UnwearNamed a )
-         )
-      => ResolveName (a :: Type) (b :: Type)
-instance ( a ~ Wear Named    ( UnwearNamed a )
-         , b ~ Wear Resolved ( UnwearNamed a )
-         , Lookupable ( UnwearNamed a )
-         )
-      => ResolveName a b
-
-resolveName :: forall (thing :: Type) m
-            .  ResolveName ( Wear Named thing ) ( Wear Resolved thing )
-            => MonadTcPlugin m
-            => Wear Named thing
-            -> StateT ImportedModules m ( Wear Resolved thing )
-resolveName (Qualified str mod_name pkg) = do
-  md <- lookupModule pkg mod_name
-  nm <- lift $ lookupOrig md
-                 (mkOccName
-#if !MIN_VERSION_ghc(9,0,0)
-                   @_
-#endif
-                   @thing
-                   str
-                 )
-  lift $ lookup
-#if !MIN_VERSION_ghc(9,0,0)
-           @_
-#endif
-           @thing nm
-
---------------------------------------------------------------------------------
--- Caching of found modules.
-
-data ImportedModules
-  = ImportedModules
-    { home_modules      :: UniqFM ModuleName Module
-    , this_pkg_modules  :: UniqFM UnitId ( UniqFM ModuleName Module )
-    , other_pkg_modules :: UniqFM UnitId ( UniqFM ModuleName Module )
-    }
-
-emptyModules :: ImportedModules
-emptyModules =
-  ImportedModules
-    { home_modules      = emptyUFM
-    , this_pkg_modules  = emptyUFM
-    , other_pkg_modules = emptyUFM
-    }
-
-lookupCachedModule :: Monad m => PkgQual -> ModuleName -> StateT ImportedModules m (Maybe Module)
-lookupCachedModule NoPkgQual    mod_name
-  =   ( `lookupUFM` mod_name )
-  .   home_modules
-  <$> get
-lookupCachedModule (ThisPkg pkg) mod_name
-  =   ( ( `lookupUFM` mod_name ) =<< )
-  .   ( `lookupUFM` pkg )
-  .   this_pkg_modules
-  <$> get
-lookupCachedModule (OtherPkg pkg) mod_name
-  =   ( ( `lookupUFM` mod_name ) =<< )
-  .   ( `lookupUFM` pkg )
-  .   other_pkg_modules
-  <$> get
-
-insertCachedModule :: Monad m => PkgQual -> ModuleName -> Module -> StateT ImportedModules m ()
-insertCachedModule NoPkgQual    mod_name md = do
-  mods@( ImportedModules { home_modules = prev } ) <- get
-  put $ mods { home_modules = addToUFM prev mod_name md }
-insertCachedModule (ThisPkg pkg) mod_name md = do
-  mods@( ImportedModules { this_pkg_modules = prev } ) <- get
-  put $ mods { this_pkg_modules = addToUFM_C plusUFM prev pkg (unitUFM mod_name md) }
-insertCachedModule (OtherPkg pkg) mod_name md = do
-  mods@( ImportedModules { other_pkg_modules = prev } ) <- get
-  put $ mods { other_pkg_modules = addToUFM_C plusUFM prev pkg (unitUFM mod_name md) }
-
-lookupModule :: MonadTcPlugin m => PkgQual -> ModuleName -> StateT ImportedModules m Module
-lookupModule pkg mod_name = do
-  cachedResult <- lookupCachedModule pkg mod_name
-  case cachedResult of
-    Just res -> do
-      insertCachedModule pkg mod_name res
-      pure res
-    Nothing -> do
-      findResult <- lift $ findImportedModule mod_name pkg
-      case findResult of
-        Found _ res
-          -> pure res
-        other -> do
-          hsc_env <- lift . liftTcPluginM $ getTopEnv
-          let
-            err_doc :: SDoc
-#if MIN_VERSION_ghc(9,2,0)
-            err_doc = cannotFindModule hsc_env mod_name other
-#else
-            err_doc = cannotFindModule dflags  mod_name other
-            dflags :: DynFlags
-            dflags = hsc_dflags hsc_env
-#endif
-          pgmErrorDoc
-            ( "GHC.TcPlugin.API: could not find module " <> mod_str <> " in " <> pkg_name )
-            err_doc
-  where
-    pkg_name, mod_str :: String
-    pkg_name = case pkg of
-      NoPkgQual     -> "home package"
-      ThisPkg unit  -> "home-unit package " <> unitIdString unit
-      OtherPkg unit -> "other unit package" <> unitIdString unit
-    mod_str = moduleNameString mod_name
-
---------------------------------------------------------------------------------
--- Constrained traversals.
-
-type TraversalC (c :: Type -> Type -> Constraint) (s :: Type)  (t :: Type)
-  =  forall f. ( Applicative f )
-  => ( forall a b. c a b => a -> f b ) -> s -> f t
-
-class GTraversableC (c :: Type -> Type -> Constraint) (s :: Type -> Type) (t :: Type -> Type) where
-  gtraverseC :: TraversalC c (s x) (t x)
-
-instance
-  ( GTraversableC c l l'
-  , GTraversableC c r r'
-  ) => GTraversableC c (l :*: r) (l' :*: r') where
-  gtraverseC f (l :*: r)
-    = (:*:) <$> gtraverseC @c f l <*> gtraverseC @c f r
-
-instance
-  ( GTraversableC c l l'
-  , GTraversableC c r r'
-  ) => GTraversableC c (l :+: r) (l' :+: r') where
-  gtraverseC f (L1 l) = L1 <$> gtraverseC @c f l
-  gtraverseC f (R1 r) = R1 <$> gtraverseC @c f r
-
-instance GTraversableC c s t
-  => GTraversableC c (M1 i m s) (M1 i m t) where
-  gtraverseC f (M1 x) = M1 <$> gtraverseC @c f x
-
-instance GTraversableC c U1 U1 where
-  gtraverseC _ _ = pure U1
-
-instance GTraversableC c V1 V1 where
-  gtraverseC _ = pure
-
-instance c a b => GTraversableC c (Rec0 a) (Rec0 b) where
-  gtraverseC f (K1 a) = K1 <$> f a
-
---------------------------------------------------------------------------------
--- Generically and Generically1 wrappers for DerivingVia.
-
-#if !MIN_VERSION_base(4,17,0)
--- | A type whose instances are defined generically, using the
--- 'Generic1' representation. 'Generically1' is a higher-kinded
--- version of 'Generically' that uses 'Generic'.
---
--- Generic instances can be derived for type constructors via
--- @'Generically1' F@ using @-XDerivingVia@.
-newtype Generically1 (f :: k -> Type) (a :: k) = Generically1 ( f a )
-#endif
+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralisedNewtypeDeriving #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}++#if MIN_VERSION_ghc(9,0,0)+{-# LANGUAGE StandaloneKindSignatures #-}+#endif++{-|+Module: GHC.TcPlugin.API.Names++This module provides an /optional/ framework that facilitates name lookup+in type-checking plugins, using constrained traversals (similar to the+<https://hackage.haskell.org/package/barbies barbies library>).++See the 'ResolveNames' typeclass.++Before:++> data PluginDefs =+>   PluginDefs+>     { myTyCon           :: TyCon+>     , myClass           :: Class+>     , myPromotedDataCon :: TyCon+>     }+>+> findMyModule :: MonadTcPlugin m => m Module+> findMyModule = do+>   findResult <- findImportedModule ( mkModuleName "MyModule" ) Nothing+>   case findResult of+>     Found _ res -> pure res+>     _           -> error $ "MyPlugin: could not find any module named MyModule."+>+> pluginInit :: TcPluginM Init PluginDefs+> pluginInit = do+>   myModule <- findMyModule+>   myTyCon           <-                       tcLookupTyCon   =<< lookupOrig myModule ( mkTcOcc   "MyTyCon"   )+>   myClass           <-                       tcLookupClass   =<< lookupOrig myModule ( mkClsOcc  "MyClass"   )+>   myPromotedDataCon <- fmap promoteDataCon . tcLookupDataCon =<< lookupOrig myModule ( mkDataOcc "MyDataCon" )+>   pure ( PluginDefs { .. } )++After:++> data PluginDefsHKD n =+>   PluginDefs+>     { myTyCon            :: Wear n TyCon+>     , myClass            :: Wear n Class+>     , myPromotedDataCon  :: Wear n ( Promoted DataCon )+>     }+>   deriving stock Generic+>   deriving ResolveNames+>     via Generically1 PluginDefsHKD+>+> type PluginDefs = PluginDefsHKD Resolved+>+> pluginInit :: TcPluginM Init PluginDefs+> pluginInit = resolveNames pluginNames+>   where+>     pluginNames :: PluginDefsHKD Named+>     pluginNames =+>       PluginDefs+>         { myTyCon           = mkQualified "MyTyCon"+>         , myClass           = mkQualified "MyClass"+>         , myPromotedDataCon = mkQualified "MyDataCon"+>         }+>     mkQualified :: String -> QualifiedName thing+>     mkQualified str =+>       Qualified+>         { name    = str+>         , module' = mkModuleName "MyModule"+>         , package = Nothing+>         }++-}++module GHC.TcPlugin.API.Names+  ( ResolveNames, resolveNames+  , Wear, QualifiedName(..), NameResolution(..)+  , Promoted+  , Lookupable(..)++    -- * Re-export Generically1 for compatibility.+  , Generically1(..)+  ) where++-- base+import Prelude+  hiding ( lookup )+import Data.Coerce+  ( Coercible, coerce )+import Data.Kind+  ( Type, Constraint )+import GHC.Generics+  ( Generic(..)+#if MIN_VERSION_base(4,17,0)+  , Generically1(..)+#endif+  , (:+:)(..), (:*:)(..)+  , K1(K1), M1(M1), U1(..), V1, Rec0+  )+import GHC.TypeLits+  ( TypeError, ErrorMessage(..) )++-- transformers+import Control.Monad.Trans.State.Strict+  ( StateT, evalStateT, get, put )+import Control.Monad.Trans.Class+  ( MonadTrans(lift) )++-- ghc+#if MIN_VERSION_ghc(9,3,0)+import GHC.Iface.Errors+  ( cannotFindModule )+#elif MIN_VERSION_ghc(9,2,0)+import GHC.Iface.Load+  ( cannotFindModule )+#else+import GHC.Driver.Types+  ( hsc_dflags )+import GHC.Driver.Finder+  ( cannotFindModule )+import GHC.Driver.Session+  ( DynFlags )+#endif+#if MIN_VERSION_ghc(9,5,0)+import Language.Haskell.Syntax.Module.Name+  ( moduleNameString )+#else+import GHC.Unit.Module.Name+  ( moduleNameString )+#endif+import GHC.Unit.Types+  ( unitIdString )+import GHC.Utils.Panic+  ( pgmErrorDoc )+import GHC.Tc.Plugin+  ( getTopEnv )+import GHC.Types.Unique.FM+  ( addToUFM, addToUFM_C, lookupUFM, plusUFM, unitUFM )++-- ghc-tcplugin-api+import GHC.TcPlugin.API+  hiding ( Type )+import GHC.TcPlugin.API.Internal+  ( MonadTcPlugin(liftTcPluginM) )++--------------------------------------------------------------------------------++-- | A 'QualifiedName' is the name of something,+-- together with the names of the module and package it comes from.+data QualifiedName (thing :: Type)+  = Qualified+    { -- | Name of the thing (e.g. name of the 'TyCon' or 'Class').+      name    :: String+      -- | Name of the module in which the thing can be found.+    , module' :: ModuleName+      -- | Name of the package in which the module can be found.+    , package :: PkgQual+    }++-- | Type-level parameter to 'Wear' type family, for higher-kinded data.+--+-- @Wear Named thing@ is the identifier data passed in as an argument.+-- @Wear Resolved thing@ is the result of name resolving the thing.+--+-- This allows users to pass a record of names, of type @MyData Named@,+-- and obtain a record of looked-up things, of type @MyData Resolved@.+--+-- Refer to 'ResolveNames' for a worked example.+data NameResolution = Named | Resolved++-- | Use this to refer to a @Promoted DataCon@.+data Promoted (thing :: k) :: Type++-- | Type-family used for higher-kinded data pattern.+--+-- This allows the same record to be re-used,+-- as explained in the worked example for 'ResolveNames'.+--+-- For instance, if one defines:+--+-- > data MyData n+-- >   = MyData+-- >   { myClass :: !( Wear n Class )+-- >   , myTyCon :: !( Wear n TyCon )+-- >   }+--+-- then a record of type @MyData Named@ is simply a record of textual names+-- (a typeclass name and a type-constructor name, with associated module & packages),+-- whereas a record of type @MyData Resolved@ contains a typeclass's @Class@+-- as well as a type-constructor's @TyCon@.+#if MIN_VERSION_ghc(9,0,0)+type Wear :: forall k. NameResolution -> k -> Type+#endif+type family Wear (n :: NameResolution) (thing :: k) :: Type where+#if MIN_VERSION_ghc(9,0,0)+  Wear @Type Named thing           = QualifiedName thing+#else+  Wear Named thing                 = QualifiedName thing+#endif+  Wear Resolved (Promoted DataCon) = TyCon+  Wear Resolved (Promoted a)+    = TypeError+      ( Text "Cannot promote " :<>: ShowType a :<>: Text "."+      :$$: Text "Can only promote 'DataCon's."+      )+  Wear Resolved thing = thing++-- | Retrieve the underlying thing being referred to by inspecting+-- the type parameter of 'QualifiedName'.+type family UnwearNamed (loc :: Type) :: Type where+  UnwearNamed (QualifiedName thing) = thing++-- | Type-class overloading things that can be looked up by name:+--+-- * classes,+-- * data constructors (as well as their promotion),+-- * type-constructors.+#if MIN_VERSION_ghc(9,0,0)+type Lookupable :: forall {k}. k -> Constraint+#endif+class Lookupable (a :: k) where+  mkOccName :: String -> OccName+  lookup :: MonadTcPlugin m => Name -> m (Wear Resolved a)++instance Lookupable TyCon where+  mkOccName = mkTcOcc+  lookup = tcLookupTyCon+instance Lookupable DataCon where+  mkOccName = mkDataOcc+  lookup = tcLookupDataCon+instance Lookupable Class where+  mkOccName = mkClsOcc+  lookup = tcLookupClass+instance Lookupable (Promoted DataCon) where+  mkOccName = mkDataOcc+  lookup = fmap promoteDataCon . tcLookupDataCon++-- | This class exposes the method 'resolveNames' which will+-- perform name resolution for all the fields in a datatype.+--+-- Example usage: we define a record that will hold+-- the things we want to look up, using the 'Wear' type family.+--+-- For example:+--+--  > data MyData n+--  >   = MyData+--  >   { myClass       :: !( Wear n Class )+--  >   , myTyCon       :: !( Wear n TyCon )+--  >   , myDataCon     :: !( Wear n DataCon )+--  >   , myPromDataCon :: !( Wear n (Promoted DataCon) )+--  >   }+--  >   deriving stock Generic+--  >   deriving ResolveNames+--  >     via Generically1 MyData+--+-- Now we can specify the names of the things which we want to look up,+-- together with the modules and packages in which they belong:+--+-- > myNames :: MyData Named+-- > myNames = MyData+-- >  { myClass = QualifiedName "MyClass" "My.Module" ( Just "my-pkg-name" )+-- >  , ...+-- >  }+--+-- Then we can call 'resolveNames':+--+-- > resolvedNames :: MonadTcPlugin m => m (MyData Resolved)+-- > resolvedNames = resolveNames myNames+--+-- This returns a record containing the looked up things we want,+-- e.g. @myClass :: Class@, @myPromDataCon :: TyCon@, etc.+class ResolveNames (f :: NameResolution -> Type) where+  resolve_names :: ( Coercible res ( f Resolved ), MonadTcPlugin m )+                => f Named -> m res+  -- Workaround: the result is anything coercible to "f Resolved" rather than just "f Resolved",+  -- because otherwise GHC complains when using DerivingVia that we don't know the role+  -- of the parameter to m, despite the quantified constraint superclass to MonadTcPlugin.+  --+  -- This unfortunately worsens type-inference, so we export+  -- 'resolveNames' separately.++-- | Resolve a collection of names.+--+-- See 'ResolveNames' for further details.+resolveNames :: ( MonadTcPlugin m, ResolveNames f )+             => f Named -> m ( f Resolved )+resolveNames = resolve_names++instance ( Generic (f Named)+         , Generic (f Resolved)+         , GTraversableC ResolveName (Rep (f Named)) (Rep (f Resolved))+         )+      => ResolveNames (Generically1 f) where+  resolve_names+    :: forall+#if MIN_VERSION_ghc(9,0,0)+         {m}+#else+          m+#endif+         res+    .  ( Coercible res ( Generically1 f Resolved ), MonadTcPlugin m )+    => Generically1 f Named -> m res+  resolve_names ( Generically1 dat )+    =  ( `evalStateT` emptyModules )+    $  coerce . to @(f Resolved)+   <$> gtraverseC @ResolveName resolveName ( from dat )++-- | Type-class dispatch for looking up names.+--+-- Every instance is of the form:+--+-- > ResolveName (Wear Named thing) (Wear Resolved thing)+--+-- which allows one to write 'resolveName':+--+-- > resolveName :: ... => Wear Named thing -> m ( Wear Resolved thing )+class    ( a ~ Wear Named    ( UnwearNamed a )+         , b ~ Wear Resolved ( UnwearNamed a )+         , Lookupable ( UnwearNamed a )+         )+      => ResolveName (a :: Type) (b :: Type)+instance ( a ~ Wear Named    ( UnwearNamed a )+         , b ~ Wear Resolved ( UnwearNamed a )+         , Lookupable ( UnwearNamed a )+         )+      => ResolveName a b++resolveName :: forall (thing :: Type) m+            .  ResolveName ( Wear Named thing ) ( Wear Resolved thing )+            => MonadTcPlugin m+            => Wear Named thing+            -> StateT ImportedModules m ( Wear Resolved thing )+resolveName (Qualified str mod_name pkg) = do+  md <- lookupModule pkg mod_name+  nm <- lift $ lookupOrig md+                 (mkOccName+#if !MIN_VERSION_ghc(9,0,0)+                   @_+#endif+                   @thing+                   str+                 )+  lift $ lookup+#if !MIN_VERSION_ghc(9,0,0)+           @_+#endif+           @thing nm++--------------------------------------------------------------------------------+-- Caching of found modules.++data ImportedModules+  = ImportedModules+    { home_modules      :: UniqFM ModuleName Module+    , this_pkg_modules  :: UniqFM UnitId ( UniqFM ModuleName Module )+    , other_pkg_modules :: UniqFM UnitId ( UniqFM ModuleName Module )+    }++emptyModules :: ImportedModules+emptyModules =+  ImportedModules+    { home_modules      = emptyUFM+    , this_pkg_modules  = emptyUFM+    , other_pkg_modules = emptyUFM+    }++lookupCachedModule :: Monad m => PkgQual -> ModuleName -> StateT ImportedModules m (Maybe Module)+lookupCachedModule NoPkgQual    mod_name+  =   ( `lookupUFM` mod_name )+  .   home_modules+  <$> get+lookupCachedModule (ThisPkg pkg) mod_name+  =   ( ( `lookupUFM` mod_name ) =<< )+  .   ( `lookupUFM` pkg )+  .   this_pkg_modules+  <$> get+lookupCachedModule (OtherPkg pkg) mod_name+  =   ( ( `lookupUFM` mod_name ) =<< )+  .   ( `lookupUFM` pkg )+  .   other_pkg_modules+  <$> get++insertCachedModule :: Monad m => PkgQual -> ModuleName -> Module -> StateT ImportedModules m ()+insertCachedModule NoPkgQual    mod_name md = do+  mods@( ImportedModules { home_modules = prev } ) <- get+  put $ mods { home_modules = addToUFM prev mod_name md }+insertCachedModule (ThisPkg pkg) mod_name md = do+  mods@( ImportedModules { this_pkg_modules = prev } ) <- get+  put $ mods { this_pkg_modules = addToUFM_C plusUFM prev pkg (unitUFM mod_name md) }+insertCachedModule (OtherPkg pkg) mod_name md = do+  mods@( ImportedModules { other_pkg_modules = prev } ) <- get+  put $ mods { other_pkg_modules = addToUFM_C plusUFM prev pkg (unitUFM mod_name md) }++lookupModule :: MonadTcPlugin m => PkgQual -> ModuleName -> StateT ImportedModules m Module+lookupModule pkg mod_name = do+  cachedResult <- lookupCachedModule pkg mod_name+  case cachedResult of+    Just res -> do+      insertCachedModule pkg mod_name res+      pure res+    Nothing -> do+      findResult <- lift $ findImportedModule mod_name pkg+      case findResult of+        Found _ res+          -> pure res+        other -> do+          hsc_env <- lift . liftTcPluginM $ getTopEnv+          let+            err_doc :: SDoc+#if MIN_VERSION_ghc(9,2,0)+            err_doc = cannotFindModule hsc_env mod_name other+#else+            err_doc = cannotFindModule dflags  mod_name other+            dflags :: DynFlags+            dflags = hsc_dflags hsc_env+#endif+          pgmErrorDoc+            ( "GHC.TcPlugin.API: could not find module " <> mod_str <> " in " <> pkg_name )+            err_doc+  where+    pkg_name, mod_str :: String+    pkg_name = case pkg of+      NoPkgQual     -> "home package"+      ThisPkg unit  -> "home-unit package " <> unitIdString unit+      OtherPkg unit -> "other unit package" <> unitIdString unit+    mod_str = moduleNameString mod_name++--------------------------------------------------------------------------------+-- Constrained traversals.++type TraversalC (c :: Type -> Type -> Constraint) (s :: Type)  (t :: Type)+  =  forall f. ( Applicative f )+  => ( forall a b. c a b => a -> f b ) -> s -> f t++class GTraversableC (c :: Type -> Type -> Constraint) (s :: Type -> Type) (t :: Type -> Type) where+  gtraverseC :: TraversalC c (s x) (t x)++instance+  ( GTraversableC c l l'+  , GTraversableC c r r'+  ) => GTraversableC c (l :*: r) (l' :*: r') where+  gtraverseC f (l :*: r)+    = (:*:) <$> gtraverseC @c f l <*> gtraverseC @c f r++instance+  ( GTraversableC c l l'+  , GTraversableC c r r'+  ) => GTraversableC c (l :+: r) (l' :+: r') where+  gtraverseC f (L1 l) = L1 <$> gtraverseC @c f l+  gtraverseC f (R1 r) = R1 <$> gtraverseC @c f r++instance GTraversableC c s t+  => GTraversableC c (M1 i m s) (M1 i m t) where+  gtraverseC f (M1 x) = M1 <$> gtraverseC @c f x++instance GTraversableC c U1 U1 where+  gtraverseC _ _ = pure U1++instance GTraversableC c V1 V1 where+  gtraverseC _ = pure++instance c a b => GTraversableC c (Rec0 a) (Rec0 b) where+  gtraverseC f (K1 a) = K1 <$> f a++--------------------------------------------------------------------------------+-- Generically and Generically1 wrappers for DerivingVia.++#if !MIN_VERSION_base(4,17,0)+-- | A type whose instances are defined generically, using the+-- 'Generic1' representation. 'Generically1' is a higher-kinded+-- version of 'Generically' that uses 'Generic'.+--+-- Generic instances can be derived for type constructors via+-- @'Generically1' F@ using @-XDerivingVia@.+newtype Generically1 (f :: k -> Type) (a :: k) = Generically1 ( f a )+#endif