diff --git a/compiler/typecheck/TcDerivUtils.hs b/compiler/typecheck/TcDerivUtils.hs
index 3a662d97518a84a5e68d6c5f7c1104cbda060fd0..8991407831f81fbd347bb653cc784aac5a2b06cd 100644
--- a/compiler/typecheck/TcDerivUtils.hs
+++ b/compiler/typecheck/TcDerivUtils.hs
@@ -512,7 +512,8 @@ cond_functorOK allowFunctions allowExQuantifiedLastTyVar _ rep_tc
     tc_tvs            = tyConTyVars rep_tc
     Just (_, last_tv) = snocView tc_tvs
     bad_stupid_theta  = filter is_bad (tyConStupidTheta rep_tc)
-    is_bad pred       = last_tv `elemVarSet` tyCoVarsOfType pred
+    is_bad pred       = last_tv `elemVarSet` exactTyCoVarsOfType pred
+      -- See Note [Check that the type variable is truly universal]
 
     data_cons = tyConDataCons rep_tc
     check_con con = allValid (check_universal con : foldDataConArgs (ft_check con) con)
@@ -524,7 +525,7 @@ cond_functorOK allowFunctions allowExQuantifiedLastTyVar _ rep_tc
                 -- in TcGenFunctor
       | Just tv <- getTyVar_maybe (last (tyConAppArgs (dataConOrigResTy con)))
       , tv `elem` dataConUnivTyVars con
-      , not (tv `elemVarSet` tyCoVarsOfTypes (dataConTheta con))
+      , not (tv `elemVarSet` exactTyCoVarsOfTypes (dataConTheta con))
       = IsValid   -- See Note [Check that the type variable is truly universal]
       | otherwise
       = NotValid (badCon con existential)
@@ -666,4 +667,17 @@ As a result, T can have a derived Foldable instance:
     foldr _ z T6       = z
 
 See Note [DeriveFoldable with ExistentialQuantification] in TcGenFunctor.
+
+For Functor and Traversable, we must take care not to let type synonyms
+unfairly reject a type for not being truly universally quantified. An
+example of this is:
+
+    type C (a :: Constraint) b = a
+    data T a b = C (Show a) b => MkT b
+
+Here, the existential context (C (Show a) b) does technically mention the last
+type variable b. But this is OK, because expanding the type synonym C would
+give us the context (Show a), which doesn't mention b. Therefore, we must make
+sure to expand type synonyms before performing this check. Not doing so led to
+Trac #13813.
 -}
diff --git a/testsuite/tests/deriving/should_compile/T13813.hs b/testsuite/tests/deriving/should_compile/T13813.hs
new file mode 100644
index 0000000000000000000000000000000000000000..e63869cb974430df5d72673deb599a456a1c63e1
--- /dev/null
+++ b/testsuite/tests/deriving/should_compile/T13813.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE StandaloneDeriving #-}
+module T13813 where
+
+import GHC.Exts (Constraint)
+
+type C (a :: Constraint) b = a
+
+data T a b = C (Show a) b => MkT b
+deriving instance Functor (T a)
diff --git a/testsuite/tests/deriving/should_compile/all.T b/testsuite/tests/deriving/should_compile/all.T
index 36476d5f9c5aa47c8b4eec51c41c83a7f65efbc4..d1615ab647b3edda63dcac53b1e7bd54b0414111 100644
--- a/testsuite/tests/deriving/should_compile/all.T
+++ b/testsuite/tests/deriving/should_compile/all.T
@@ -91,3 +91,4 @@ test('T13297', normal, compile, [''])
 test('T13758', normal, compile, [''])
 test('drv-empty-data', [normalise_errmsg_fun(just_the_deriving)],compile, ['-ddump-deriv -dsuppress-uniques'])
 test('drv-phantom', [normalise_errmsg_fun(just_the_deriving)],compile, ['-ddump-deriv -dsuppress-uniques'])
+test('T13813', normal, compile, [''])