diff options
| -rw-r--r-- | compiler/GHC/Rename/Expr.hs | 2 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Errors.hs | 23 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Errors/Ppr.hs | 41 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Errors/Types.hs | 18 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Gen/Arrow.hs | 2 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Gen/Match.hs | 89 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/Concrete.hs | 112 | ||||
| -rw-r--r-- | compiler/GHC/Types/Basic.hs | 13 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_compile/T20855b.hs | 40 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_compile/T20864.hs | 26 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_compile/all.T | 2 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_fail/T20855.hs | 14 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_fail/T20855.stderr | 10 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_fail/T20855c.hs | 15 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_fail/T20855c.stderr | 10 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_fail/T20864_fail.hs | 16 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_fail/T20864_fail.stderr | 20 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_fail/all.T | 3 |
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']) |