diff --git a/compiler/GHC/Core/Predicate.hs b/compiler/GHC/Core/Predicate.hs
index 0eeaca71f51f602182428c193ca4ff666ad445ce..cbf8b269f8f84110e9a6efe43bb10afcce08583d 100644
--- a/compiler/GHC/Core/Predicate.hs
+++ b/compiler/GHC/Core/Predicate.hs
@@ -26,7 +26,7 @@ module GHC.Core.Predicate (
   -- Implicit parameters
   isIPLikePred, mentionsIP, isIPTyCon, isIPClass,
   isCallStackTy, isCallStackPred, isCallStackPredTy,
-  isExceptionContextPred,
+  isExceptionContextPred, isExceptionContextTy,
   isIPPred_maybe,
 
   -- Evidence variables
@@ -46,7 +46,7 @@ import GHC.Prelude
 
 import GHC.Core.Type
 import GHC.Core.Class
-import GHC.Core.TyCo.Compare( eqType, tcEqTyConApps )
+import GHC.Core.TyCo.Compare( tcEqTyConApps )
 import GHC.Core.TyCo.FVs( tyCoVarsOfTypeList, tyCoVarsOfTypesList )
 import GHC.Core.TyCon
 import GHC.Core.TyCon.RecWalk
@@ -370,7 +370,7 @@ isExceptionContextPred cls tys
   | otherwise
   = Nothing
 
--- | Is a type a 'CallStack'?
+-- | Is a type an 'ExceptionContext'?
 isExceptionContextTy :: Type -> Bool
 isExceptionContextTy ty
   | Just tc <- tyConAppTyCon_maybe ty
@@ -416,31 +416,38 @@ isCallStackTy ty
 isIPLikePred :: Type -> Bool
 -- Is `pred`, or any of its superclasses, an implicit parameter?
 -- See Note [Local implicit parameters]
-isIPLikePred pred = mentions_ip_pred initIPRecTc Nothing pred
-
-mentionsIP :: Type -> Class -> [Type] -> Bool
--- Is (cls tys) an implicit parameter with key `str_ty`, or
--- is any of its superclasses such at thing.
+isIPLikePred pred =
+  mentions_ip_pred initIPRecTc (const True) (const True) pred
+
+mentionsIP :: (Type -> Bool) -- ^ predicate on the string
+           -> (Type -> Bool) -- ^ predicate on the type
+           -> Class
+           -> [Type] -> Bool
+-- ^ @'mentionsIP' str_cond ty_cond cls tys@ returns @True@ if:
+--
+--    - @cls tys@ is of the form @IP str ty@, where @str_cond str@ and @ty_cond ty@
+--      are both @True@,
+--    - or any superclass of @cls tys@ has this property.
+--
 -- See Note [Local implicit parameters]
-mentionsIP str_ty cls tys = mentions_ip initIPRecTc (Just str_ty) cls tys
-
-mentions_ip :: RecTcChecker -> Maybe Type -> Class -> [Type] -> Bool
-mentions_ip rec_clss mb_str_ty cls tys
-  | Just (str_ty', _) <- isIPPred_maybe cls tys
-  = case mb_str_ty of
-       Nothing -> True
-       Just str_ty -> str_ty `eqType` str_ty'
+mentionsIP = mentions_ip initIPRecTc
+
+mentions_ip :: RecTcChecker -> (Type -> Bool) -> (Type -> Bool) -> Class -> [Type] -> Bool
+mentions_ip rec_clss str_cond ty_cond cls tys
+  | Just (str_ty, ty) <- isIPPred_maybe cls tys
+  = str_cond str_ty && ty_cond ty
   | otherwise
-  = or [ mentions_ip_pred rec_clss mb_str_ty (classMethodInstTy sc_sel_id tys)
+  = or [ mentions_ip_pred rec_clss str_cond ty_cond (classMethodInstTy sc_sel_id tys)
        | sc_sel_id <- classSCSelIds cls ]
 
-mentions_ip_pred :: RecTcChecker -> Maybe Type -> Type -> Bool
-mentions_ip_pred  rec_clss mb_str_ty ty
+
+mentions_ip_pred :: RecTcChecker -> (Type -> Bool) -> (Type -> Bool) -> Type -> Bool
+mentions_ip_pred rec_clss str_cond ty_cond ty
   | Just (cls, tys) <- getClassPredTys_maybe ty
   , let tc = classTyCon cls
   , Just rec_clss' <- if isTupleTyCon tc then Just rec_clss
                       else checkRecTc rec_clss tc
-  = mentions_ip rec_clss' mb_str_ty cls tys
+  = mentions_ip rec_clss' str_cond ty_cond cls tys
   | otherwise
   = False -- Includes things like (D []) where D is
           -- a Constraint-ranged family; #7785
@@ -507,7 +514,38 @@ Small worries (Sept 20):
 * The superclass hunt stops when it encounters the same class again,
   but in principle we could have the same class, differently instantiated,
   and the second time it could have an implicit parameter
-I'm going to treat these as problems for another day. They are all exotic.  -}
+I'm going to treat these as problems for another day. They are all exotic.
+
+Note [Using typesAreApart when calling mentionsIP]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We call 'mentionsIP' in two situations:
+
+  (1) to check that a predicate does not contain any implicit parameters
+      IP str ty, for a fixed literal str and any type ty,
+  (2) to check that a predicate does not contain any HasCallStack or
+      HasExceptionContext constraints.
+
+In both of these cases, we want to be sure, so we should be conservative:
+
+  For (1), the predicate might contain an implicit parameter IP Str a, where
+  Str is a type family such as:
+
+    type family MyStr where MyStr = "abc"
+
+  To safeguard against this (niche) situation, instead of doing a simple
+  type equality check, we use 'typesAreApart'. This allows us to recognise
+  that 'IP MyStr a' contains an implicit parameter of the form 'IP "abc" ty'.
+
+  For (2), we similarly might have
+
+    type family MyCallStack where MyCallStack = CallStack
+
+  Again, here we use 'typesAreApart'. This allows us to see that
+
+    (?foo :: MyCallStack)
+
+  is indeed a CallStack constraint, hidden under a type family.
+-}
 
 {- *********************************************************************
 *                                                                      *
diff --git a/compiler/GHC/Tc/Solver/Dict.hs b/compiler/GHC/Tc/Solver/Dict.hs
index 2bb750d880d207cd5995f98e7a15398d495b11ec..fd2e596b292a571afa95c180397289b4025575c4 100644
--- a/compiler/GHC/Tc/Solver/Dict.hs
+++ b/compiler/GHC/Tc/Solver/Dict.hs
@@ -191,7 +191,7 @@ in two places:
 * In `GHC.Tc.Solver.InertSet.solveOneFromTheOther`, be careful when we have
    (?x :: ty) in the inert set and an identical (?x :: ty) as the work item.
 
-* In `updInertDicts` in this module, when adding [G] (?x :: ty), remove  any
+* In `updInertDicts`, in this module, when adding [G] (?x :: ty), remove any
   existing [G] (?x :: ty'), regardless of ty'.
 
 * Wrinkle (SIP1): we must be careful of superclasses.  Consider
@@ -211,7 +211,7 @@ in two places:
   An important special case is constraint tuples like [G] (% ?x::ty, Eq a %).
   But it could happen for `class xx => D xx where ...` and the constraint D
   (?x :: int).  This corner (constraint-kinded variables instantiated with
-  implicit parameter constraints) is not well explorered.
+  implicit parameter constraints) is not well explored.
 
   Example in #14218, and #23761
 
diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs
index b15feebf5c7d8e54daac018b11989d7bebce1820..b2854e17bc16ddb0d75ce4b3bf55c0630e69bff0 100644
--- a/compiler/GHC/Tc/Solver/Monad.hs
+++ b/compiler/GHC/Tc/Solver/Monad.hs
@@ -170,7 +170,7 @@ import GHC.Tc.Types.Origin
 import GHC.Tc.Types.CtLoc
 import GHC.Tc.Types.Constraint
 
-import GHC.Builtin.Names ( unsatisfiableClassNameKey )
+import GHC.Builtin.Names ( unsatisfiableClassNameKey, callStackTyConName, exceptionContextTyConName )
 
 import GHC.Core.Type
 import GHC.Core.TyCo.Rep as Rep
@@ -181,6 +181,7 @@ import GHC.Core.Predicate
 import GHC.Core.Reduction
 import GHC.Core.Class
 import GHC.Core.TyCon
+import GHC.Core.Unify (typesAreApart)
 
 import GHC.Types.Name
 import GHC.Types.TyThing
@@ -197,7 +198,7 @@ import qualified GHC.Rename.Env as TcM
 import GHC.Utils.Outputable
 import GHC.Utils.Panic
 import GHC.Utils.Logger
-import GHC.Utils.Misc (HasDebugCallStack)
+import GHC.Utils.Misc (HasDebugCallStack, (<||>))
 
 import GHC.Data.Bag as Bag
 import GHC.Data.Pair
@@ -215,7 +216,6 @@ import Data.Maybe ( isJust )
 import qualified Data.Semigroup as S
 import GHC.Types.SrcLoc
 import GHC.Rename.Env
---import GHC.Tc.Solver.Solve (solveWanteds)
 
 #if defined(DEBUG)
 import GHC.Types.Unique.Set (nonDetEltsUniqSet)
@@ -380,21 +380,24 @@ updInertDicts :: DictCt -> TcS ()
 updInertDicts dict_ct@(DictCt { di_cls = cls, di_ev = ev, di_tys = tys })
   = do { traceTcS "Adding inert dict" (ppr dict_ct $$ ppr cls  <+> ppr tys)
 
-       ; if |  isGiven ev, Just (str_ty, _) <- isIPPred_maybe cls tys
+       ; if | isGiven ev, Just (str_ty, _) <- isIPPred_maybe cls tys
             -> -- See (SIP1) and (SIP2) in Note [Shadowing of implicit parameters]
                -- Update /both/ inert_cans /and/ inert_solved_dicts.
                updInertSet $ \ inerts@(IS { inert_cans = ics, inert_solved_dicts = solved }) ->
-               inerts { inert_cans         = updDicts (filterDicts (not_ip_for str_ty)) ics
-                      , inert_solved_dicts = filterDicts (not_ip_for str_ty) solved }
-            |  otherwise
+               inerts { inert_cans         = updDicts (filterDicts (does_not_mention_ip_for str_ty)) ics
+                      , inert_solved_dicts = filterDicts (does_not_mention_ip_for str_ty) solved }
+            | otherwise
             -> return ()
-
        -- Add the new constraint to the inert set
        ; updInertCans (updDicts (addDict dict_ct)) }
   where
-    not_ip_for :: Type -> DictCt -> Bool
-    not_ip_for str_ty (DictCt { di_cls = cls, di_tys = tys })
-      = not (mentionsIP str_ty cls tys)
+    -- Does this class constraint or any of its superclasses mention
+    -- an implicit parameter (?str :: ty) for the given 'str' and any type 'ty'?
+    does_not_mention_ip_for :: Type -> DictCt -> Bool
+    does_not_mention_ip_for str_ty (DictCt { di_cls = cls, di_tys = tys })
+      = not $ mentionsIP (not . typesAreApart str_ty) (const True) cls tys
+        -- See Note [Using typesAreApart when calling mentionsIP]
+        -- in GHC.Core.Predicate
 
 updInertIrreds :: IrredCt -> TcS ()
 updInertIrreds irred
@@ -523,14 +526,88 @@ getSafeOverlapFailures
 updSolvedDicts :: InstanceWhat -> DictCt -> TcS ()
 -- Conditionally add a new item in the solved set of the monad
 -- See Note [Solved dictionaries] in GHC.Tc.Solver.InertSet
-updSolvedDicts what dict_ct@(DictCt { di_ev = ev })
+updSolvedDicts what dict_ct@(DictCt { di_cls = cls, di_tys = tys, di_ev = ev })
   | isWanted ev
   , instanceReturnsDictCon what
-  = do { traceTcS "updSolvedDicts:" $ ppr dict_ct
+  = do { is_callstack    <- is_tyConTy isCallStackTy        callStackTyConName
+       ; is_exceptionCtx <- is_tyConTy isExceptionContextTy exceptionContextTyConName
+       ; let contains_callstack_or_exceptionCtx =
+               mentionsIP
+                 (const True)
+                    -- NB: the name of the call-stack IP is irrelevant
+                    -- e.g (?foo :: CallStack) counts!
+                 (is_callstack <||> is_exceptionCtx)
+                 cls tys
+       -- See Note [Don't add HasCallStack constraints to the solved set]
+       ; unless contains_callstack_or_exceptionCtx $
+    do { traceTcS "updSolvedDicts:" $ ppr dict_ct
        ; updInertSet $ \ ics ->
-         ics { inert_solved_dicts = addSolvedDict dict_ct (inert_solved_dicts ics) } }
+           ics { inert_solved_dicts = addSolvedDict dict_ct (inert_solved_dicts ics) }
+       } }
   | otherwise
   = return ()
+  where
+
+    -- Return a predicate that decides whether a type is CallStack
+    -- or ExceptionContext, accounting for e.g. type family reduction, as
+    -- per Note [Using typesAreApart when calling mentionsIP].
+    --
+    -- See Note [Using isCallStackTy in mentionsIP].
+    is_tyConTy :: (Type -> Bool) -> Name -> TcS (Type -> Bool)
+    is_tyConTy is_eq tc_name
+      = do { (mb_tc, _) <- wrapTcS $ TcM.tryTc $ TcM.tcLookupTyCon tc_name
+           ; case mb_tc of
+              Just tc ->
+                return $ \ ty -> not (typesAreApart ty (mkTyConTy tc))
+              Nothing ->
+                return is_eq
+           }
+
+{- Note [Don't add HasCallStack constraints to the solved set]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We must not add solved Wanted dictionaries that mention HasCallStack constraints
+to the solved set, or we might fail to accumulate the proper call stack, as was
+reported in #25529.
+
+Recall that HasCallStack constraints (and the related HasExceptionContext
+constraints) are implicit parameter constraints, and are accumulated as per
+Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence.
+
+When we solve a Wanted that contains a HasCallStack constraint, we don't want
+to cache the result, because re-using that solution means re-using the call-stack
+in a different context!
+
+See also Note [Shadowing of implicit parameters], which deals with a similar
+problem with Given implicit parameter constraints.
+
+Note [Using isCallStackTy in mentionsIP]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+To implement Note [Don't add HasCallStack constraints to the solved set],
+we need to check whether a constraint contains a HasCallStack or HasExceptionContext
+constraint. We do this using the 'mentionsIP' function, but as per
+Note [Using typesAreApart when calling mentionsIP] we don't want to simply do:
+
+  mentionsIP
+    (const True) -- (ignore the implicit parameter string)
+    (isCallStackTy <||> isExceptionContextTy)
+
+because this does not account for e.g. a type family that reduces to CallStack.
+The predicate we want to use instead is:
+
+    \ ty -> not (typesAreApart ty callStackTy && typesAreApart ty exceptionContextTy)
+
+However, this is made difficult by the fact that CallStack and ExceptionContext
+are not wired-in types; they are only known-key. This means we must look them
+up using 'tcLookupTyCon'. However, this might fail, e.g. if we are in the middle
+of typechecking ghc-internal and these data-types have not been typechecked yet!
+
+In that case, we simply fall back to the naive 'isCallStackTy'/'isExceptionContextTy'
+logic.
+
+Note that it would be somewhat painful to wire-in ExceptionContext: at the time
+of writing (March 2025), this would require wiring in the ExceptionAnnotation
+class, as well as SomeExceptionAnnotation, which is a data type with existentials.
+-}
 
 getSolvedDicts :: TcS (DictMap DictCt)
 getSolvedDicts = do { ics <- getInertSet; return (inert_solved_dicts ics) }
diff --git a/compiler/GHC/Tc/Solver/Types.hs b/compiler/GHC/Tc/Solver/Types.hs
index 3fa7ab27f7d5030d978e5946093a7363c65cb63f..ebb76c521c9cfa05fad91d2d02f79c1f21520a09 100644
--- a/compiler/GHC/Tc/Solver/Types.hs
+++ b/compiler/GHC/Tc/Solver/Types.hs
@@ -178,7 +178,7 @@ Suppose f :: HasCallStack => blah.  Then
     IP "callStack" CallStack
   See Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence
 
-* We cannonicalise such constraints, in GHC.Tc.Solver.Dict.canDictNC, by
+* We canonicalise such constraints, in GHC.Tc.Solver.Dict.canDictNC, by
   pushing the call-site info on the stack, and changing the CtOrigin
   to record that has been done.
    Bind:  s1 = pushCallStack <site-info> s2
diff --git a/compiler/GHC/Tc/Types/Evidence.hs b/compiler/GHC/Tc/Types/Evidence.hs
index 032902e775c920ad09b6c8b93cc7f9a7893d5ecf..e42d3d5cce5ab70213124be227fc35a95b8c2673 100644
--- a/compiler/GHC/Tc/Types/Evidence.hs
+++ b/compiler/GHC/Tc/Types/Evidence.hs
@@ -778,7 +778,7 @@ Wrinkles
 (CS3) GHC should NEVER infer a CallStack constraint unless one was requested
   with a partial type signature (See GHC.Tc.Solver..pickQuantifiablePreds).
 
-(CS4)- A CallStack (defined in GHC.Stack.Types) is a [(String, SrcLoc)],
+(CS4) A CallStack (defined in GHC.Stack.Types) is a [(String, SrcLoc)],
   where the String is the name of the binder that is used at the
   SrcLoc. SrcLoc is also defined in GHC.Stack.Types and contains the
   package/module/file name, as well as the full source-span. Both
diff --git a/testsuite/tests/plugins/plugins10.stdout b/testsuite/tests/plugins/plugins10.stdout
index 9324ba97b083dd2f5f95698b4b3af30bc459b328..ce75d949e2de2008cfba4c051490df556a598b55 100644
--- a/testsuite/tests/plugins/plugins10.stdout
+++ b/testsuite/tests/plugins/plugins10.stdout
@@ -9,6 +9,8 @@ interfacePlugin: GHC.Internal.Prim.Ext
 interfacePlugin: GHC.Internal.TH.Quote
 interfacePlugin: GHC.Internal.TH.Syntax
 typeCheckPlugin (rn)
+interfacePlugin: GHC.Internal.Stack.Types
+interfacePlugin: GHC.Internal.Exception.Context
 typeCheckPlugin (tc)
 parsePlugin(a)
 typeCheckPlugin (rn)
diff --git a/testsuite/tests/plugins/static-plugins.stdout b/testsuite/tests/plugins/static-plugins.stdout
index 46e5b341080456e5a06bbca4b3abc140b34c9ef5..bfbe68c09f79eb60a7baddcbf76e7d54a0448f81 100644
--- a/testsuite/tests/plugins/static-plugins.stdout
+++ b/testsuite/tests/plugins/static-plugins.stdout
@@ -9,6 +9,8 @@ interfacePlugin: GHC.Internal.System.IO
 interfacePlugin: GHC.Internal.Types
 interfacePlugin: GHC.Internal.Show
 typeCheckPlugin (rn)
+interfacePlugin: GHC.Internal.Stack.Types
+interfacePlugin: GHC.Internal.Exception.Context
 interfacePlugin: GHC.Internal.TopHandler
 typeCheckPlugin (tc)
 interfacePlugin: GHC.Internal.CString
diff --git a/testsuite/tests/typecheck/should_run/T25529.hs b/testsuite/tests/typecheck/should_run/T25529.hs
new file mode 100644
index 0000000000000000000000000000000000000000..ef769e0051e00319166c9d5d65b9fd48eb69ebed
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/T25529.hs
@@ -0,0 +1,33 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE ImplicitParams #-}
+
+module Main where
+
+import GHC.Stack (HasCallStack, CallStack, SrcLoc(srcLocStartLine, srcLocStartCol), callStack, getCallStack)
+
+main :: IO ()
+main =
+  let ?myImplicitParam = ()
+   in run action
+
+type MyConstraints = (HasCallStack, ?myImplicitParam :: ())
+
+action :: MyConstraints => IO ()
+action = run $ pure ()
+
+-- | Print the current call stack and then run an action.
+run ::
+  MyConstraints =>
+  IO a ->
+  IO a
+run action = do
+  let prettyCallStack = unlines $ map prettyCallStackEntry $ getCallStack callStack
+      prettyCallStackEntry (name, loc) =
+        name
+        <> ", called at "
+        <> show (srcLocStartLine loc)
+        <> ":"
+        <> show (srcLocStartCol loc)
+  putStrLn "============================================================"
+  putStrLn prettyCallStack
+  action
diff --git a/testsuite/tests/typecheck/should_run/T25529.stdout b/testsuite/tests/typecheck/should_run/T25529.stdout
new file mode 100644
index 0000000000000000000000000000000000000000..468a27ef8aa73d98568355f70287a29e23d1c576
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/T25529.stdout
@@ -0,0 +1,7 @@
+============================================================
+run, called at 11:7
+
+============================================================
+run, called at 16:10
+action, called at 11:11
+
diff --git a/testsuite/tests/typecheck/should_run/all.T b/testsuite/tests/typecheck/should_run/all.T
index f27df87c541eef8d914a72f17fbfd52971d2b89a..1dd52653394723e8e280b71cfee9989ddbbe6e40 100755
--- a/testsuite/tests/typecheck/should_run/all.T
+++ b/testsuite/tests/typecheck/should_run/all.T
@@ -170,6 +170,7 @@ test('T22510', normal, compile_and_run, [''])
 test('T21973a', [exit_code(1)], compile_and_run, [''])
 test('T21973b', normal, compile_and_run, [''])
 test('T23761', normal, compile_and_run, [''])
+test('T25529', normal, compile_and_run, [''])
 test('T23761b', normal, compile_and_run, [''])
 test('T17594e', normal, compile_and_run, [''])