diff --git a/compiler/coreSyn/CoreArity.hs b/compiler/coreSyn/CoreArity.hs
index 37454ebee08c84b4d5fd9be7eebd3ea247a786d9..afd6759571cd463c1817e256b0ce0ff1a3c20323 100644
--- a/compiler/coreSyn/CoreArity.hs
+++ b/compiler/coreSyn/CoreArity.hs
@@ -1153,7 +1153,7 @@ freshEtaId :: Int -> TCvSubst -> Type -> (TCvSubst, Id)
 freshEtaId n subst ty
       = (subst', eta_id')
       where
-        ty'     = Type.substTy subst ty
+        ty'     = Type.substTyUnchecked subst ty
         eta_id' = uniqAway (getTCvInScope subst) $
                   mkSysLocalOrCoVar (fsLit "eta") (mkBuiltinUnique n) ty'
         subst'  = extendTCvInScope subst eta_id'
diff --git a/compiler/typecheck/TcGenGenerics.hs b/compiler/typecheck/TcGenGenerics.hs
index abc7d59a552532620a099df6d5e4f8b666d4e492..123cfd35352df7b0168960c03c10ceff11ec901b 100644
--- a/compiler/typecheck/TcGenGenerics.hs
+++ b/compiler/typecheck/TcGenGenerics.hs
@@ -431,7 +431,7 @@ tc_mkRepFamInsts gk tycon inst_tys =
            env        = zipTyEnv env_tyvars env_inst_args
            in_scope   = mkInScopeSet (tyCoVarsOfTypes inst_tys)
            subst      = mkTvSubst in_scope env
-           repTy'     = substTy  subst repTy
+           repTy'     = substTyUnchecked  subst repTy
            tcv'       = tyCoVarsOfTypeList inst_ty
            (tv', cv') = partition isTyVar tcv'
            tvs'       = scopedSort tv'
diff --git a/compiler/typecheck/TcSigs.hs b/compiler/typecheck/TcSigs.hs
index 9146b10fe2995c86f7e33fd1f4b931c8caf9e36f..7b00165c523a48e6c00a869b2eac52d8b99a088e 100644
--- a/compiler/typecheck/TcSigs.hs
+++ b/compiler/typecheck/TcSigs.hs
@@ -505,7 +505,7 @@ tcInstSig hs_sig@(PartialSig { psig_hs_ty = hs_ty
                              , sig_inst_wcs   = wcs
                              , sig_inst_wcx   = wcx
                              , sig_inst_theta = substTys subst theta
-                             , sig_inst_tau   = substTy  subst tau }
+                             , sig_inst_tau   = substTyUnchecked  subst tau }
        ; traceTc "End partial sig }" (ppr inst_sig)
        ; return inst_sig }
 
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index 9ccfaae31d674a389e8e9879b25c23a3fed74614..27fde886132f46d1e8786f75019fac8b47dc4bda 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -3196,8 +3196,7 @@ isValidTCvSubst (TCvSubst in_scope tenv cenv) =
 -- Note [The substitution invariant].
 checkValidSubst :: HasCallStack => TCvSubst -> [Type] -> [Coercion] -> a -> a
 checkValidSubst subst@(TCvSubst in_scope tenv cenv) tys cos a
--- TODO (RAE): Change back to ASSERT
-  = WARN( not (isValidTCvSubst subst),
+  = ASSERT2( isValidTCvSubst subst,
              text "in_scope" <+> ppr in_scope $$
              text "tenv" <+> ppr tenv $$
              text "tenvFVs" <+> ppr (tyCoVarsOfTypesSet tenv) $$
@@ -3205,7 +3204,7 @@ checkValidSubst subst@(TCvSubst in_scope tenv cenv) tys cos a
              text "cenvFVs" <+> ppr (tyCoVarsOfCosSet cenv) $$
              text "tys" <+> ppr tys $$
              text "cos" <+> ppr cos )
-    WARN( not tysCosFVsInScope,
+    ASSERT2( tysCosFVsInScope,
              text "in_scope" <+> ppr in_scope $$
              text "tenv" <+> ppr tenv $$
              text "cenv" <+> ppr cenv $$
diff --git a/testsuite/tests/typecheck/should_compile/T13951.hs b/testsuite/tests/typecheck/should_compile/T13951.hs
new file mode 100644
index 0000000000000000000000000000000000000000..8cbeb8c11ac5043d373eab0a8176947d0526b955
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T13951.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE PolyKinds, GADTs, Rank2Types, ScopedTypeVariables, Trustworthy #-}
+module Control.Monad.Skeleton.Internal where
+
+data Cat k a b where
+  Empty :: Cat k a a
+  Leaf :: k a b -> Cat k a b
+  Tree :: Cat k a b -> Cat k b c -> Cat k a c
+
+viewL :: forall k a b r. Cat k a b
+  -> ((a ~ b) => r)
+  -> (forall x. k a x -> Cat k x b -> r)
+  -> r
+viewL Empty e _ = e
+viewL (Leaf k) _ r = k `r` Empty
+viewL (Tree a b) e r = go a b where
+  go :: Cat k a x -> Cat k x b -> r
+  go Empty t = viewL t e r
+  go (Leaf k) t = r k t
+  go (Tree c d) t = go c (Tree d t)
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index d312f5074dc1a938ce00323f918334a4e2f7c891..b94f0210585ed55b0323dd6adf4114105fcf61bf 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -669,3 +669,4 @@ test('T16188', normal, compile, [''])
 test('T16204a', normal, compile, [''])
 test('T16204b', normal, compile, [''])
 test('T16225', normal, compile, [''])
+test('T13951', normal, compile, [''])