diff --git a/changelog.md b/changelog.md
--- a/changelog.md
+++ b/changelog.md
@@ -1,4 +1,9 @@
 
+# Version 0.5.2.0 (2024-11-29)
+
+- Update to support GHC 9.10 and 9.12.  
+  Now requires `ghc-tcplugin-api` 0.13 or above.
+
 # Version 0.5.1.0 (2023-08-30)
 
 - Be more thorough when resetting GHC solver monad state. This should ensure
diff --git a/if-instance.cabal b/if-instance.cabal
--- a/if-instance.cabal
+++ b/if-instance.cabal
@@ -1,6 +1,6 @@
 cabal-version:  3.0
 name:           if-instance
-version:        0.5.1.0
+version:        0.5.2.0
 synopsis:       Branch on whether a constraint is satisfied
 license:        BSD-3-Clause
 build-type:     Simple
@@ -60,9 +60,9 @@
 
   build-depends:
     base
-      >= 4.15.0 && < 4.20,
+      >= 4.15.0 && < 4.22,
     ghc
-      >= 9.0    && < 9.10,
+      >= 9.0    && < 9.14,
 
   default-language:
     Haskell2010
@@ -85,7 +85,7 @@
 
   build-depends:
     ghc-tcplugin-api
-      >= 0.11 && < 0.12,
+      >= 0.13 && < 0.15,
 
   exposed-modules:
     Data.Constraint.If
diff --git a/src/IfSat/Plugin.hs b/src/IfSat/Plugin.hs
--- a/src/IfSat/Plugin.hs
+++ b/src/IfSat/Plugin.hs
@@ -15,7 +15,7 @@
 import Data.Foldable
   ( for_ )
 import Data.Maybe
-  ( catMaybes )
+  ( catMaybes, mapMaybe )
 
 -- ghc
 import GHC.Plugins
@@ -30,17 +30,17 @@
   ( solveSimpleGivens, solveSimpleWanteds )
 #endif
 import GHC.Tc.Solver.Monad
-  ( runTcS, runTcSWithEvBinds, traceTcS )
+  ( runTcSWithEvBinds, traceTcS )
 import GHC.Tc.Types
   ( TcM )
 import GHC.Tc.Types.Constraint
-  ( isEmptyWC )
+  ( isEmptyWC, CtEvidence (..), ctEvEvId )
 import GHC.Tc.Utils.TcType
   ( MetaDetails(..), metaTyVarRef
   , tyCoVarsOfTypeList
   )
 import GHC.Tc.Utils.TcMType
-  ( isUnfilledMetaTyVar )
+  ( isUnfilledMetaTyVar, newTcEvBinds )
 
 -- ghc-tcplugin-api
 import GHC.TcPlugin.API
@@ -139,8 +139,8 @@
       ct_l = mkNonCanonical ct_l_ev
       ct_r = mkNonCanonical ct_r_ev
       ct_l_ev_dest, ct_r_ev_dest :: TcEvDest
-      ct_l_ev_dest = ctev_dest ct_l_ev
-      ct_r_ev_dest = ctev_dest ct_r_ev
+      ct_l_ev_dest = wantedEvDest ct_l_ev
+      ct_r_ev_dest = wantedEvDest ct_r_ev
 
     evBindsVar <- askEvBinds
     -- Start a new constraint solver run.
@@ -172,7 +172,7 @@
               , text "ev   =" <+> ppr ct_l_evExpr
               ]
             )
-          wrapTcS $ ( Just <$> dispatchTrueEvTerm defs ct_l_ty ct_r_ty ct_l_evExpr )
+          wrapTcS $ ( Just <$> dispatchTrueEvTerm defs givens ct_l_ty ct_r_ty ct_l_evExpr )
         _ -> do
           -- We couldn't solve 'ct_l': this means we must solve 'ct_r',
           -- to provide evidence needed for the 'False' branch.
@@ -201,7 +201,7 @@
                 vcat [ text "ct_r =" <+> ppr ct_r_ty
                      , text "ev   =" <+> ppr ct_r_evExpr
                      ]
-              wrapTcS $ ( Just <$> dispatchFalseEvTerm defs ct_l_ty ct_r_ty ct_r_evExpr )
+              wrapTcS $ ( Just <$> dispatchFalseEvTerm defs givens ct_l_ty ct_r_ty ct_r_evExpr )
             _ -> do
               -- We could solve neither 'ct_l' not 'ct_r'.
               -- This means we can't solve the disjunction constraint.
@@ -245,8 +245,8 @@
 --     ( a :: ( IsSat ct_l ~ True, ct_l ) => r )
 --     ( _ :: ( IsSat ct_l ~ False, IsSat ct_r ~ True, ct_r ) => r )
 --   -> a ct_l_isSat_co ct_l_evTerm
-dispatchTrueEvTerm :: PluginDefs -> Type -> Type -> EvExpr -> TcM EvTerm
-dispatchTrueEvTerm defs@( PluginDefs { orClass } ) ct_l_ty ct_r_ty ct_l_evTerm = do
+dispatchTrueEvTerm :: PluginDefs -> [ Ct ] -> Type -> Type -> EvExpr -> TcM EvTerm
+dispatchTrueEvTerm defs@( PluginDefs { orClass } ) givens ct_l_ty ct_r_ty ct_l_evTerm = do
   r_name <- newName ( mkTyVarOcc "r" )
   a_name <- newName ( mkVarOcc   "a" )
   let
@@ -264,7 +264,7 @@
       , Type ct_r_ty
       , mkCoreLams [ r, a, b ]
         ( mkCoreApps ( Var a )
-          [ sat_co_expr defs ct_l_ty True
+          [ sat_co_expr defs ct_l_ty ( usedGivenCoercions givens ct_l_evTerm ) True
           , ct_l_evTerm
           ]
         )
@@ -277,8 +277,8 @@
 --     ( _ :: ( IsSat ct_l ~ True, ct_l ) => r )
 --     ( b :: ( IsSat ct_l ~ False, IsSat ct_r ~ True, ct_r ) => r )
 --   -> b ct_l_notSat_co ct_r_isSat_co ct_r_evTerm
-dispatchFalseEvTerm :: PluginDefs -> Type -> Type -> EvExpr -> TcM EvTerm
-dispatchFalseEvTerm defs@( PluginDefs { orClass } ) ct_l_ty ct_r_ty ct_r_evExpr = do
+dispatchFalseEvTerm :: PluginDefs -> [Ct] -> Type -> Type -> EvExpr -> TcM EvTerm
+dispatchFalseEvTerm defs@( PluginDefs { orClass } ) givens ct_l_ty ct_r_ty ct_r_evExpr = do
   r_name <- newName ( mkTyVarOcc "r" )
   b_name <- newName ( mkVarOcc   "b" )
   let
@@ -296,14 +296,17 @@
       , Type ct_r_ty
       , mkCoreLams [ r, a, b ]
         ( mkCoreApps ( Var b )
-          [ sat_co_expr defs ct_l_ty False
-          , sat_co_expr defs ct_r_ty True
+          [ sat_co_expr defs ct_l_ty [] False
+            --                       ^^
+            -- NB: GHC has no notion of apartness constraints, so there is
+            -- no evidence we can provide for why we failed to solve a constraint.
+          , sat_co_expr defs ct_r_ty ( usedGivenCoercions givens ct_r_evExpr ) True
           , ct_r_evExpr
           ]
         )
       ]
 
--- @ sat_eqTy defs ct_ty b @ represents the type @ IsSat ct ~ b @.
+-- The type @IsSat ct ~ b@.
 sat_eqTy :: PluginDefs -> Type -> Bool -> Type
 sat_eqTy ( PluginDefs { isSatTyCon } ) ct_ty booly
   = mkTyConApp eqTyCon
@@ -312,17 +315,17 @@
     rhs :: Type
     rhs = if booly then tru else fls
 
--- @ sat_co_expr defs ct_ty b @ is an expression of type @ IsSat ct ~ b @.
-sat_co_expr :: PluginDefs -> Type -> Bool -> EvExpr
-sat_co_expr ( PluginDefs { isSatTyCon } ) ct_ty booly
+-- Construct an expression of type @IsSat ct ~ b@.
+sat_co_expr :: PluginDefs -> Type -> [Coercion] -> Bool -> EvExpr
+sat_co_expr ( PluginDefs { isSatTyCon } ) ct_ty deps booly
   = mkCoreConApps eqDataCon
       [ Type boolTy
       , Type $ mkTyConApp isSatTyCon [ ct_ty ]
       , Type rhs
       , Coercion $
           mkPluginUnivCo ( "IfSat :" <> show booly )
-          Nominal
-          ( mkTyConApp isSatTyCon [ct_ty] ) rhs
+            Nominal deps
+            ( mkTyConApp isSatTyCon [ct_ty] ) rhs
       ]
   where
     rhs :: Type
@@ -332,13 +335,37 @@
 fls = mkTyConTy promotedFalseDataCon
 tru = mkTyConTy promotedTrueDataCon
 
+-- | After filling in evidence for a constraint, compute which Givens the
+-- evidence depends on.
+usedGivenCoercions :: [ Ct ] -> EvExpr -> [ Coercion ]
+usedGivenCoercions givens ev = mapMaybe dep_cv givens
+  where
+    dep_cv :: Ct -> Maybe Coercion
+    dep_cv ct
+      | ctEv@( CtGiven {} ) <- ctEvidence ct
+      , EqPred {} <- classifyPredType ( ctPred ct )
+      , let v = ctEvEvId ctEv
+      , v `elemVarSet` ev_cvs
+      = Just $ mkCoVarCo v
+      | otherwise
+      = Nothing
+    ev_cvs :: CoVarSet
+    ev_cvs = filterVarSet isCoVar $ exprFreeVars ev
+
+-- | Small utility wrapper around 'ctev_dest' to avoid incomplete record
+-- selector warnings.
+wantedEvDest :: HasDebugCallStack => CtEvidence -> TcEvDest
+wantedEvDest ( CtWanted { ctev_dest = dst } ) = dst
+wantedEvDest g@( CtGiven {} ) =
+  pprPanic "wantedEvDest called on CtGiven" (ppr g)
+
 --------------------------------------------------------------------------------
 
 rewriter :: PluginDefs -> UniqFM TyCon TcPluginRewriter
 rewriter defs@( PluginDefs { isSatTyCon } )
   = listToUFM [ ( isSatTyCon, isSatRewriter defs ) ]
 
-isSatRewriter :: PluginDefs -> [Ct] -> [Type] -> TcPluginM Rewrite TcPluginRewriteResult
+isSatRewriter :: PluginDefs -> [ Ct ] -> [ Type ] -> TcPluginM Rewrite TcPluginRewriteResult
 isSatRewriter ( PluginDefs { isSatTyCon } ) givens [ct_ty] = do
   tcPluginTrace "IfSat rewriter {" (ppr givens $$ ppr ct_ty)
   rewriteEnv <- askRewriteEnv
@@ -346,8 +373,9 @@
   let
     ct :: Ct
     ct = mkNonCanonical ct_ev
+  evBindsVar <- unsafeLiftTcM newTcEvBinds
   -- Start a new Solver run.
-  ( redn, _ ) <- unsafeLiftTcM $ runTcS $ do
+  redn <- unsafeLiftTcM $ runTcSWithEvBinds evBindsVar $ do
 
     -- Add back all the Givens.
     traceTcS "IfSat rewriter: adding Givens to the inert set" (ppr givens)
@@ -363,23 +391,31 @@
     -- Try to solve 'ct', using both Givens and top-level instances.
     residual_wc <- solveSimpleWanteds ( unitBag ct )
 
+    mb_ct_evTerm <- lookupEvTerm evBindsVar $ wantedEvDest ct_ev
+
     -- Reset the solver state to before we attempted to solve 'ct',
     -- and undo any type variable unifications that happened.
     restoreTcS
     wrapTcS $ for_ ct_unfilled_metas \ meta ->
       writeTcRef ( metaTyVarRef meta ) Flexi
 
-    -- When there are residual Wanteds, we couldn't solve the constraint.
     let
       is_sat :: Bool
-      is_sat = isEmptyWC residual_wc
       sat :: Type
-      sat
-        | is_sat
-        = mkTyConTy promotedTrueDataCon
+      deps :: [ Coercion ]
+      ( is_sat, sat, deps )
+        | Just ( EvExpr ct_evExpr ) <- mb_ct_evTerm
+        , isEmptyWC residual_wc
+        = ( True, mkTyConTy promotedTrueDataCon, usedGivenCoercions givens ct_evExpr )
         | otherwise
-        = mkTyConTy promotedFalseDataCon
-    pure $ mkTyFamAppReduction ( "IsSat: " <> show is_sat ) Nominal isSatTyCon [ct_ty] sat
+        = ( False, mkTyConTy promotedFalseDataCon, [] )
+    pure $
+      mkTyFamAppReduction ( "IsSat: " <> show is_sat )
+        Nominal
+        deps
+        isSatTyCon
+        [ct_ty]
+        sat
 
   tcPluginTrace "IfSat rewriter }" ( ppr redn )
   pure $ TcPluginRewriteTo redn []
diff --git a/src/IfSat/Plugin/Compat.hs b/src/IfSat/Plugin/Compat.hs
--- a/src/IfSat/Plugin/Compat.hs
+++ b/src/IfSat/Plugin/Compat.hs
@@ -84,7 +84,6 @@
 wrapTcS = unsafeCoerce const
 #endif
 
-
 -- Obtain the 'TcSEnv' underlying the 'TcS' monad (in the form of a 'ShimTcSEnv').
 getShimTcSEnv :: TcS ShimTcSEnv
 getShimTcSEnv = unsafeCoerce ( return :: ShimTcSEnv -> TcM ShimTcSEnv )