ghc-tcplugin-api 0.3.1.0 → 0.4.0.0

raw patch · 7 files changed

+836/−56 lines, 7 filesdep ~basedep ~ghcPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base, ghc

API changes (from Hackage documentation)

Files

• changelog.md +12/−0
• ghc-tcplugin-api.cabal +77/−3
• src/GHC/TcPlugin/API.hs +27/−14
• src/GHC/TcPlugin/API/Internal.hs +21/−8
• src/GHC/TcPlugin/API/Internal/Shim.hs +166/−27
• src/GHC/TcPlugin/API/Internal/Shim/Reduction.hs +68/−4
• src/GHC/TcPlugin/API/Names.hs +465/−0

@@ -1,4 +1,16 @@ 
+# 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

@@ -1,6 +1,6 @@ cabal-version:  3.0
 name:           ghc-tcplugin-api
-version:        0.3.1.0
+version:        0.4.0.0
 synopsis:       An API for type-checker plugins.
 license:        BSD-3-Clause
 build-type:     Simple
@@ -33,9 +33,9 @@ 
   build-depends:
     base
-      >= 4.15.0 && < 4.18,
+      >= 4.14.0 && < 4.18,
     ghc
-      >= 9.0    && < 9.5,
+      >= 8.10   && < 9.5,
     transformers
       >= 0.5    && < 0.6,
 
@@ -55,6 +55,7 @@ 
   exposed-modules:
     GHC.TcPlugin.API,
+    GHC.TcPlugin.API.Names,
     GHC.TcPlugin.API.Internal
 
   if impl(ghc >= 9.3.0)
@@ -66,3 +67,76 @@ 
   if impl(ghc < 9.5.0)
     cpp-options: -DHAS_DERIVEDS
+
+  -- Compatibility for versions of GHC prior to 9.0.
+  if impl(ghc < 9.0)
+
+    reexported-modules:
+        GHC.Core.Make
+      , GHC.Plugins
+      , GHC.Types.Unique.DFM
+      , GHC.Types.Unique.FM
+      , GHC.Utils.Outputable
+
+    mixins:
+      ghc
+        ( GHC        as GHC
+
+        , PrelNames  as GHC.Builtin.Names
+        , TysWiredIn as GHC.Builtin.Types
+
+        , 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
+
+        , Name       as GHC.Types.Name
+        , OccName    as GHC.Types.Name.Occurrence
+        , 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
+          )

@@ -3,7 +3,6 @@ {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE PatternSynonyms #-}
-{-# LANGUAGE StandaloneKindSignatures #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 {-|
@@ -361,14 +360,18 @@ 
     -- ** Function types
 
-  , AnonArgFlag(..), Mult
+  , AnonArgFlag(..)
   , mkFunTy, mkVisFunTy, mkInvisFunTy, mkVisFunTys
-  , mkForAllTy, mkForAllTys, mkInvisForAllTys
+  , mkForAllTy, mkForAllTys
   , mkPiTy, mkPiTys
+
+#if MIN_VERSION_ghc(9,0,0)
+  , Mult
   , mkFunTyMany
   , mkScaledFunTy
   , mkVisFunTyMany, mkVisFunTysMany
   , mkInvisFunTyMany, mkInvisFunTysMany
+#endif
 
     -- ** Zonking
 
@@ -415,9 +418,6 @@   , Pred(..), EqRel(..), FunDep, CtFlavour
   , Ct, CtLoc, CtEvidence, CtOrigin
   , QCInst
-#if MIN_VERSION_ghc(9,2,0)
-  , CanEqLHS
-#endif
   , Type, PredType
   , InstEnvs, TcLevel
 
@@ -472,15 +472,18 @@   ( Type, PredType, Kind
   , Coercion(..), CoercionHole(..)
   , UnivCoProvenance(..)
-  , AnonArgFlag(..), Mult
+  , AnonArgFlag(..)
   , mkTyVarTy, mkTyVarTys
   , mkFunTy, mkVisFunTy, mkInvisFunTy, mkVisFunTys
-  , mkForAllTy, mkForAllTys, mkInvisForAllTys
+  , mkForAllTy, mkForAllTys
   , mkPiTy, mkPiTys
+#if MIN_VERSION_ghc(9,0,0)
+  , Mult
   , mkFunTyMany
   , mkScaledFunTy
   , mkVisFunTyMany, mkVisFunTysMany
   , mkInvisFunTyMany, mkInvisFunTysMany
+#endif
   )
 import GHC.Core.Type
   ( eqType, mkTyConTy, mkTyConApp, splitTyConApp_maybe
@@ -496,16 +499,11 @@ #if HAS_REWRITING
   , TcPluginSolveResult(..), TcPluginRewriteResult(..)
   , RewriteEnv(..)
-#else
-  , TcPluginResult(..)
 #endif
   )
 import GHC.Tc.Types.Constraint
   ( Ct(..), CtLoc(..), CtEvidence(..), CtFlavour(..)
   , QCInst(..)
-#if MIN_VERSION_ghc(9,2,0)
-  , CanEqLHS(..)
-#endif
   , ctPred, ctLoc, ctEvidence, ctEvExpr
   , ctFlavour, ctEqRel, ctOrigin
   , bumpCtLocDepth
@@ -530,8 +528,15 @@   )
 import GHC.Types.Unique
   ( Unique )
-import GHC.Types.Unique.FM
+#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
@@ -801,3 +806,11 @@   -> 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
+
+#endif

@@ -6,6 +6,7 @@ {-# LANGUAGE GADTs #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE RecordWildCards #-}
 {-# LANGUAGE ScopedTypeVariables #-}
@@ -59,6 +60,8 @@   where
 
 -- base
+import Data.Coerce
+  ( Coercible )
 import Data.Kind
   ( Constraint, Type )
 import GHC.TypeLits
@@ -186,10 +189,10 @@ -- > myTcPlugin :: [String] -> GHC.TcPlugin.API.TcPlugin
 -- > myTcPlugin args = ...
 data TcPlugin = forall s. TcPlugin
-  { tcPluginInit    :: TcPluginM Init s
+  { tcPluginInit :: TcPluginM Init s
       -- ^ Initialise plugin, when entering type-checker.
 
-  , tcPluginSolve   :: s -> TcPluginSolver
+  , tcPluginSolve :: s -> TcPluginSolver
       -- ^ Solve some constraints.
       --
       -- This function will be invoked at two points in the constraint solving
@@ -204,7 +207,12 @@       -- Use @ \\ _ _ _ -> pure $ TcPluginOK [] [] @ if your plugin
       -- does not provide this functionality.
 
-  , tcPluginRewrite :: s -> GHC.UniqFM GHC.TyCon TcPluginRewriter
+  , 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
@@ -216,7 +224,7 @@     --
     -- Use @ const emptyUFM @ if your plugin does not provide this functionality.
 
-  , tcPluginStop    :: s -> TcPluginM Stop ()
+  , tcPluginStop :: s -> TcPluginM Stop ()
    -- ^ Clean up after the plugin, when exiting the type-checker.
   }
 
@@ -286,7 +294,7 @@ -- Note that you must import the internal module in order to access the methods.
 -- Please report a bug if you find yourself needing this functionality.
 type  MonadTcPlugin :: ( Type -> Type ) -> Constraint
-class Monad m => MonadTcPlugin m where
+class ( Monad m, ( forall x y. Coercible x y => Coercible (m x) (m y) ) ) => MonadTcPlugin m where
 
   {-# MINIMAL liftTcPluginM, unsafeWithRunInTcM #-}
 
@@ -361,7 +369,7 @@ instance MonadTcPlugin ( TcPluginM Stop ) where
   liftTcPluginM = TcPluginStopM
   unsafeWithRunInTcM runInTcM
-    = unsafeLiftTcM $ runInTcM 
+    = unsafeLiftTcM $ runInTcM
 #ifdef HAS_REWRITING
       ( GHC.runTcPluginM . tcPluginStopM )
 #else
@@ -432,7 +440,12 @@ #else
     adaptUserSolveAndRewrite
       :: ( userDefs -> TcPluginSolver )
-      -> ( userDefs -> GHC.UniqFM GHC.TyCon TcPluginRewriter )
+      -> ( userDefs -> GHC.UniqFM
+#if MIN_VERSION_ghc(9,0,0)
+                         GHC.TyCon
+#endif
+                         TcPluginRewriter
+         )
       -> TcPluginDefs userDefs
       -> GHC.TcPluginSolver
     adaptUserSolveAndRewrite userSolve userRewrite ( TcPluginDefs { tcPluginUserDefs, tcPluginBuiltinDefs } )
@@ -492,7 +505,7 @@ -- | 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'.

@@ -18,7 +18,7 @@ 
 module GHC.TcPlugin.API.Internal.Shim
   ( Reduction(..), mkReduction
-  , TcPluginSolveResult, TcPluginRewriteResult(..)
+  , TcPluginSolveResult(TcPluginContradiction, TcPluginOk, ..), TcPluginRewriteResult(..)
   , RewriteEnv(..)
   , shimRewriter
   )
@@ -28,11 +28,13 @@ import Prelude
   hiding ( Floating(cos), iterate )
 import Control.Monad
-  ( forM, when )
-#if !MIN_VERSION_ghc(9,2,0)
+  ( forM, unless, when )
 import Data.Foldable
-  ( foldlM )
+  ( traverse_
+#if !MIN_VERSION_ghc(9,2,0)
+  , foldlM
 #endif
+  )
 #if MIN_VERSION_ghc(9,2,0)
 import Data.List.NonEmpty
   ( NonEmpty((:|)) )
@@ -71,7 +73,11 @@   )
 import GHC.Core.Type
   ( TyVar
-  , tcView , mkTyConApp, mkScaled, coreView , tymult, tyVarKind
+  , 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
@@ -88,6 +94,7 @@   , matchFam
   , runTcPluginTcS, runTcSWithEvBinds
   , traceTcS
+  , setWantedEvTerm
 #if MIN_VERSION_ghc(9,2,0)
   , lookupFamAppCache, lookupFamAppInert, extendFamAppCache
   , pattern EqualCtList
@@ -96,11 +103,13 @@ #endif
   )
 import GHC.Tc.Types
-  ( TcPluginM, TcPluginResult(..)
+  ( TcPluginM
   , unsafeTcPluginTcM, getEvBindsTcPluginM
   )
+import qualified GHC.Tc.Types as GHC
+  ( TcPluginResult(..) )
 import GHC.Tc.Types.Constraint
-  ( Ct(..)
+  ( Ct(..), CtEvidence(..)
   , CtLoc, CtFlavour(..), CtFlavourRole, ShadowInfo(..)
 #if MIN_VERSION_ghc(9,2,0)
   , CanEqLHS(..)
@@ -149,14 +158,89 @@ 
 --------------------------------------------------------------------------------
 
+-- | The type-family rewriting environment.
 data RewriteEnv
   = FE { fe_loc     :: !CtLoc
        , fe_flavour :: !CtFlavour
        , fe_eq_rel  :: !EqRel
        }
 
-type TcPluginSolveResult = TcPluginResult
+-- | 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.
@@ -173,28 +257,38 @@ 
 type Rewriter = RewriteEnv -> [Ct] -> [Type] -> TcPluginM TcPluginRewriteResult
 
-type Rewriters = UniqFM TyCon Rewriter
+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 TcPluginSolveResult
+             -> TcPluginM GHC.TcPluginResult
 shimRewriter givens deriveds wanteds rws solver
   | isNullUFM rws
-  = solver givens deriveds wanteds
+  = adaptSolveResult (null wanteds) =<< solver givens deriveds wanteds
   | otherwise
   = do
-    res <- solver givens deriveds wanteds
-    case res of
-      contra@( TcPluginContradiction {} ) ->
-        pure contra
-      TcPluginOk solved new -> do
-        ( rewrittenDeriveds, solvedDeriveds, newCts1 ) <- traverseCts ( reduceCt rws givens ) deriveds
-        ( rewrittenWanteds , solvedWanteds , newCts2 ) <- traverseCts ( reduceCt rws givens ) wanteds
-        pure $
-            TcPluginOk
-              ( solved ++ solvedDeriveds ++ solvedWanteds )
-              ( new ++ newCts1 ++ rewrittenDeriveds ++ newCts2 ++ rewrittenWanteds )
+    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]
@@ -262,12 +356,31 @@   | otherwise
   = rewrite_ty_con_app tc tys
 
-rewrite_one (FunTy { ft_af = vis, ft_mult = mult, ft_arg = ty1, ft_res = ty2 })
+rewrite_one
+  (FunTy
+    { ft_af = vis
+#if MIN_VERSION_ghc(9,0,0)
+    , ft_mult = mult
+#endif
+    , ft_arg = ty1
+    , ft_res = 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 vis w_redn arg_redn res_redn }
+       ; return $
+           mkFunRedn
+             role
+             vis
+#if MIN_VERSION_ghc(9,0,0)
+             w_redn
+#endif
+             arg_redn
+             res_redn
+        }
 
 rewrite_one ty@(ForAllTy {})
   = do { let (bndrs, rho) = tcSplitForAllTyVarBinders ty
@@ -555,9 +668,27 @@   split _ (ForAllTy b res) =
     let !(bs, ty', _) = split res res
     in  (Named b : bs, ty', True)
-  split _ (FunTy { ft_af = af, ft_mult = w, ft_arg = arg, ft_res = res }) =
+  split _
+    (FunTy
+      { ft_af = af
+#if MIN_VERSION_ghc(9,0,0)
+      , ft_mult = w
+#endif
+      , ft_arg = arg
+      , ft_res = res
+      }
+    ) =
     let !(bs, ty', named) = split res res
-    in  (Anon af (mkScaled w arg) : bs, ty', named)
+    in  ( Anon
+          af
+#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' #-}
@@ -568,7 +699,15 @@     go (Bndr tv (NamedTCB vis)) (bndrs, _)
       = (Named (Bndr tv vis) : bndrs, True)
     go (Bndr tv (AnonTCB af))   (bndrs, n)
-      = (Anon af (tymult (tyVarKind tv)) : bndrs, n)
+      = (Anon af
+          (
+#if MIN_VERSION_ghc(9,0,0)
+            tymult
+#endif
+             (tyVarKind tv)
+          )
+          : bndrs
+        , n)
     {-# INLINE go #-}
 {-# INLINE ty_con_binders_ty_binders' #-}
 

@@ -1,4 +1,5 @@ {-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE CPP #-}
 
 module GHC.TcPlugin.API.Internal.Shim.Reduction where
 
@@ -12,8 +13,13 @@ import GHC.Core.Coercion
   ( Coercion, CoercionN, MCoercion(..)
   , Role(Nominal), LiftingContext
+#if MIN_VERSION_ghc(9,0,0)
   , castCoercionKind1, castCoercionKind2
-  , coercionLKind, coercionRKind, coercionKind
+  , coercionLKind, coercionRKind
+#else
+  , mkCoherenceLeftCo, mkNomReflCo
+#endif
+  , coercionKind
   , coToMCo
   , decomposePiCos, downgradeRole
   , liftCoSubst, emptyLiftingContext, extendLiftingContextAndInScope, zapLiftingContext
@@ -27,7 +33,11 @@ import GHC.Core.Predicate
   ( mkClassPred )
 import GHC.Core.TyCo.Rep
-  ( TyCoBinder, mkFunTy )
+  ( TyCoBinder, mkFunTy
+#if !MIN_VERSION_ghc(9,0,0)
+  , Coercion(..)
+#endif
+  )
 import GHC.Core.TyCon
   ( TyCon )
 import GHC.Core.Type
@@ -314,17 +324,35 @@ -- Combines 'mkFunCo' and 'mkFunTy'.
 mkFunRedn :: Role
           -> AnonArgFlag
+#if MIN_VERSION_ghc(9,0,0)
           -> ReductionN -- ^ multiplicity reduction
+#endif
           -> Reduction  -- ^ argument reduction
           -> Reduction  -- ^ result reduction
           -> Reduction
 mkFunRedn r vis
+#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 w_co arg_co res_co)
-        (mkFunTy vis w_ty arg_ty res_ty)
+        ( mkFunCo
+            r
+#if MIN_VERSION_ghc(9,0,0)
+            w_co
+#endif
+            arg_co
+            res_co
+        )
+        ( mkFunTy
+            vis
+#if MIN_VERSION_ghc(9,0,0)
+            w_ty
+#endif
+            arg_ty
+            res_ty
+        )
 {-# INLINE mkFunRedn #-}
 
 -- | Create a 'Reduction' associated to a Π type,
@@ -516,3 +544,39 @@ 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

@@ -0,0 +1,465 @@+{-# 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 StandaloneKindSignatures #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+{-|
+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
+import GHC.Utils.Panic
+  ( pgmErrorDoc )
+import GHC.Unit.Module.Name
+  ( moduleNameString )
+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.
+type QualifiedName :: k -> Type
+data QualifiedName thing
+  = 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.
+      -- Use 'Nothing' to signify the current home package.
+    , package :: Maybe FastString
+    }
+
+-- | 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@.
+type Promoted :: k -> Type
+data Promoted thing
+
+-- | 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@.
+type Wear :: forall k. NameResolution -> k -> Type
+type family Wear n thing where
+  Wear Named    thing              = QualifiedName thing
+  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 UnwearNamed :: Type -> Type
+type family UnwearNamed loc 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 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.
+type ResolveNames :: ( NameResolution -> Type ) -> Constraint
+class ResolveNames f 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 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 )
+type     ResolveName :: Type -> Type -> Constraint
+class    ( a ~ Wear Named    ( UnwearNamed a )
+         , b ~ Wear Resolved ( UnwearNamed a )
+         , Lookupable ( UnwearNamed a )
+         )
+      => ResolveName a b
+instance ( a ~ Wear Named    ( UnwearNamed a )
+         , b ~ Wear Resolved ( UnwearNamed a )
+         , Lookupable ( UnwearNamed a )
+         )
+      => ResolveName a b
+
+resolveName :: forall thing m
+            .  ResolveName ( Wear Named thing ) ( Wear Resolved thing )
+            => MonadTcPlugin m
+            => Wear Named thing
+            -> StateT ImportedModules m ( Wear Resolved thing )
+resolveName (Qualified str mod_name mb_pkg) = do
+  md <- lookupModule mb_pkg mod_name
+  nm <- lift $ lookupOrig md (mkOccName @thing str)
+  lift $ lookup @thing nm
+
+--------------------------------------------------------------------------------
+-- Caching of found modules.
+
+data ImportedModules
+  = ImportedModules
+    { home_modules :: UniqFM ModuleName Module
+    , pkg_modules  :: UniqFM FastString ( UniqFM ModuleName Module )
+    }
+
+emptyModules :: ImportedModules
+emptyModules = ImportedModules emptyUFM emptyUFM
+
+lookupCachedModule :: Monad m => Maybe FastString -> ModuleName -> StateT ImportedModules m (Maybe Module)
+lookupCachedModule Nothing    mod_name
+  =   ( `lookupUFM` mod_name )
+  .   home_modules
+  <$> get
+lookupCachedModule (Just pkg) mod_name
+  =   ( ( `lookupUFM` mod_name ) =<< )
+  .   ( `lookupUFM` pkg )
+  .   pkg_modules
+  <$> get
+
+insertCachedModule :: Monad m => Maybe FastString -> ModuleName -> Module -> StateT ImportedModules m ()
+insertCachedModule Nothing    mod_name md = do
+  mods@( ImportedModules { home_modules = prev } ) <- get
+  put $ mods { home_modules = addToUFM prev mod_name md }
+insertCachedModule (Just pkg) mod_name md = do
+  mods@( ImportedModules { pkg_modules = prev } ) <- get
+  put $ mods { pkg_modules = addToUFM_C plusUFM prev pkg (unitUFM mod_name md) }
+
+lookupModule :: MonadTcPlugin m => Maybe FastString -> ModuleName -> StateT ImportedModules m Module
+lookupModule mb_pkg mod_name = do
+  cachedResult <- lookupCachedModule mb_pkg mod_name
+  case cachedResult of
+    Just res -> do
+      insertCachedModule mb_pkg mod_name res
+      pure res
+    Nothing -> do
+      findResult <- lift $ findImportedModule mod_name mb_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 mb_pkg of
+      Just pkg -> "package " <> show pkg
+      Nothing  -> "home package"
+    mod_str = moduleNameString mod_name
+
+--------------------------------------------------------------------------------
+-- Constrained traversals.
+
+type TraversalC :: ( Type -> Type -> Constraint ) -> Type -> Type -> Type
+type TraversalC c s t
+  =  forall f. ( Applicative f )
+  => ( forall a b. c a b => a -> f b ) -> s -> f t
+
+type GTraversableC :: ( Type -> Type -> Constraint )
+                   -> ( Type -> Type )
+                   -> ( Type -> Type )
+                   -> Constraint
+class GTraversableC c s t 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@.
+type    Generically1 :: ( k -> Type ) -> ( k -> Type )
+newtype Generically1 f a = Generically1 ( f a )
+  deriving newtype Generic
+#endif