Make `tcCheckSatisfiability` incremental (#18645)

By taking and returning an `InertSet`.
Every new `TcS` session can then pick up where a prior session left with
`setTcSInerts`.

Since we don't want to unflatten the Givens (and because it leads to
infinite loops, see !3971), we introduced a new variant of `runTcS`,
`runTcSInerts`, that takes and returns the `InertSet` and makes
sure not to unflatten the Givens after running the `TcS` action.

Fixes #18645 and #17836.

Metric Decrease:
    T17977
    T18478

8 files changed, 178 insertions, 50 deletions

diff --git a/compiler/GHC/HsToCore/PmCheck/Oracle.hs b/compiler/GHC/HsToCore/PmCheck/Oracle.hs
index 0109d596c5..e3f4cec57b 100644
--- a/compiler/GHC/HsToCore/PmCheck/Oracle.hs
+++ b/compiler/GHC/HsToCore/PmCheck/Oracle.hs
@@ -584,13 +584,11 @@ nameTyCt pred_ty = do
 tyOracle :: TyState -> Bag PredType -> DsM (Maybe TyState)
 tyOracle (TySt inert) cts
   = do { evs <- traverse nameTyCt cts
-       ; let new_inert = inert `unionBags` evs
        ; tracePm "tyOracle" (ppr cts)
-       ; ((_warns, errs), res) <- initTcDsForSolver $ tcCheckSatisfiability new_inert
+       ; ((_warns, errs), res) <- initTcDsForSolver $ tcCheckSatisfiability inert evs
        ; case res of
-            Just True  -> return (Just (TySt new_inert))
-            Just False -> return Nothing
-            Nothing    -> pprPanic "tyOracle" (vcat $ pprErrMsgBagWithLoc errs) }
+            Just mb_new_inert -> return (TySt <$> mb_new_inert)
+            Nothing           -> pprPanic "tyOracle" (vcat $ pprErrMsgBagWithLoc errs) }
 
 -- | A 'SatisfiabilityCheck' based on new type-level constraints.
 -- Returns a new 'Nabla' if the new constraints are compatible with existing
diff --git a/compiler/GHC/HsToCore/PmCheck/Types.hs b/compiler/GHC/HsToCore/PmCheck/Types.hs
index eea6130791..12bd5f32fb 100644
--- a/compiler/GHC/HsToCore/PmCheck/Types.hs
+++ b/compiler/GHC/HsToCore/PmCheck/Types.hs
@@ -47,7 +47,6 @@ import GHC.Prelude
 import GHC.Utils.Misc
 import GHC.Data.Bag
 import GHC.Data.FastString
-import GHC.Types.Var (EvVar)
 import GHC.Types.Id
 import GHC.Types.Var.Env
 import GHC.Types.Unique.DSet
@@ -68,7 +67,7 @@ import GHC.Core.Utils (exprType)
 import GHC.Builtin.Names
 import GHC.Builtin.Types
 import GHC.Builtin.Types.Prim
-import GHC.Tc.Utils.TcType (evVarPred)
+import GHC.Tc.Solver.Monad (InertSet, emptyInert)
 import GHC.Driver.Types (ConLikeSet)
 
 import Numeric (fromRat)
@@ -597,15 +596,14 @@ initTmState = TmSt emptySDIE emptyCoreMap
 
 -- | The type oracle state. A poor man's 'GHC.Tc.Solver.Monad.InsertSet': The invariant is
 -- that all constraints in there are mutually compatible.
-newtype TyState = TySt (Bag EvVar)
+newtype TyState = TySt InertSet
 
 -- | Not user-facing.
 instance Outputable TyState where
-  ppr (TySt evs)
-    = braces $ hcat $ punctuate comma $ map (ppr . evVarPred) $ bagToList evs
+  ppr (TySt inert) = ppr inert
 
 initTyState :: TyState
-initTyState = TySt emptyBag
+initTyState = TySt emptyInert
 
 -- | A normalised refinement type ∇ (\"nabla\"), comprised of an inert set of
 -- canonical (i.e. mutually compatible) term and type constraints that form the
diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs
index 96fe5cbca2..f08622d8f1 100644
--- a/compiler/GHC/Tc/Solver.hs
+++ b/compiler/GHC/Tc/Solver.hs
@@ -718,22 +718,22 @@ simplifyDefault theta
        ; return () }
 
 ------------------
-tcCheckSatisfiability :: Bag EvVar -> TcM Bool
--- Return True if satisfiable, False if definitely contradictory
-tcCheckSatisfiability given_ids
-  = do { lcl_env <- TcM.getLclEnv
-       ; let given_loc = mkGivenLoc topTcLevel UnkSkol lcl_env
-       ; (res, _ev_binds) <- runTcS $
-             do { traceTcS "checkSatisfiability {" (ppr given_ids)
-                ; let given_cts = mkGivens given_loc (bagToList given_ids)
-                     -- See Note [Superclasses and satisfiability]
-                ; solveSimpleGivens given_cts
-                ; insols <- getInertInsols
-                ; insols <- try_harder insols
-                ; traceTcS "checkSatisfiability }" (ppr insols)
-                ; return (isEmptyBag insols) }
-       ; return res }
- where
+tcCheckSatisfiability :: InertSet -> Bag EvVar -> TcM (Maybe InertSet)
+-- Return (Just new_inerts) if satisfiable, Nothing if definitely contradictory
+tcCheckSatisfiability inerts given_ids = do
+  (sat, new_inerts) <- runTcSInerts inerts $ do
+    traceTcS "checkSatisfiability {" (ppr inerts <+> ppr given_ids)
+    lcl_env <- TcS.getLclEnv
+    let given_loc = mkGivenLoc topTcLevel UnkSkol lcl_env
+    let given_cts = mkGivens given_loc (bagToList given_ids)
+    -- See Note [Superclasses and satisfiability]
+    solveSimpleGivens given_cts
+    insols <- getInertInsols
+    insols <- try_harder insols
+    traceTcS "checkSatisfiability }" (ppr insols)
+    return (isEmptyBag insols)
+  return $ if sat then Just new_inerts else Nothing
+  where
     try_harder :: Cts -> TcS Cts
     -- Maybe we have to search up the superclass chain to find
     -- an unsatisfiable constraint.  Example: pmcheck/T3927b.
@@ -749,15 +749,11 @@ tcCheckSatisfiability given_ids
 
 -- | Normalise a type as much as possible using the given constraints.
 -- See @Note [tcNormalise]@.
-tcNormalise :: Bag EvVar -> Type -> TcM Type
-tcNormalise given_ids ty
-  = do { lcl_env <- TcM.getLclEnv
-       ; let given_loc = mkGivenLoc topTcLevel UnkSkol lcl_env
-       ; norm_loc <- getCtLocM PatCheckOrigin Nothing
-       ; (res, _ev_binds) <- runTcS $
-             do { traceTcS "tcNormalise {" (ppr given_ids)
-                ; let given_cts = mkGivens given_loc (bagToList given_ids)
-                ; solveSimpleGivens given_cts
+tcNormalise :: InertSet -> Type -> TcM Type
+tcNormalise inerts ty
+  = do { norm_loc <- getCtLocM PatCheckOrigin Nothing
+       ; (res, _new_inerts) <- runTcSInerts inerts $
+             do { traceTcS "tcNormalise {" (ppr inerts)
                 ; ty' <- flattenType norm_loc ty
                 ; traceTcS "tcNormalise }" (ppr ty')
                 ; pure ty' }
@@ -788,8 +784,9 @@ Note [tcNormalise]
 tcNormalise is a rather atypical entrypoint to the constraint solver. Whereas
 most invocations of the constraint solver are intended to simplify a set of
 constraints or to decide if a particular set of constraints is satisfiable,
-the purpose of tcNormalise is to take a type, plus some local constraints, and
-normalise the type as much as possible with respect to those constraints.
+the purpose of tcNormalise is to take a type, plus some locally solved
+constraints in the form of an InertSet, and normalise the type as much as
+possible with respect to those constraints.
 
 It does *not* reduce type or data family applications or look through newtypes.
 
@@ -798,9 +795,9 @@ expression, it's possible that the type of the scrutinee will only reduce
 if some local equalities are solved for. See "Wrinkle: Local equalities"
 in Note [Type normalisation] in "GHC.HsToCore.PmCheck".
 
-To accomplish its stated goal, tcNormalise first feeds the local constraints
-into solveSimpleGivens, then uses flattenType to simplify the desired type
-with respect to the givens.
+To accomplish its stated goal, tcNormalise first initialises the solver monad
+with the given InertCans, then uses flattenType to simplify the desired type
+with respect to the Givens in the InertCans.
 
 ***********************************************************************************
 *                                                                                 *
@@ -893,7 +890,7 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
        ; psig_theta_vars <- mapM TcM.newEvVar psig_theta
        ; wanted_transformed_incl_derivs
             <- setTcLevel rhs_tclvl $
-               runTcSWithEvBinds ev_binds_var $
+               runTcSWithEvBinds ev_binds_var True $
                do { let loc         = mkGivenLoc rhs_tclvl UnkSkol $
                                       env_lcl tc_env
                         psig_givens = mkGivens loc psig_theta_vars
diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs
index 49a3fb5c46..7facc96055 100644
--- a/compiler/GHC/Tc/Solver/Monad.hs
+++ b/compiler/GHC/Tc/Solver/Monad.hs
@@ -15,7 +15,7 @@ module GHC.Tc.Solver.Monad (
     getWorkList, updWorkListTcS, pushLevelNoWorkList,
 
     -- The TcS monad
-    TcS, runTcS, runTcSDeriveds, runTcSWithEvBinds,
+    TcS, runTcS, runTcSDeriveds, runTcSWithEvBinds, runTcSInerts,
     failTcS, warnTcS, addErrTcS,
     runTcSEqualities,
     nestTcS, nestImplicTcS, setEvBindsTcS,
@@ -55,7 +55,7 @@ module GHC.Tc.Solver.Monad (
     tcLookupClass, tcLookupId,
 
     -- Inerts
-    InertSet(..), InertCans(..),
+    InertSet(..), InertCans(..), emptyInert,
     updInertTcS, updInertCans, updInertDicts, updInertIrreds,
     getNoGivenEqs, setInertCans,
     getInertEqs, getInertCans, getInertGivens,
@@ -2785,28 +2785,41 @@ runTcS :: TcS a                -- What to run
        -> TcM (a, EvBindMap)
 runTcS tcs
   = do { ev_binds_var <- TcM.newTcEvBinds
-       ; res <- runTcSWithEvBinds ev_binds_var tcs
+       ; res <- runTcSWithEvBinds ev_binds_var True tcs
        ; ev_binds <- TcM.getTcEvBindsMap ev_binds_var
        ; return (res, ev_binds) }
-
 -- | This variant of 'runTcS' will keep solving, even when only Deriveds
 -- are left around. It also doesn't return any evidence, as callers won't
 -- need it.
 runTcSDeriveds :: TcS a -> TcM a
 runTcSDeriveds tcs
   = do { ev_binds_var <- TcM.newTcEvBinds
-       ; runTcSWithEvBinds ev_binds_var tcs }
+       ; runTcSWithEvBinds ev_binds_var True tcs }
 
 -- | This can deal only with equality constraints.
 runTcSEqualities :: TcS a -> TcM a
 runTcSEqualities thing_inside
   = do { ev_binds_var <- TcM.newNoTcEvBinds
-       ; runTcSWithEvBinds ev_binds_var thing_inside }
+       ; runTcSWithEvBinds ev_binds_var True thing_inside }
+
+-- | A variant of 'runTcS' that takes and returns an 'InertSet' for
+-- later resumption of the 'TcS' session. Crucially, it doesn't
+-- 'unflattenGivens' when done.
+runTcSInerts :: InertSet -> TcS a -> TcM (a, InertSet)
+runTcSInerts inerts tcs = do
+  ev_binds_var <- TcM.newTcEvBinds
+  -- Passing False here to prohibit unflattening
+  runTcSWithEvBinds ev_binds_var False $ do
+    setTcSInerts inerts
+    a <- tcs
+    new_inerts <- getTcSInerts
+    return (a, new_inerts)
 
 runTcSWithEvBinds :: EvBindsVar
+                  -> Bool       -- ^ Unflatten types afterwards? Don't if you want to reuse the InertSet.
                   -> TcS a
                   -> TcM a
-runTcSWithEvBinds ev_binds_var tcs
+runTcSWithEvBinds ev_binds_var unflatten tcs
   = do { unified_var <- TcM.newTcRef 0
        ; step_count <- TcM.newTcRef 0
        ; inert_var <- TcM.newTcRef emptyInert
@@ -2824,7 +2837,7 @@ runTcSWithEvBinds ev_binds_var tcs
        ; when (count > 0) $
          csTraceTcM $ return (text "Constraint solver steps =" <+> int count)
 
-       ; unflattenGivens inert_var
+       ; when unflatten $ unflattenGivens inert_var
 
 #if defined(DEBUG)
        ; ev_binds <- TcM.getTcEvBindsMap ev_binds_var
diff --git a/testsuite/tests/pmcheck/should_compile/T17836.hs b/testsuite/tests/pmcheck/should_compile/T17836.hs
new file mode 100644
index 0000000000..3e6a055ca4
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T17836.hs
@@ -0,0 +1,97 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE PatternSynonyms #-}
+module PM where
+
+import Data.Type.Equality ( type (:~:)(..) )
+import qualified Data.Kind
+
+data Type :: Data.Kind.Type -> Data.Kind.Type where
+  SRecNil :: Type ()
+  SRecCons :: String -> Type a -> Type b -> Type (a, b)
+  SIntTy  :: Type Int
+
+pattern RecCons1 a <- (SRecCons _ _ a)
+
+eqType :: Type ty1 -> Type ty2 -> Maybe (ty1 :~: ty2)
+eqType SRecNil SRecNil = Just Refl
+eqType (SRecCons l1 s1 t1) (SRecCons l2 s2 t2)
+  | Just Refl <- s1 `eqType` s2
+  , Just Refl <- t1 `eqType` t2
+  , l1 == l2
+  = Just Refl
+eqType SIntTy  SIntTy  = Just Refl
+eqType _ _ = Nothing
+
+massive :: Int -> Type ty -> Type recty -> (forall ty'. Type ty' -> m r) -> m r
+massive fieldN sFieldTy sRecTy k =
+  case (fieldN, sFieldTy, sRecTy) of
+    (0, t, SRecCons _ t' _)
+        |  Just Refl <- t `eqType` t' -> k sFieldTy
+    (1, t, RecCons1 (SRecCons _ t' _))
+        |  Just Refl <- t `eqType` t' -> k sFieldTy
+    (2, t, RecCons1 (RecCons1 (SRecCons _ t' _)))
+        |  Just Refl <- t `eqType` t' -> k sFieldTy
+    (3, t, RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _))))
+        |  Just Refl <- t `eqType` t' -> k sFieldTy
+    (4, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _)))))
+        |  Just Refl <- t `eqType` t' -> k sFieldTy
+    (5, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _))))))
+        |  Just Refl <- t `eqType` t' -> k sFieldTy
+    (6, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _)))))))
+        |  Just Refl <- t `eqType` t' -> k sFieldTy
+    (7, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _))))))))
+        |  Just Refl <- t `eqType` t' -> k sFieldTy
+    (8, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _)))))))))
+        |  Just Refl <- t `eqType` t' -> k sFieldTy
+    (9, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _))))))))))
+        |  Just Refl <- t `eqType` t' -> k sFieldTy
+    (10, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _)))))))))))
+        |  Just Refl <- t `eqType` t' -> k sFieldTy
+    (11, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _))))))))))))
+        |  Just Refl <- t `eqType` t' -> k sFieldTy
+    (12, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _)))))))))))))
+        |  Just Refl <- t `eqType` t' -> k sFieldTy
+    (13, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _))))))))))))))
+        |  Just Refl <- t `eqType` t' -> k sFieldTy
+    (14, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _)))))))))))))))
+        |  Just Refl <- t `eqType` t' -> k sFieldTy
+    (15, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _))))))))))))))))
+        |  Just Refl <- t `eqType` t' -> k sFieldTy
+    (16, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _)))))))))))))))))
+        |  Just Refl <- t `eqType` t' -> k sFieldTy
+    (17, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _))))))))))))))))))
+        |  Just Refl <- t `eqType` t' -> k sFieldTy
+    (18, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _)))))))))))))))))))
+        |  Just Refl <- t `eqType` t' -> k sFieldTy
+    (19, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _))))))))))))))))))))
+        |  Just Refl <- t `eqType` t' -> k sFieldTy
+    (20, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _)))))))))))))))))))))
+        |  Just Refl <- t `eqType` t' -> k sFieldTy
+    (21, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _))))))))))))))))))))))
+        |  Just Refl <- t `eqType` t' -> k sFieldTy
+    (22, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _)))))))))))))))))))))))
+        |  Just Refl <- t `eqType` t' -> k sFieldTy
+    (23, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _))))))))))))))))))))))))
+        |  Just Refl <- t `eqType` t' -> k sFieldTy
+    (24, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _)))))))))))))))))))))))))
+        |  Just Refl <- t `eqType` t' -> k sFieldTy
+    (25, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _))))))))))))))))))))))))))
+        |  Just Refl <- t `eqType` t' -> k sFieldTy
+    (26, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _)))))))))))))))))))))))))))
+        |  Just Refl <- t `eqType` t' -> k sFieldTy
+    (27, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _))))))))))))))))))))))))))))
+        |  Just Refl <- t `eqType` t' -> k sFieldTy
+    (28, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _)))))))))))))))))))))))))))))
+        |  Just Refl <- t `eqType` t' -> k sFieldTy
+    (29, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _))))))))))))))))))))))))))))))
+        |  Just Refl <- t `eqType` t' -> k sFieldTy
+    (30, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _)))))))))))))))))))))))))))))))
+        |  Just Refl <- t `eqType` t' -> k sFieldTy
+    (31, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _))))))))))))))))))))))))))))))))
+        |  Just Refl <- t `eqType` t' -> k sFieldTy
+    (32, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _)))))))))))))))))))))))))))))))))
+        |  Just Refl <- t `eqType` t' -> k sFieldTy
+    _ -> error "TODO support records >32"
diff --git a/testsuite/tests/pmcheck/should_compile/T17836b.hs b/testsuite/tests/pmcheck/should_compile/T17836b.hs
new file mode 100644
index 0000000000..7cc7f098ca
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T17836b.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PatternSynonyms #-}
+module PM where
+
+data T a  where
+  T :: T b -> T (a, b)
+
+pattern P a <- (T a)
+
+massive :: T recty -> ()
+massive (P (P (P (P (P (P (P (P (P (P (P (P (P (P (P (P (P _))))))))))))))))) = ()
diff --git a/testsuite/tests/pmcheck/should_compile/T17836b.stderr b/testsuite/tests/pmcheck/should_compile/T17836b.stderr
new file mode 100644
index 0000000000..cad78da8da
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T17836b.stderr
@@ -0,0 +1,10 @@
+
+T17836b.hs:11:1: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In an equation for ‘massive’:
+        Patterns not matched:
+            T _
+            P (T _)
+            P (P (T _))
+            P (P (P (T _)))
+            ...
diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T
index e8938be163..c2f14ce664 100644
--- a/testsuite/tests/pmcheck/should_compile/all.T
+++ b/testsuite/tests/pmcheck/should_compile/all.T
@@ -124,6 +124,10 @@ test('T17729', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T17783', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T17836', collect_compiler_stats('bytes allocated',10), compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T17836b', collect_compiler_stats('bytes allocated',10), compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T17977', collect_compiler_stats('bytes allocated',10), compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T17977b', collect_compiler_stats('bytes allocated',10), compile,