diff --git a/changelog.md b/changelog.md
--- a/changelog.md
+++ b/changelog.md
@@ -1,3 +1,18 @@
+# Version 0.12.0.0 (2024-22-10)
+
+- Add support for GHC 9.12.
+
+- `mkPluginUnivCo`, `mkPluginUnivEvTerm` and `mkTyFamAppReduction` now all take
+  an additional `DVarSet` argument which allows specifying evidence that we
+  depend on. This stops evidence terms being floated out past used enclosing
+  Givens (see [GHC issue #23923](https://gitlab.haskell.org/ghc/ghc/-/issues/23923)).
+
+- Re-export `DVarSet`, `emptyDVarSet`, `extendDVarSet`, `unionDVarSet`,
+  `unitDVarSet`, and `mkDVarSet`, as well as `ctEvId`, in order to facilitate
+  construction and manipulation of `DVarSet`s.
+
+- Re-export `GHC.Types.Unique.Set`, `GHC.Types.Unique.DSet`.
+
 # Version 0.11.0.0 (2023-08-29)
 
 - Add support for GHC 9.8.
diff --git a/ghc-tcplugin-api.cabal b/ghc-tcplugin-api.cabal
--- a/ghc-tcplugin-api.cabal
+++ b/ghc-tcplugin-api.cabal
@@ -1,12 +1,12 @@
 cabal-version:  3.0
 name:           ghc-tcplugin-api
-version:        0.11.0.0
+version:        0.12.0.0
 synopsis:       An API for type-checker plugins.
 license:        BSD-3-Clause
 build-type:     Simple
 author:         Sam Derbyshire
 maintainer:     Sam Derbyshire
-copyright:      2021-2023 Sam Derbyshire
+copyright:      2021-2024 Sam Derbyshire
 homepage:       https://github.com/sheaf/ghc-tcplugin-api
 category:       Type System, GHC, Plugin
 description:
@@ -33,11 +33,11 @@
 
   build-depends:
     base
-      >= 4.13.0 && < 4.20,
+      >= 4.13.0 && < 4.22,
     containers
-      >= 0.6    && < 0.7,
+      >= 0.6    && < 0.8,
     ghc
-      >= 8.8    && < 9.9,
+      >= 8.8    && < 9.13,
     transformers
       >= 0.5    && < 0.7,
 
@@ -68,6 +68,8 @@
     , GHC.Plugins
     , GHC.Types.Unique.DFM
     , GHC.Types.Unique.FM
+    , GHC.Types.Unique.Set
+    , GHC.Types.Unique.DSet
     , GHC.Utils.Outputable
 
   if impl(ghc >= 9.3.0)
@@ -126,7 +128,9 @@
         , SrcLoc     as GHC.Types.SrcLoc
         , Unique     as GHC.Types.Unique
         , UniqDFM    as GHC.Types.Unique.DFM
+        , UniqDSet   as GHC.Types.Unique.DSet
         , UniqFM     as GHC.Types.Unique.FM
+        , UniqSet    as GHC.Types.Unique.Set
         , Var        as GHC.Types.Var
         , VarEnv     as GHC.Types.Var.Env
         , VarSet     as GHC.Types.Var.Set
diff --git a/src/GHC/TcPlugin/API.hs b/src/GHC/TcPlugin/API.hs
--- a/src/GHC/TcPlugin/API.hs
+++ b/src/GHC/TcPlugin/API.hs
@@ -246,6 +246,7 @@
     -- | == Some further functions for inspecting constraints
   , eqType
   , ctLoc, ctEvidence, ctFlavour, ctEqRel, ctOrigin
+  , ctEvId
 
     -- ** Constraint evidence
 
@@ -259,6 +260,20 @@
   , mkReflCo, mkSymCo, mkTransCo, mkUnivCo
   , mkCoercionTy, isCoercionTy, isCoercionTy_maybe
 
+    -- *** Depending on outer Givens
+
+    -- | When a plugin returns a coercion that depends on outer Given constraints,
+    -- it should declare this dependency using the 'DVarSet' argument to
+    -- functions such as 'mkPluginUnivCo', 'mkPluginUnivEvTerm' and 'mkTyFamAppReduction'
+    -- in order to avoid this coercion getting floated out past such enclosing
+    -- Givens.
+    --
+    -- You can use 'ctEvId' to obtain the evidence variable corresponding to
+    -- a Given constraint, and functions such as 'emptyDVarSet', 'unitDVarSet',
+    -- 'unionDVarSet' and 'extendDVarSet' to construct the appropriate 'DVarSet's.
+  , DVarSet
+  , emptyDVarSet, unitDVarSet, unionDVarSet, extendDVarSet, mkDVarSet
+
     -- *** Evidence terms
 
     -- | Typeclass constraints have a different notion of evidence: evidence terms.
@@ -611,7 +626,7 @@
 import GHC.Tc.Types.Constraint
   ( Ct(..), CtLoc(..), CtEvidence(..), CtFlavour(..)
   , QCInst(..), TcEvDest(..)
-  , ctPred, ctLoc, ctEvidence, ctEvExpr
+  , ctPred, ctLoc, ctEvidence, ctEvId, ctEvExpr
   , ctFlavour, ctEqRel, ctOrigin
   , bumpCtLocDepth
   , mkNonCanonical
@@ -649,6 +664,11 @@
   ( OccName(..)
   , mkVarOcc, mkDataOcc, mkTyVarOcc, mkTcOcc, mkClsOcc
   )
+import GHC.Types.Var.Set
+  ( mkDVarSet, emptyDVarSet, extendDVarSet
+  , unitDVarSet, extendDVarSet, unionDVarSet
+  , DVarSet
+  )
 #if MIN_VERSION_ghc(9,3,0)
 import GHC
   ( HscEnv )
@@ -1007,12 +1027,20 @@
 -- The plugin is responsible for not emitting any unsound coercions,
 -- such as a coercion between 'Int' and 'Float'.
 mkPluginUnivCo
-  :: String -- ^ Name of equality (for the plugin's internal use, or for debugging)
+  :: String  -- ^ Name of equality (for the plugin's internal use, or for debugging)
   -> Role
-  -> TcType -- ^ LHS
-  -> TcType -- ^ RHS
+  -> DVarSet -- ^ Evidence that this proof term depends on (use e.g. 'ctEvId' for a Given)
+  -> TcType  -- ^ LHS
+  -> TcType  -- ^ RHS
   -> Coercion
-mkPluginUnivCo str role lhs rhs = mkUnivCo ( PluginProv str ) role lhs rhs
+mkPluginUnivCo str role _deps lhs rhs =
+  let prov =
+        PluginProv
+          str
+#if MIN_VERSION_ghc(9,11,0)
+          _deps
+#endif
+  in mkUnivCo prov role lhs rhs
 
 -- | Conjure up an evidence term for an equality between two types
 -- at the given 'Role' ('Nominal' or 'Representational').
@@ -1022,12 +1050,14 @@
 -- The plugin is responsible for not emitting any unsound equalities,
 -- such as an equality between 'Int' and 'Float'.
 mkPluginUnivEvTerm
-  :: String -- ^ Name of equality (for the plugin's internal use, or for debugging)
+  :: String  -- ^ Name of equality (for the plugin's internal use, or for debugging)
   -> Role
-  -> TcType -- ^ LHS
-  -> TcType -- ^ RHS
+  -> DVarSet -- ^ Evidence that this proof term depends on (use e.g. 'ctEvId' for a Given)
+  -> TcType  -- ^ LHS
+  -> TcType  -- ^ RHS
   -> EvTerm
-mkPluginUnivEvTerm str role lhs rhs = evCoercion $ mkPluginUnivCo str role lhs rhs
+mkPluginUnivEvTerm str role deps lhs rhs =
+  evCoercion $ mkPluginUnivCo str role deps lhs rhs
 
 -- | Provide a rewriting of a saturated type family application
 -- at the given 'Role' ('Nominal' or 'Representational').
@@ -1035,14 +1065,15 @@
 -- The result can be passed to 'TcPluginRewriteTo' to specify the outcome
 -- of rewriting a type family application.
 mkTyFamAppReduction
-  :: String   -- ^ Name of reduction (for debugging)
-  -> Role     -- ^ Role of reduction ('Nominal' or 'Representational')
-  -> TyCon    -- ^ Type family 'TyCon'
-  -> [TcType] -- ^ Type family arguments
-  -> TcType   -- ^ The type that the type family application reduces to
+  :: String    -- ^ Name of reduction (for debugging)
+  -> Role      -- ^ Role of reduction ('Nominal' or 'Representational')
+  -> DVarSet   -- ^ Evidence that this reduction depends on (use e.g. 'ctEvId' for a Given)
+  -> TyCon     -- ^ Type family 'TyCon'
+  -> [TcType]  -- ^ Type family arguments
+  -> TcType    -- ^ The type that the type family application reduces to
   -> Reduction
-mkTyFamAppReduction str role tc args ty =
-  Reduction ( mkPluginUnivCo str role ( mkTyConApp tc args ) ty ) ty
+mkTyFamAppReduction str role deps tc args ty =
+  Reduction ( mkPluginUnivCo str role deps ( mkTyConApp tc args ) ty ) ty
 
 --------------------------------------------------------------------------------