Disallow unlifted binders in {Trans,Par}ListCompwip/transform-list-comp

  As noted in #20864 the variables used by a then clause in
  TransformListComp need to be of lifted type, because they are passed
  to the "take" function and put into tuples, which require lifted
  arguments.

  A similar problem was happening in parallel list comprehensions,
  which also require lifted variables as we put zip them together
  using tuples. So we also require that the bound types are lifted,
  at least until we can come up with a more general desugaring method
  that can handle unboxed types.

  Closes #20864 and #20855

18 files changed, 422 insertions, 34 deletions

diff --git a/compiler/GHC/Rename/Expr.hs b/compiler/GHC/Rename/Expr.hs
index 6316ecea63..7300908ea7 100644
--- a/compiler/GHC/Rename/Expr.hs
+++ b/compiler/GHC/Rename/Expr.hs
@@ -1256,7 +1256,7 @@ rnStmt ctxt _ (L loc (TransStmt { trS_stmts = stmts, trS_by = by, trS_form = for
        ; let all_fvs  = fvs1 `plusFV` fvs2 `plusFV` fvs3
                              `plusFV` fvs4 `plusFV` fvs5
              bndr_map = used_bndrs `zip` used_bndrs
-             -- See Note [TransStmt binder map] in GHC.Hs.Expr
+             -- See Note [TransStmt binder map] in Language.Haskell.Syntax.Expr
 
        ; traceRn "rnStmt: implicitly rebound these used binders:" (ppr bndr_map)
        ; return (([(L loc (TransStmt { trS_ext = noExtField
diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs
index 237c6fa4a3..a9dabdc783 100644
--- a/compiler/GHC/Tc/Errors.hs
+++ b/compiler/GHC/Tc/Errors.hs
@@ -1676,10 +1676,14 @@ mkTyVarEqErr' :: SolverReportErrCtxt -> ErrorItem
               -> (TcTyVar, TcCoercionN) -> TcType -> TcM (AccReportMsgs, [GhcHint])
 mkTyVarEqErr' ctxt item (tv1, co1) ty2
 
-  -- Is this a representation-polymorphism error, e.g.
-  -- alpha[conc] ~# rr[sk] ? If so, handle that first.
-  | Just frr_info <- mb_concrete_reason
-  = do
+  -- Is this an error involving a concrete metavariable being equal
+  -- to a non-concrete type, e.g. alpha[conc] ~# rr[sk]?
+  -- If so, handle that first.
+  | Just (conc_reason, conc_tv, not_conc) <- mb_concrete_reason
+  = case conc_reason of
+    ConcreteFRR frr_orig -> do
+      let frr_info = FRR_Info { frr_info_origin = frr_orig
+                              , frr_info_not_concrete = Just (conc_tv, not_conc) }
       (_, infos) <- zonkTidyFRRInfos (cec_tidy ctxt) [frr_info]
       return (FixedRuntimeRepError infos :| [], [])
 
@@ -1776,20 +1780,17 @@ mkTyVarEqErr' ctxt item (tv1, co1) ty2
     -- we need to retrieve the ConcreteTvOrigin. Just knowing whether
     -- there is an error is not sufficient. See #21430.
     mb_concrete_reason
-      | Just frr_orig <- isConcreteTyVar_maybe tv1
+      | Just conc_orig <- isConcreteTyVar_maybe tv1
       , not (isConcrete ty2)
-      = Just $ frr_reason frr_orig tv1 ty2
-      | Just (tv2, frr_orig) <- isConcreteTyVarTy_maybe ty2
+      = Just (conc_orig, tv1, ty2)
+      | Just (tv2, conc_orig) <- isConcreteTyVarTy_maybe ty2
       , not (isConcreteTyVar tv1)
-      = Just $ frr_reason frr_orig tv2 ty1
+      = Just (conc_orig, tv2, ty1)
       -- NB: if it's an unsolved equality in which both sides are concrete
       -- (e.g. a concrete type variable on both sides), then it's not a
       -- representation-polymorphism problem.
       | otherwise
       = Nothing
-    frr_reason (ConcreteFRR frr_orig) conc_tv not_conc
-      = FRR_Info { frr_info_origin = frr_orig
-                 , frr_info_not_concrete = Just (conc_tv, not_conc) }
 
     ty1 = mkTyVarTy tv1
 
diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs
index 349f587ddc..b89556a42a 100644
--- a/compiler/GHC/Tc/Errors/Ppr.hs
+++ b/compiler/GHC/Tc/Errors/Ppr.hs
@@ -3,6 +3,7 @@
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE NamedFieldPuns #-}
 {-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE ViewPatterns #-}
 
 {-# OPTIONS_GHC -fno-warn-orphans #-} -- instance Diagnostic TcRnMessage
 
@@ -723,7 +724,8 @@ instance Diagnostic TcRnMessage where
                      , text "in the following constraint" <> plural tidy_wanteds ])
              2
              (pprWithArising tidy_wanteds)
-
+    TcRnMustBeLifted ctxt bad_ids
+      -> mkSimpleDecorated $ pprMustBeLiftedError ctxt bad_ids
 
     TcRnForeignImportPrimExtNotSet _decl
       -> mkSimpleDecorated $
@@ -1271,6 +1273,8 @@ instance Diagnostic TcRnMessage where
       -> ErrorWithoutFlag
     TcRnPragmaWarning{}
       -> WarningWithFlag Opt_WarnWarningsDeprecations
+    TcRnMustBeLifted {}
+      -> ErrorWithoutFlag
 
   diagnosticHints = \case
     TcRnUnknownMessage m
@@ -1581,10 +1585,14 @@ instance Diagnostic TcRnMessage where
       -> noHints
     TcRnSpecialiseNotVisible name
       -> [SuggestSpecialiseVisibilityHints name]
-    TcRnNameByTemplateHaskellQuote{} -> noHints
-    TcRnIllegalBindingOfBuiltIn{} -> noHints
-    TcRnPragmaWarning{} -> noHints
-
+    TcRnNameByTemplateHaskellQuote{}
+      -> noHints
+    TcRnIllegalBindingOfBuiltIn{}
+      -> noHints
+    TcRnPragmaWarning{}
+      -> noHints
+    TcRnMustBeLifted {}
+      -> noHints
 
 -- | Change [x] to "x", [x, y] to "x and y", [x, y, z] to "x, y, and z",
 -- and so on.  The `and` stands for any `conjunction`, which is passed in.
@@ -1597,6 +1605,7 @@ commafyWith conjunction xs = addConjunction $ punctuate comma xs
           addConjunction (x : xs) = x : addConjunction xs
           addConjunction _ = panic "commafyWith expected 2 or more elements"
 
+
 deriveInstanceErrReasonHints :: Class
                              -> UsingGeneralizedNewtypeDeriving
                              -> DeriveInstanceErrReason
@@ -2228,7 +2237,8 @@ pprTcSolverReportMsg _ (FixedRuntimeRepError frr_origs) =
           = quotes (text "Levity")
           | otherwise
           = text "type"
-
+pprTcSolverReportMsg _ (NotLiftedError reason id) =
+  pprMustBeLiftedError reason (id :| [])
 pprTcSolverReportMsg _ (SkolemEscape item implic esc_skols) =
   let
     esc_doc = sep [ text "because" <+> what <+> text "variable" <> plural esc_skols
@@ -2497,6 +2507,25 @@ pprTcSolverReportMsg _ (UnsafeOverlap item matches unsafe_overlapped) =
     pred        = errorItemPred item
     (clas, tys) = getClassPredTys pred
 
+-- | Pretty-print an error when an 'Id' that is required to be lifted
+-- does not have a lifted type.
+pprMustBeLiftedError :: MustBeLiftedReason -> NonEmpty Id -> SDoc
+pprMustBeLiftedError ctxt (NE.toList -> bad_ids) =
+  vcat
+    ( hsep [ text "Expected" <+> what <> comma
+           , text "but the following variable" <> plural bad_ids <+> isOrAre bad_ids <+> text "unlifted:" ]
+    : map ppr_id bad_ids ++ [info] )
+  where
+    what :: SDoc
+    what = case bad_ids of { [_] -> text "a lifted variable"; _ -> text "lifted variables"}
+    ppr_id :: Id -> SDoc
+    ppr_id v = bullet <+> ppr v <+> dcolon <+> ppr ty <+> dcolon <+> ppr ki
+      where
+        ty = idType v
+        ki = typeKind ty
+    info :: SDoc
+    info = text "NB: variables used in" <+> ppr ctxt <> text "s" <+> text "must be lifted."
+
 {- *********************************************************************
 *                                                                      *
                  Displaying potential instances
diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs
index e8c3c6e411..4b8056b2a8 100644
--- a/compiler/GHC/Tc/Errors/Types.hs
+++ b/compiler/GHC/Tc/Errors/Types.hs
@@ -41,6 +41,7 @@ module GHC.Tc.Errors.Types (
   , Exported(..)
   , HsDocContext(..)
   , FixedRuntimeRepErrorInfo(..)
+  , MustBeLiftedReason(..)
 
   , ErrorItem(..), errorItemOrigin, errorItemEqRel, errorItemPred, errorItemCtLoc
 
@@ -2175,6 +2176,15 @@ data TcRnMessage where
     pragma_warning_defined_mod :: ModuleName
   } -> TcRnMessage
 
+  {-| TcRnMustBeLifted is an error that occurs when an 'Id' has an unlifted type,
+      even though it appears in a context which requires it to be lifted, for example
+      because we want to put a variable with that 'Id' into a boxed tuple.
+
+      Test cases: T20864, T20855.
+  -}
+  TcRnMustBeLifted :: MustBeLiftedReason -> NE.NonEmpty Id -> TcRnMessage
+
+
 -- | Specifies which back ends can handle a requested foreign import or export
 type ExpectedBackends = [Backend]
 
@@ -2807,6 +2817,14 @@ data TcSolverReportMsg
    -- See 'FixedRuntimeRepErrorInfo' and 'FixedRuntimeRepContext' for more information.
   | FixedRuntimeRepError [FixedRuntimeRepErrorInfo]
 
+  -- | The type of an 'Id' should have been lifted, but wasn't.
+  --
+  -- Used when we want to put 'Id's into a big tuple for desugaring parallel and transform
+  -- list comprehensions.
+  --
+  -- Test cases: T20864, T20855.
+  | NotLiftedError MustBeLiftedReason Id
+
   -- | A skolem type variable escapes its scope.
   --
   -- Example:
diff --git a/compiler/GHC/Tc/Gen/Arrow.hs b/compiler/GHC/Tc/Gen/Arrow.hs
index 6e4166d36d..83c1f3b211 100644
--- a/compiler/GHC/Tc/Gen/Arrow.hs
+++ b/compiler/GHC/Tc/Gen/Arrow.hs
@@ -438,7 +438,7 @@ tcArrDoStmt env ctxt (RecStmt { recS_stmts = L l stmts, recS_later_ids = later_n
                 --      (see Note [How RecStmt works] in Language.Haskell.Syntax.Expr)
 
         ; let rec_ids = takeList rec_names tup_ids
-        ; later_ids <- tcLookupLocalIds later_names
+        ; later_ids <- lookupBigTupIds ArrowRecStmtMustBeLifted later_names
 
         ; let rec_rets = takeList rec_names tup_rets
         ; let ret_table = zip tup_ids tup_rets
diff --git a/compiler/GHC/Tc/Gen/Match.hs b/compiler/GHC/Tc/Gen/Match.hs
index e1a0c2401b..776bda1f00 100644
--- a/compiler/GHC/Tc/Gen/Match.hs
+++ b/compiler/GHC/Tc/Gen/Match.hs
@@ -32,6 +32,8 @@ module GHC.Tc.Gen.Match
    , tcDoStmt
    , tcGuardStmt
    , checkPatCounts
+
+   , lookupBigTupIds
    )
 where
 
@@ -50,7 +52,7 @@ import GHC.Tc.Gen.Head( tcCheckId )
 import GHC.Tc.Utils.TcMType
 import GHC.Tc.Utils.TcType
 import GHC.Tc.Gen.Bind
-import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep_syntactic )
+import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep_syntactic, unifyTypeRuntimeRep_syntactic )
 import GHC.Tc.Utils.Unify
 import GHC.Tc.Types.Origin
 import GHC.Tc.Types.Evidence
@@ -494,7 +496,7 @@ tcLcStmt m_tc ctxt (ParStmt _ bndr_stmts_s _ _) elt_ty thing_inside
     loop (ParStmtBlock x stmts names _ : pairs)
       = do { (stmts', (ids, pairs', thing))
                 <- tcStmtsAndThen ctxt (tcLcStmt m_tc) stmts elt_ty $ \ _elt_ty' ->
-                   do { ids <- tcLookupLocalIds names
+                   do { ids <- lookupBigTupIds ParStmtMustBeLifted names
                       ; (pairs', thing) <- loop pairs
                       ; return (ids, pairs', thing) }
            ; return ( ParStmtBlock x stmts' ids noSyntaxExpr : pairs', thing ) }
@@ -509,7 +511,7 @@ tcLcStmt m_tc ctxt (TransStmt { trS_form = form, trS_stmts = stmts
        ; (stmts', (bndr_ids, by'))
             <- tcStmtsAndThen (TransStmtCtxt ctxt) (tcLcStmt m_tc) stmts unused_ty $ \_ -> do
                { by' <- traverse tcInferRho by
-               ; bndr_ids <- tcLookupLocalIds bndr_names
+               ; bndr_ids <- lookupBigTupIds TransStmtMustBeLifted bndr_names
                ; return (bndr_ids, by') }
 
        ; let m_app ty = mkTyConApp m_tc [ty]
@@ -546,7 +548,7 @@ tcLcStmt m_tc ctxt (TransStmt { trS_form = form, trS_stmts = stmts
 
              -- Ensure that every old binder of type `b` is linked up with its
              -- new binder which should have type `n b`
-             -- See Note [TransStmt binder map] in GHC.Hs.Expr
+             -- See Note [TransStmt binder map] in Language.Haskell.Syntax.Expr
              n_bndr_ids  = zipWith mk_n_bndr n_bndr_names bndr_ids
              bindersMap' = bndr_ids `zip` n_bndr_ids
 
@@ -699,7 +701,7 @@ tcMcStmt ctxt (TransStmt { trS_stmts = stmts, trS_bndrs = bindersMap
                                          ; return (Just e') }
 
                 -- Find the Ids (and hence types) of all old binders
-                ; bndr_ids <- tcLookupLocalIds bndr_names
+                ; bndr_ids <- lookupBigTupIds TransStmtMustBeLifted bndr_names
 
                 -- 'return' is only used for the binders, so we know its type.
                 --   return :: (a,b,c,..) -> m (a,b,c,..)
@@ -739,7 +741,7 @@ tcMcStmt ctxt (TransStmt { trS_stmts = stmts, trS_bndrs = bindersMap
 
              -- Ensure that every old binder of type `b` is linked up with its
              -- new binder which should have type `n b`
-             -- See Note [TransStmt binder map] in GHC.Hs.Expr
+             -- See Note [TransStmt binder map] in Language.Haskell.Syntax.Expr
              n_bndr_ids = zipWithEqual "tcMcStmt" mk_n_bndr n_bndr_names bndr_ids
              bindersMap' = bndr_ids `zip` n_bndr_ids
 
@@ -831,7 +833,7 @@ tcMcStmt ctxt (ParStmt _ bndr_stmts_s mzip_op bind_op) res_ty thing_inside
            ; (stmts', (ids, return_op', pairs', thing))
                 <- tcStmtsAndThen ctxt tcMcStmt stmts (mkCheckExpType m_tup_ty) $
                    \m_tup_ty' ->
-                   do { ids <- tcLookupLocalIds names
+                   do { ids <- lookupBigTupIds ParStmtMustBeLifted names
                       ; let tup_ty = mkBigCoreVarTupTy ids
                       ; (_, return_op') <-
                           tcSyntaxOp MCompOrigin return_op
@@ -949,7 +951,7 @@ tcDoStmt ctxt (RecStmt { recS_stmts = L l stmts, recS_later_ids = later_names
                   ; return (thing, new_res_ty) }
 
         ; let rec_ids = takeList rec_names tup_ids
-        ; later_ids <- tcLookupLocalIds later_names
+        ; later_ids <- lookupBigTupIds RecStmtMustBeLifted later_names
         ; traceTc "tcdo" $ vcat [ppr rec_ids <+> ppr (map idType rec_ids),
                                  ppr later_ids <+> ppr (map idType later_ids)]
         ; return (RecStmt { recS_stmts = L l stmts', recS_later_ids = later_ids
@@ -1168,3 +1170,74 @@ check_match_pats matchContext (MG { mg_alts = L _ (match1:matches) })
 
     args_in_match :: (LocatedA (Match GhcRn body1) -> Int)
     args_in_match (L _ (Match { m_pats = pats })) = length pats
+
+{-**********************************************************************
+*                                                                      *
+\subsection{Ensuring liftedness}
+*                                                                      *
+************************************************************************
+
+Note [Ensuring liftedness]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+Parallel list comprehensions and transform list comprehensions are
+desugared by using tuples, for example:
+
+  [ x + y1 + y2 | x <- xs, y1 <- ys | y2 <- ys ]
+
+    ==>
+
+  [ x + y1 + y2 | ((x,y1),y2) <- zip [ (x,y1) | x <- xs, y1 <- ys ] ys ].
+
+Such a desugaring only works if we can indeed put x, y1, y2 into tuples;
+in particular, they must be lifted.
+
+This means that, when typechecking this parallel list comprehension, we need
+to ensure that the Ids 'x', 'y1' and 'y2' are lifted. (Failing to do so
+caused #20864 and #20855.)
+
+  (1)
+    The Ids are already known to have a syntactically fixed RuntimeRep,
+    in the sense of Note [Fixed RuntimeRep].
+    That is, we have already performed a representation-polymorphism
+    check elsewhere in the program. This check might well have been
+    a PHASE 2 check that produced a coercion. See
+    Note [The Concrete mechanism].
+
+  (2)
+    We thus need to check that the RuntimeRep of each Id is LiftedRep.
+    A syntactic check suffices, as we have already handled all rewriting
+    in (1). In particular, if we decided to perform unification
+
+      co <- unifyKind rep liftedRepTy
+
+    the resulting coercion, co, would be rather useless: it would always be
+    either reflexive or a deferred type error. We would then have to find
+    a good place to store this coercion in the AST, which would involve
+    changing a fair bit of the parallel/transform list comprehension code,
+    for no real benefit.
+
+As a result, it is best to do a simple syntactic check, which is achieved
+by the function unifyTypeRuntimeRep_syntactic in GHC.Tc.Utils.Concrete.
+-}
+
+-- | Given a list of binder names, this function:
+--
+--  - looks up the associated local 'Id's using 'tcLookupLocalIds'
+--  - ensures their types are all lifted, throwing an error in the 'TcM' monad
+--    if this is not the case.
+lookupBigTupIds :: MustBeLiftedReason -> [Name] -> TcM [TcId]
+lookupBigTupIds lifted_reason names
+  = do { ids <- tcLookupLocalIds names
+       ; bad_ids <- filterM not_lifted ids
+       ; case bad_ids of
+           []       -> return ids
+           bad:bads -> failWithTc (TcRnMustBeLifted lifted_reason (bad NE.:| bads)) }
+
+  where
+    not_lifted :: TcId -> TcM Bool
+    not_lifted v
+      = do { is_lifted <- unifyTypeRuntimeRep_syntactic ty liftedRepTy
+               -- See Note [Ensuring liftedness].
+           ; return $ not is_lifted }
+      where
+        ty = idType v
diff --git a/compiler/GHC/Tc/Utils/Concrete.hs b/compiler/GHC/Tc/Utils/Concrete.hs
index da9efb7ef3..01e95c18c7 100644
--- a/compiler/GHC/Tc/Utils/Concrete.hs
+++ b/compiler/GHC/Tc/Utils/Concrete.hs
@@ -11,6 +11,9 @@ module GHC.Tc.Utils.Concrete
 
     -- * Making a type concrete
   , makeTypeConcrete
+
+    -- * Syntactic unification of concrete types
+  , unifyTypeRuntimeRep_syntactic, unifyConcrete_syntactic,
   )
  where
 
@@ -18,27 +21,33 @@ import GHC.Prelude
 
 import GHC.Builtin.Types       ( liftedTypeKindTyCon, unliftedTypeKindTyCon )
 
-import GHC.Core.Coercion       ( coToMCo, mkCastTyMCo )
+import GHC.Core.Coercion       ( coToMCo, mkCastTyMCo, isReflexiveCo )
 import GHC.Core.TyCo.Rep       ( Type(..), MCoercion(..) )
 import GHC.Core.TyCon          ( isConcreteTyCon )
 import GHC.Core.Type           ( isConcrete, typeKind, tyVarKind, tcView
-                               , mkTyVarTy, mkTyConApp, mkFunTy, mkAppTy )
-
+                               , mkTyVarTy, mkTyConApp, mkFunTy, mkAppTy
+                               , getRuntimeRep )
 import GHC.Tc.Types            ( TcM, ThStage(..), PendingStuff(..) )
-import GHC.Tc.Types.Constraint ( NotConcreteError(..), NotConcreteReason(..) )
+import GHC.Tc.Types.Constraint ( NotConcreteError(..), NotConcreteReason(..)
+                               , isEmptyWC )
 import GHC.Tc.Types.Evidence   ( Role(..), TcCoercionN, TcMCoercionN
                                , mkTcGReflRightMCo, mkTcNomReflCo )
-import GHC.Tc.Types.Origin     ( CtOrigin(..), FixedRuntimeRepContext, FixedRuntimeRepOrigin(..) )
-import GHC.Tc.Utils.Monad      ( emitNotConcreteError, setTcLevel, getCtLocM, getStage, traceTc )
+import GHC.Tc.Types.Origin     ( CtOrigin(..), FixedRuntimeRepContext, FixedRuntimeRepOrigin(..)
+                               , TypedThing(..) )
+import GHC.Tc.Utils.Monad      ( emitNotConcreteError, setTcLevel, getCtLocM, getStage, traceTc
+                               , captureConstraints )
 import GHC.Tc.Utils.TcType     ( TcType, TcKind, TcTypeFRR
                                , MetaInfo(..), ConcreteTvOrigin(..)
-                               , isMetaTyVar, metaTyVarInfo, tcTyVarLevel )
+                               , isMetaTyVar, metaTyVarInfo, tcTyVarLevel
+                               , tcEqType )
 import GHC.Tc.Utils.TcMType    ( newConcreteTyVar, isFilledMetaTyVar_maybe, writeMetaTyVar
                                , emitWantedEq )
+import {-# SOURCE #-} GHC.Tc.Utils.Unify ( unifyKind )
 
 import GHC.Types.Basic         ( TypeOrKind(..) )
 import GHC.Utils.Misc          ( HasDebugCallStack )
 import GHC.Utils.Outputable
+import GHC.Utils.Panic
 
 import Control.Monad      ( void )
 import Data.Functor       ( ($>) )
@@ -682,3 +691,92 @@ makeTypeConcrete conc_orig ty =
 
     bale_out :: TcType -> NotConcreteReason -> WriterT [NotConcreteReason] TcM TcType
     bale_out ty reason = do { tell [reason]; return ty }
+
+
+{-
+%************************************************************************
+%*                                                                      *
+                       Syntactic unification
+%*                                                                      *
+%**********************************************************************-}
+
+
+-- | Given a type @ty :: TYPE rr@ and a desired 'RuntimeRep' @desired_rr@,
+-- this function attempts to syntactically unify @rr@ with @desired_rr@,
+-- returning whether it succeeded.
+--
+-- Preconditions:
+--   - The kind of @ty@ must be of the form @TYPE rr@.
+--   - Both @rr@ and @desired_rr@ are concrete 'RuntimeRep's,
+--     in the sense of Note [Concrete types].
+unifyTypeRuntimeRep_syntactic :: HasDebugCallStack
+                              => TcType -- ^ type to constrain (e.g. @ty :: TYPE rr@)
+                              -> TcType -- ^ desired 'RuntimeRep' (e.g. 'liftedRepTy')
+                              -> TcM Bool
+unifyTypeRuntimeRep_syntactic ty desired_rr
+  = do { res <- unifyConcrete_syntactic rr desired_rr
+          -- NB: unifyConcrete_syntactic asserts that both arguments are concrete,
+          -- so no need to assert that here.
+       ; traceTc "unifyTypeRuntimeRep_syntatic" $
+          vcat [ text "ty:" <+> ppr ty
+               , text "rr:" <+> ppr rr
+               , text "desired_rr:" <+> ppr desired_rr
+               , text "OK:" <+> ppr res ]
+       ; return res }
+  where
+    rr = getRuntimeRep ty
+
+-- | Syntactically unify two concrete types. Looks through filled metavariables,
+-- but does not do any rewriting, nor does it ever defer work to the
+-- constraint solver (this function never emits any constraints).
+--
+-- Preconditions:
+--    - The LHS and RHS types are both concrete, in the sense of
+--      Note [Concrete types] in GHC.Tc.Utils.Concrete.
+--    - The kinds of LHS and RHS are equal (according to 'tcEqType').
+unifyConcrete_syntactic :: HasDebugCallStack => TcType -> TcType -> TcM Bool
+unifyConcrete_syntactic ty desired_ty
+  = do { massertPpr (conc1 && conc2) $
+           vcat [ text "unifyConcrete_syntactic: non-concrete" <+> what_not_conc
+                , text "LHS:" <+> ppr ty
+                , text "RHS:" <+> ppr desired_ty ]
+       ; massertPpr (ki1 `tcEqType` ki2) $
+           vcat [ text "unifyConcrete_syntactic: kind mismatch"
+                , text "LHS:" <+> ppr ty <+> dcolon <+> ppr ki1
+                , text "RHS:" <+> ppr desired_ty <+> dcolon <+> ppr ki2 ]
+       ; (co, wc) <- captureConstraints $ unifyKind (Just $ TypeThing desired_ty) ty desired_ty
+       ; traceTc "unifyConcrete_syntactic" $
+            vcat [ text "ty:" <+> ppr ty
+                 , text "desired_ty:" <+> ppr desired_ty
+                 , text "co:" <+> ppr co
+                 , text "wc:" <+> ppr wc ]
+
+       ; if not $ isEmptyWC wc
+
+         -- There were unsolved constraints, perhaps something like `IntRep ~# LiftedRep`.
+         then return False
+
+         -- No unsolved constraints: we expect evidence for the equality to be Refl,
+         -- as both sides are concrete.
+         else
+    do { massertPpr (isReflexiveCo co) $
+           vcat [ text "unifyConcrete_syntactic: unification succeeded with non-reflexive coercion"
+                , text "ty:" <+> ppr ty
+                , text "desired_ty:" <+> ppr desired_ty
+                , text "co:" <+> ppr co ]
+       ; return True } }
+  where
+    ki1, ki2 :: TcKind
+    ki1 = typeKind ty
+    ki2 = typeKind desired_ty
+    conc1, conc2 :: Bool
+    conc1 = isConcrete ty
+    conc2 = isConcrete desired_ty
+    what_not_conc :: SDoc
+    what_not_conc
+      | not conc1 && not conc2
+      = text "LHS and RHS"
+      | not conc1
+      = text "LHS"
+      | otherwise
+      = text "RHS"
diff --git a/compiler/GHC/Types/Basic.hs b/compiler/GHC/Types/Basic.hs
index 027fe63bad..c5f2f786ed 100644
--- a/compiler/GHC/Types/Basic.hs
+++ b/compiler/GHC/Types/Basic.hs
@@ -105,6 +105,7 @@ module GHC.Types.Basic (
         TypeOrKind(..), isTypeLevel, isKindLevel,
 
         Levity(..), mightBeLifted, mightBeUnlifted,
+        MustBeLiftedReason(..),
 
         NonStandardDefaultingStrategy(..),
         DefaultingStrategy(..), defaultNonStandardTyVars,
@@ -1898,6 +1899,18 @@ mightBeUnlifted :: Maybe Levity -> Bool
 mightBeUnlifted (Just Lifted) = False
 mightBeUnlifted _             = True
 
+data MustBeLiftedReason
+  = ParStmtMustBeLifted
+  | TransStmtMustBeLifted
+  | RecStmtMustBeLifted
+  | ArrowRecStmtMustBeLifted
+
+instance Outputable MustBeLiftedReason where
+  ppr ParStmtMustBeLifted      = text "parallel list comprehension"
+  ppr TransStmtMustBeLifted    = text "transform list comprehension"
+  ppr RecStmtMustBeLifted      = text "recursive statement"
+  ppr ArrowRecStmtMustBeLifted = text "arrow recursive statement"
+
 {- *********************************************************************
 *                                                                      *
                         Defaulting options
diff --git a/testsuite/tests/typecheck/should_compile/T20855b.hs b/testsuite/tests/typecheck/should_compile/T20855b.hs
new file mode 100644
index 0000000000..3b33971736
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T20855b.hs
@@ -0,0 +1,40 @@
+{-# language Haskell2010
+           , AllowAmbiguousTypes
+           , DataKinds
+           , ParallelListComp
+           , PolyKinds
+           , ScopedTypeVariables
+           , StandaloneKindSignatures
+           , TypeApplications
+           , TypeFamilies
+           , UnliftedNewtypes #-}
+
+module T20855b where
+
+import Data.Kind ( Constraint, Type )
+import GHC.Exts ( TYPE, RuntimeRep(..), LiftedRep )
+
+type R :: Type -> RuntimeRep
+type family R a where
+  R Bool = IntRep
+  R ()   = LiftedRep
+
+type C :: Type -> Constraint
+class C a where
+  type T a :: TYPE (R a)
+  foo :: [D a] -> T a
+
+instance C () where
+  type T () = Int
+  foo ds = sum . take 5 . drop (10^7)
+        $ [ (a + b)
+          | a <- [ bar () .. ]
+          | MkD b <- ds ]
+
+data family D a
+data instance D () = MkD (T ())
+
+bar :: () -> T ()
+bar _ = 10
+
+main = print $ foo @() (map MkD [ bar () .. ])
diff --git a/testsuite/tests/typecheck/should_compile/T20864.hs b/testsuite/tests/typecheck/should_compile/T20864.hs
new file mode 100644
index 0000000000..2324091b63
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T20864.hs
@@ -0,0 +1,26 @@
+{-# language MagicHash, TransformListComp, GADTs, TypeFamilies, PolyKinds, DataKinds #-}
+{-# language PartialTypeSignatures, NamedWildCards, UnliftedNewtypes #-}
+
+module T20864 where
+
+import Data.Kind
+import GHC.Exts
+
+loom :: [Int] -> [Int]
+loom xs = [z | I# x <- xs, let p = x +# 3#, z <- [1 .. I# p], then take 3]
+
+type R :: Type -> RuntimeRep
+type family R a where
+  R Int = LiftedRep
+
+class C a where
+  type T a :: TYPE (R a)
+  data D a :: Type
+  cool :: [D a] -> [D a]
+
+instance C Int where
+  type T Int = Int
+  data D Int = MkD (T Int)
+  -- this one requires type-family reduction in the kind to observe liftedness
+  cool :: [D Int] -> [D Int]
+  cool xs = [MkD (x + 1612) | MkD x <- xs, then take 3]
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 62edaf99e6..afdeda7cb5 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -843,3 +843,5 @@ test('T18802', normal, compile, [''])
 test('T18802b', normal, compile, [''])
 test('T21289', normal, compile, [''])
 test('HardRecordUpdate', normal, compile, [''])
+test('T20864', normal, compile, [''])
+test('T20855b', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T20855.hs b/testsuite/tests/typecheck/should_fail/T20855.hs
new file mode 100644
index 0000000000..1af4a8590b
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T20855.hs
@@ -0,0 +1,14 @@
+{-# language Haskell2010, ParallelListComp, MagicHash #-}
+
+module T20855 where
+
+import GHC.Exts
+
+gore :: [Maybe Int] -> [Int] -> [Int]
+gore xs ys =
+  [ I# (x +# y)
+  | Just (I# x) <- xs
+  | I# y <- ys
+  ]
+
+main = print $ take 5 . drop (10^7) $ gore [Just i | i <- [1..]] [10..]
diff --git a/testsuite/tests/typecheck/should_fail/T20855.stderr b/testsuite/tests/typecheck/should_fail/T20855.stderr
new file mode 100644
index 0000000000..e6d519eea2
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T20855.stderr
@@ -0,0 +1,10 @@
+
+T20855.hs:10:14: error:
+    • Expected a lifted variable, but the following variable is unlifted:
+      • x :: Int# :: TYPE 'IntRep
+      NB: variables used in parallel list comprehensions must be lifted.
+    • In a stmt of a list comprehension:
+        Just (I# x) <- xs |  I# y <- ys
+      In the expression: [I# (x +# y) | Just (I# x) <- xs |  I# y <- ys]
+      In an equation for ‘gore’:
+          gore xs ys = [I# (x +# y) | Just (I# x) <- xs |  I# y <- ys]
diff --git a/testsuite/tests/typecheck/should_fail/T20855c.hs b/testsuite/tests/typecheck/should_fail/T20855c.hs
new file mode 100644
index 0000000000..b6be82b687
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T20855c.hs
@@ -0,0 +1,15 @@
+{-# language Haskell2010, ParallelListComp, MagicHash, DataKinds #-}
+
+module T20855c where
+
+import GHC.Exts
+
+gore :: (IntRep ~ LiftedRep) => [Maybe Int] -> [Int] -> [Int]
+gore xs ys =
+  [ I# (x +# y)
+  | Just (I# x) <- xs
+  | I# y <- ys
+  ]
+
+main :: (IntRep ~ LiftedRep) => IO ()
+main = print $ take 5 . drop (10^7) $ gore [Just i | i <- [1..]] [10..]
diff --git a/testsuite/tests/typecheck/should_fail/T20855c.stderr b/testsuite/tests/typecheck/should_fail/T20855c.stderr
new file mode 100644
index 0000000000..e27e93071e
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T20855c.stderr
@@ -0,0 +1,10 @@
+
+T20855c.hs:10:14: error:
+    • Expected a lifted variable, but the following variable is unlifted:
+      • x :: Int# :: TYPE 'IntRep
+      NB: variables used in parallel list comprehensions must be lifted.
+    • In a stmt of a list comprehension:
+        Just (I# x) <- xs |  I# y <- ys
+      In the expression: [I# (x +# y) | Just (I# x) <- xs |  I# y <- ys]
+      In an equation for ‘gore’:
+          gore xs ys = [I# (x +# y) | Just (I# x) <- xs |  I# y <- ys]
diff --git a/testsuite/tests/typecheck/should_fail/T20864_fail.hs b/testsuite/tests/typecheck/should_fail/T20864_fail.hs
new file mode 100644
index 0000000000..3ed49b82f8
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T20864_fail.hs
@@ -0,0 +1,16 @@
+{-# language MagicHash, TransformListComp, GADTs, TypeFamilies #-}
+module T20864_fail where
+import GHC.Exts
+
+type family F a where
+  F a = Int#
+
+data Foo a where
+  Foo :: F a -> F a -> Foo a
+
+-- These fail
+glum2 :: [Foo Int] -> [Int]
+glum2 xs = [I# (x +# y) | Foo x y <- xs, then take 3]
+
+glum :: [Int] -> [Int]
+glum xs = [I# p | I# x <- xs, let p = x +# 3#, then take 3]
diff --git a/testsuite/tests/typecheck/should_fail/T20864_fail.stderr b/testsuite/tests/typecheck/should_fail/T20864_fail.stderr
new file mode 100644
index 0000000000..29c6224038
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T20864_fail.stderr
@@ -0,0 +1,20 @@
+
+T20864_fail.hs:13:33: error:
+    • Expected lifted variables, but the following variables are unlifted:
+      • x :: F Int :: TYPE 'IntRep
+      • y :: F Int :: TYPE 'IntRep
+      NB: variables used in transform list comprehensions must be lifted.
+    • In a stmt of a list comprehension: then take 3
+      In the expression: [I# (x +# y) | Foo x y <- xs, then take 3]
+      In an equation for ‘glum2’:
+          glum2 xs = [I# (x +# y) | Foo x y <- xs, then take 3]
+
+T20864_fail.hs:16:22: error:
+    • Expected a lifted variable, but the following variable is unlifted:
+      • p :: Int# :: TYPE 'IntRep
+      NB: variables used in transform list comprehensions must be lifted.
+    • In a stmt of a list comprehension: then take 3
+      In the expression:
+        [I# p | I# x <- xs, let p = x +# 3#, then take 3]
+      In an equation for ‘glum’:
+          glum xs = [I# p | I# x <- xs, let p = x +# 3#, then take 3]
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 457e0c5bc1..6892300780 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -657,3 +657,6 @@ test('T20768_fail', normal, compile_fail, [''])
 test('T21327', normal, compile_fail, [''])
 test('T21338', normal, compile_fail, [''])
 test('T21158', normal, compile_fail, [''])
+test('T20855', normal, compile_fail, ['-fdefer-type-errors'])
+test('T20855c', normal, compile_fail, ['-fdefer-type-errors'])
+test('T20864_fail', normal, compile_fail, ['-fdefer-type-errors'])