diff options
Diffstat (limited to 'compiler/GHC/Tc/Gen')
-rw-r--r-- | compiler/GHC/Tc/Gen/App.hs | 246 | ||||
-rw-r--r-- | compiler/GHC/Tc/Gen/Arrow.hs | 32 | ||||
-rw-r--r-- | compiler/GHC/Tc/Gen/Bind.hs | 11 | ||||
-rw-r--r-- | compiler/GHC/Tc/Gen/Expr.hs | 42 | ||||
-rw-r--r-- | compiler/GHC/Tc/Gen/Head.hs | 32 | ||||
-rw-r--r-- | compiler/GHC/Tc/Gen/Match.hs | 44 | ||||
-rw-r--r-- | compiler/GHC/Tc/Gen/Pat.hs | 12 | ||||
-rw-r--r-- | compiler/GHC/Tc/Gen/Rule.hs | 17 | ||||
-rw-r--r-- | compiler/GHC/Tc/Gen/Sig.hs | 17 |
9 files changed, 398 insertions, 55 deletions
diff --git a/compiler/GHC/Tc/Gen/App.hs b/compiler/GHC/Tc/Gen/App.hs index cc0814cced..22454d1acc 100644 --- a/compiler/GHC/Tc/Gen/App.hs +++ b/compiler/GHC/Tc/Gen/App.hs @@ -2,6 +2,7 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} -- Wrinkle in Note [Trees That Grow] @@ -21,13 +22,21 @@ module GHC.Tc.Gen.App import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcPolyExpr ) -import GHC.Builtin.Types (multiplicityTy) +import GHC.Types.Basic ( Arity ) +import GHC.Types.Id ( idArity, idName, hasNoBinding ) +import GHC.Types.Name ( isWiredInName ) +import GHC.Types.Var +import GHC.Builtin.Types ( multiplicityTy ) +import GHC.Core.ConLike ( ConLike(..) ) +import GHC.Core.DataCon ( dataConRepArity + , isNewDataCon, isUnboxedSumDataCon, isUnboxedTupleDataCon ) import GHC.Tc.Gen.Head import GHC.Hs import GHC.Tc.Errors.Types import GHC.Tc.Utils.Monad import GHC.Tc.Utils.Unify import GHC.Tc.Utils.Instantiate +import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep ) import GHC.Tc.Instance.Family ( tcGetFamInstEnvs, tcLookupDataFamInst_maybe ) import GHC.Tc.Gen.HsType import GHC.Tc.Utils.TcMType @@ -317,6 +326,22 @@ tcApp rn_expr exp_res_ty ; do_ql <- wantQuickLook rn_fun ; (delta, inst_args, app_res_rho) <- tcInstFun do_ql True fun fun_sigma rn_args + -- Check for representation polymorphism in the case that + -- the head of the application is a primop or data constructor + -- which has argument types that are representation-polymorphic. + -- This amounts to checking that the leftover argument types, + -- up until the arity, are not representation-polymorphic, + -- so that we can perform eta-expansion later without introducing + -- representation-polymorphic binders. + -- + -- See Note [Checking for representation-polymorphic built-ins] + ; traceTc "tcApp FRR" $ + vcat + [ text "tc_fun =" <+> ppr tc_fun + , text "inst_args =" <+> ppr inst_args + , text "app_res_rho =" <+> ppr app_res_rho ] + ; hasFixedRuntimeRep_remainingValArgs inst_args app_res_rho tc_fun + -- Quick look at result ; app_res_rho <- if do_ql then quickLookResultType delta app_res_rho exp_res_ty @@ -353,14 +378,221 @@ tcApp rn_expr exp_res_ty -- Typecheck the value arguments ; tc_args <- tcValArgs do_ql inst_args - -- Reconstruct, with special case for tagToEnum# - ; tc_expr <- if isTagToEnum rn_fun - then tcTagToEnum tc_fun fun_ctxt tc_args app_res_rho - else return (rebuildHsApps tc_fun fun_ctxt tc_args) + -- Reconstruct, with a special cases for tagToEnum#. + ; tc_expr <- + if isTagToEnum rn_fun + then tcTagToEnum tc_fun fun_ctxt tc_args app_res_rho + else do return (rebuildHsApps tc_fun fun_ctxt tc_args) -- Wrap the result ; return (mkHsWrapCo res_co tc_expr) } +{- +Note [Checking for representation-polymorphic built-ins] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We cannot have representation-polymorphic or levity-polymorphic +function arguments. See Note [Representation polymorphism invariants] +in GHC.Core. That is checked by the calls to `hasFixedRuntimeRep ` in +`tcEValArg`. + +But some /built-in/ functions are representation-polymorphic. Users +can't define such Ids; they are all GHC built-ins or data +constructors. Specifically they are: + +1. A few wired-in Ids like unsafeCoerce#, with compulsory unfoldings. +2. Primops, such as raise# +3. Newtype constructors with `UnliftedNewtypes` that have + a representation-polymorphic argument. +4. Representation-polymorphic data constructors: unboxed tuples + and unboxed sums. + +For (1) consider + badId :: forall r (a :: TYPE r). a -> a + badId = unsafeCoerce# @r @r @a @a + +The wired-in function + unsafeCoerce# :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) + (a :: TYPE r1) (b :: TYPE r2). + a -> b +has a convenient but representation-polymorphic type. It has no +binding; instead it has a compulsory unfolding, after which we +would have + badId = /\r /\(a :: TYPE r). \(x::a). ...body of unsafeCorece#... +And this is no good because of that rep-poly \(x::a). So we want +to reject this. + +On the other hand + goodId :: forall (a :: Type). a -> a + goodId = unsafeCoerce# @LiftedRep @LiftedRep @a @a + +is absolutely fine, because after we inline the unfolding, the \(x::a) +is representation-monomorphic. + +Test cases: T14561, RepPolyWrappedVar2. + +For primops (2) the situation is similar; they are eta-expanded in +CorePrep to be saturated, and that eta-expansion must not add a +representation-polymorphic lambda. + +Test cases: T14561b, RepPolyWrappedVar, UnliftedNewtypesCoerceFail. + +For (3), consider a representation-polymorphic newtype with +UnliftedNewtypes: + + type Id :: forall r. TYPE r -> TYPE r + newtype Id a where { MkId :: a } + + bad :: forall r (a :: TYPE r). a -> Id a + bad = MkId @r @a -- Want to reject + + good :: forall (a :: Type). a -> Id a + good = MkId @LiftedRep @a -- Want to accept + +Test cases: T18481, UnliftedNewtypesLevityBinder + +So these three cases need special treatment. We add a special case +in tcApp to check whether an application of an Id has any remaining +representation-polymorphic arguments, after instantiation and application +of previous arguments. This is achieved by the hasFixedRuntimeRep_remainingValArgs +function, which computes the types of the remaining value arguments, and checks +that each of these have a fixed runtime representation using hasFixedRuntimeRep. + +Wrinkles + +* Because of Note [Typechecking data constructors] in GHC.Tc.Gen.Head, + we desugar a representation-polymorphic data constructor application + like this: + (/\(r :: RuntimeRep) (a :: TYPE r) \(x::a). K r a x) @LiftedRep Int 4 + That is, a rep-poly lambda applied to arguments that instantiate it in + a rep-mono way. It's a bit like a compulsory unfolding that has been + inlined, but not yet beta-reduced. + + Because we want to accept this, we switch off Lint's representation + polymorphism checks when Lint checks the output of the desugarer; + see the lf_check_fixed_repy flag in GHC.Core.Lint.lintCoreBindings. + +* Arity. We don't want to check for arguments past the + arity of the function. For example + + raise# :: forall {r :: RuntimeRep} (a :: Type) (b :: TYPE r). a -> b + + has arity 1, so an instantiation such as: + + foo :: forall w r (z :: TYPE r). w -> z -> z + foo = raise# @w @(z -> z) + + is unproblematic. This means we must take care not to perform a + representation-polymorphism check on `z`. + + To achieve this, we consult the arity of the 'Id' which is the head + of the application (or just use 1 for a newtype constructor), + and keep track of how many value-level arguments we have seen, + to ensure we stop checking once we reach the arity. + This is slightly complicated by the need to include both visible + and invisible arguments, as the arity counts both: + see GHC.Tc.Gen.Head.countVisAndInvisValArgs. + + Test cases: T20330{a,b} + +-} + +-- | Check for representation-polymorphism in the remaining argument types +-- of a variable or data constructor, after it has been instantiated and applied to some arguments. +-- +-- See Note [Checking for representation-polymorphic built-ins] +hasFixedRuntimeRep_remainingValArgs :: [HsExprArg 'TcpInst] -> TcRhoType -> HsExpr GhcTc -> TcM () +hasFixedRuntimeRep_remainingValArgs applied_args app_res_rho = \case + + HsVar _ (L _ fun_id) + + -- (1): unsafeCoerce# + -- 'unsafeCoerce#' is peculiar: it is patched in manually as per + -- Note [Wiring in unsafeCoerce#] in GHC.HsToCore. + -- Unfortunately, even though its arity is set to 1 in GHC.HsToCore.mkUnsafeCoercePrimPair, + -- at this stage, if we query idArity, we get 0. This is because + -- we end up looking at the non-patched version of unsafeCoerce# + -- defined in Unsafe.Coerce, and that one indeed has arity 0. + -- + -- We thus manually specify the correct arity of 1 here. + | idName fun_id == unsafeCoercePrimName + -> check_thing fun_id 1 (FRRNoBindingResArg fun_id) + + -- (2): primops and other wired-in representation-polymorphic functions, + -- such as 'rightSection', 'oneShot', etc; see bindings with Compulsory unfoldings + -- in GHC.Types.Id.Make + | isWiredInName (idName fun_id) && hasNoBinding fun_id + -> check_thing fun_id (idArity fun_id) (FRRNoBindingResArg fun_id) + -- NB: idArity consults the IdInfo of the Id. This can be a problem + -- in the presence of hs-boot files, as we might not have finished + -- typechecking; inspecting the IdInfo at this point can cause + -- strange Core Lint errors (see #20447). + -- We avoid this entirely by only checking wired-in names, + -- as those are the only ones this check is applicable to anyway. + + + XExpr (ConLikeTc (RealDataCon con) _ _) + -- (3): Representation-polymorphic newtype constructors. + | isNewDataCon con + -- (4): Unboxed tuples and unboxed sums + || isUnboxedTupleDataCon con + || isUnboxedSumDataCon con + -> check_thing con (dataConRepArity con) (FRRDataConArg con) + + _ -> return () + + where + nb_applied_vis_val_args :: Int + nb_applied_vis_val_args = count isHsValArg applied_args + + nb_applied_val_args :: Int + nb_applied_val_args = countVisAndInvisValArgs applied_args + + arg_tys :: [TyCoBinder] + arg_tys = fst $ splitPiTys app_res_rho + -- We do not need to zonk app_res_rho first, because the number of arrows + -- in the (possibly instantiated) inferred type of the function will + -- be at least the arity of the function. + + check_thing :: Outputable thing => thing -> Arity -> (Int -> FRROrigin) -> TcM () + check_thing thing arity mk_frr_orig = do + traceTc "tcApp remainingValArgs check_thing" (debug_msg thing arity) + go (nb_applied_vis_val_args + 1) (nb_applied_val_args + 1) arg_tys + where + go :: Int -- ^ visible value argument index + -- (only used to report the argument position in error messages) + -> Int -- ^ value argument index + -- used to count up to the arity to ensure we don't check too many argument types + -> [TyCoBinder] + -> TcM () + go _ i_val _ + | i_val > arity + = return () + go _ _ [] + -- Should never happen: it would mean that the arity is higher + -- than the number of arguments apparent from the type + = pprPanic "hasFixedRuntimeRep_remainingValArgs" (debug_msg thing arity) + go i_visval !i_val (Anon af (Scaled _ arg_ty) : tys) + = case af of + InvisArg -> + go i_visval (i_val + 1) tys + VisArg -> do + _concrete_ev <- hasFixedRuntimeRep (mk_frr_orig i_visval) arg_ty + go (i_visval + 1) (i_val + 1) tys + go i_visval i_val (_: tys) + = go i_visval i_val tys + + -- A message containing all the relevant info, in case this functions + -- needs to be debugged again at some point. + debug_msg :: Outputable thing => thing -> Arity -> SDoc + debug_msg thing arity = + vcat + [ text "thing =" <+> ppr thing + , text "arity =" <+> ppr arity + , text "applied_args =" <+> ppr applied_args + , text "nb_applied_vis_val_args =" <+> ppr nb_applied_vis_val_args + , text "nb_applied_val_args =" <+> ppr nb_applied_val_args + , text "arg_tys =" <+> ppr arg_tys ] + -------------------- wantQuickLook :: HsExpr GhcRn -> TcM Bool -- GHC switches on impredicativity all the time for ($) @@ -438,9 +670,10 @@ tcEValArg :: AppCtxt -> EValArg 'TcpInst -> TcSigmaType -> TcM (LHsExpr GhcTc) tcEValArg ctxt (ValArg larg@(L arg_loc arg)) exp_arg_sigma = addArgCtxt ctxt larg $ do { arg' <- tcPolyExpr arg (mkCheckExpType exp_arg_sigma) + ; _concrete_ev <- hasFixedRuntimeRep (FRRApp arg) exp_arg_sigma ; return (L arg_loc arg') } -tcEValArg ctxt (ValArgQL { va_expr = larg@(L arg_loc _) +tcEValArg ctxt (ValArgQL { va_expr = larg@(L arg_loc arg) , va_fun = (inner_fun, fun_ctxt) , va_args = inner_args , va_ty = app_res_rho }) exp_arg_sigma @@ -448,6 +681,7 @@ tcEValArg ctxt (ValArgQL { va_expr = larg@(L arg_loc _) do { traceTc "tcEValArgQL {" (vcat [ ppr inner_fun <+> ppr inner_args ]) ; tc_args <- tcValArgs True inner_args ; co <- unifyType Nothing app_res_rho exp_arg_sigma + ; _concrete_ev <- hasFixedRuntimeRep (FRRApp arg) exp_arg_sigma ; traceTc "tcEValArg }" empty ; return (L arg_loc $ mkHsWrapCo co $ rebuildHsApps inner_fun fun_ctxt tc_args) } diff --git a/compiler/GHC/Tc/Gen/Arrow.hs b/compiler/GHC/Tc/Gen/Arrow.hs index 0d0e482b35..45e8f08a5e 100644 --- a/compiler/GHC/Tc/Gen/Arrow.hs +++ b/compiler/GHC/Tc/Gen/Arrow.hs @@ -22,6 +22,7 @@ import GHC.Hs.Syn.Type import GHC.Tc.Errors.Types import GHC.Tc.Gen.Match import GHC.Tc.Gen.Head( tcCheckId ) +import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep ) import GHC.Tc.Utils.TcType import GHC.Tc.Utils.TcMType import GHC.Tc.Gen.Bind @@ -91,13 +92,14 @@ tcProc :: LPat GhcRn -> LHsCmdTop GhcRn -- proc pat -> expr -> ExpRhoType -- Expected type of whole proc expression -> TcM (LPat GhcTc, LHsCmdTop GhcTc, TcCoercion) -tcProc pat cmd@(L _ (HsCmdTop names _)) exp_ty +tcProc pat cmd@(L loc (HsCmdTop names _)) exp_ty = do { exp_ty <- expTypeToType exp_ty -- no higher-rank stuff with arrows ; (co, (exp_ty1, res_ty)) <- matchExpectedAppTy exp_ty ; (co1, (arr_ty, arg_ty)) <- matchExpectedAppTy exp_ty1 -- start with the names as they are used to desugar the proc itself -- See #17423 - ; names' <- mapM (tcSyntaxName ProcOrigin arr_ty) names + ; names' <- setSrcSpan loc $ + mapM (tcSyntaxName ProcOrigin arr_ty) names ; let cmd_env = CmdEnv { cmd_arr = arr_ty } ; (pat', cmd') <- newArrowScope $ tcCheckPat (ArrowMatchCtxt ProcExpr) pat (unrestricted arg_ty) @@ -141,9 +143,10 @@ tcCmdTop env names (L loc (HsCmdTop _names cmd)) cmd_ty@(cmd_stk, res_ty) ---------------------------------------- tcCmd :: CmdEnv -> LHsCmd GhcRn -> CmdType -> TcM (LHsCmd GhcTc) -- The main recursive function -tcCmd env (L loc cmd) res_ty +tcCmd env (L loc cmd) cmd_ty@(_, res_ty) = setSrcSpan (locA loc) $ do - { cmd' <- tc_cmd env cmd res_ty + { cmd' <- tc_cmd env cmd cmd_ty + ; _concrete_ev <- hasFixedRuntimeRep (FRRArrow $ ArrowCmdResTy cmd) res_ty ; return (L loc cmd') } tc_cmd :: CmdEnv -> HsCmd GhcRn -> CmdType -> TcM (HsCmd GhcTc) @@ -219,6 +222,10 @@ tc_cmd env cmd@(HsCmdArrApp _ fun arg ho_app lr) (_, res_ty) ; arg' <- tcCheckMonoExpr arg arg_ty + ; _concrete_ev <- hasFixedRuntimeRep + (FRRArrow $ ArrowCmdArrApp (unLoc fun) (unLoc arg) ho_app) + fun_ty + ; return (HsCmdArrApp fun_ty fun' arg' ho_app lr) } where -- Before type-checking f, use the environment of the enclosing @@ -243,6 +250,9 @@ tc_cmd env cmd@(HsCmdApp x fun arg) (cmd_stk, res_ty) do { arg_ty <- newOpenFlexiTyVarTy ; fun' <- tcCmd env fun (mkPairTy arg_ty cmd_stk, res_ty) ; arg' <- tcCheckMonoExpr arg arg_ty + ; _concrete_ev <- hasFixedRuntimeRep + (FRRArrow $ ArrowCmdApp (unLoc fun) (unLoc arg)) + arg_ty ; return (HsCmdApp x fun' arg') } ------------------------------------------- @@ -271,6 +281,15 @@ tc_cmd env , m_pats = pats' , m_grhss = grhss' }) arg_tys = map (unrestricted . hsLPatType) pats' + + ; _concrete_evs <- + zipWithM + (\ (Scaled _ arg_ty) i -> + hasFixedRuntimeRep (FRRArrow $ ArrowCmdLam i) arg_ty) + arg_tys + [1..] + + ; let cmd' = HsCmdLam x (MG { mg_alts = L l [match'] , mg_ext = MatchGroupTc arg_tys res_ty , mg_origin = origin }) @@ -326,11 +345,12 @@ tc_cmd env cmd@(HsCmdArrForm x expr f fixity cmd_args) (cmd_stk, res_ty) where tc_cmd_arg :: LHsCmdTop GhcRn -> TcM (LHsCmdTop GhcTc, TcType) - tc_cmd_arg cmd@(L _ (HsCmdTop names _)) + tc_cmd_arg cmd@(L loc (HsCmdTop names _)) = do { arr_ty <- newFlexiTyVarTy arrowTyConKind ; stk_ty <- newFlexiTyVarTy liftedTypeKind ; res_ty <- newFlexiTyVarTy liftedTypeKind - ; names' <- mapM (tcSyntaxName ProcOrigin arr_ty) names + ; names' <- setSrcSpan loc $ + mapM (tcSyntaxName ArrowCmdOrigin arr_ty) names ; let env' = env { cmd_arr = arr_ty } ; cmd' <- tcCmdTop env' names' cmd (stk_ty, res_ty) ; return (cmd', mkCmdArrTy env' (mkPairTy alphaTy stk_ty) res_ty) } diff --git a/compiler/GHC/Tc/Gen/Bind.hs b/compiler/GHC/Tc/Gen/Bind.hs index e540e3db91..93fa9a7e2c 100644 --- a/compiler/GHC/Tc/Gen/Bind.hs +++ b/compiler/GHC/Tc/Gen/Bind.hs @@ -34,6 +34,7 @@ import GHC.Data.FastString import GHC.Hs import GHC.Tc.Errors.Types import GHC.Tc.Gen.Sig +import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep ) import GHC.Tc.Utils.Monad import GHC.Tc.Types.Origin import GHC.Tc.Utils.Env @@ -519,6 +520,11 @@ tcPolyBinds sig_fn prag_fn rec_group rec_tc closed bind_list InferGen mn -> tcPolyInfer rec_tc prag_fn sig_fn mn bind_list CheckGen lbind sig -> tcPolyCheck prag_fn sig lbind + ; _concrete_evs <- + mapM (\ poly_id -> + hasFixedRuntimeRep (FRRBinder $ idName poly_id) (idType poly_id)) + poly_ids + ; traceTc "} End of bindings for" (vcat [ ppr binder_names, ppr rec_group , vcat [ppr id <+> ppr (idType id) | id <- poly_ids] ]) @@ -1181,7 +1187,7 @@ tcMonoBinds :: RecFlag -- Whether the binding is recursive for typechecking pur -> [LHsBind GhcRn] -> TcM (LHsBinds GhcTc, [MonoBindInfo]) --- SPECIAL CASE 1: see Note [Inference for non-recursive function bindings] +-- SPECIAL CASE 1: see Note [Special case for non-recursive function bindings] tcMonoBinds is_rec sig_fn no_gen [ L b_loc (FunBind { fun_id = L nm_loc name , fun_matches = matches })] @@ -1210,7 +1216,7 @@ tcMonoBinds is_rec sig_fn no_gen , mbi_sig = Nothing , mbi_mono_id = mono_id }]) } --- SPECIAL CASE 2: see Note [Inference for non-recursive pattern bindings] +-- SPECIAL CASE 2: see Note [Special case for non-recursive pattern bindings] tcMonoBinds is_rec sig_fn no_gen [L b_loc (PatBind { pat_lhs = pat, pat_rhs = grhss })] | NonRecursive <- is_rec -- ...binder isn't mentioned in RHS @@ -1470,6 +1476,7 @@ tcRhs (TcPatBind infos pat' grhss pat_ty) do { traceTc "tcRhs: pat bind" (ppr pat' $$ ppr pat_ty) ; grhss' <- addErrCtxt (patMonoBindsCtxt pat' grhss) $ tcGRHSsPat grhss (mkCheckExpType pat_ty) + ; return ( PatBind { pat_lhs = pat', pat_rhs = grhss' , pat_ext = pat_ty , pat_ticks = ([],[]) } )} diff --git a/compiler/GHC/Tc/Gen/Expr.hs b/compiler/GHC/Tc/Gen/Expr.hs index 899a69353e..077414b96a 100644 --- a/compiler/GHC/Tc/Gen/Expr.hs +++ b/compiler/GHC/Tc/Gen/Expr.hs @@ -40,6 +40,7 @@ import GHC.Types.Error import GHC.Core.Multiplicity import GHC.Core.UsageEnv import GHC.Tc.Errors.Types +import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep, mkWpFun ) import GHC.Tc.Utils.Instantiate import GHC.Tc.Gen.App import GHC.Tc.Gen.Head @@ -344,7 +345,16 @@ tcExpr (ExplicitSum _ alt arity expr) res_ty ; (coi, arg_tys) <- matchExpectedTyConApp sum_tc res_ty ; -- Drop levity vars, we don't care about them here let arg_tys' = drop arity arg_tys - ; expr' <- tcCheckPolyExpr expr (arg_tys' `getNth` (alt - 1)) + arg_ty = arg_tys' `getNth` (alt - 1) + ; expr' <- tcCheckPolyExpr expr arg_ty + -- Check the whole res_ty, not just the arg_ty, to avoid #20277. + -- Example: + -- a :: TYPE rep (representation-polymorphic) + -- (# 17# | #) :: (# Int# | a #) + -- This should cause an error, even though (17# :: Int#) + -- is not representation-polymorphic: we don't know how + -- wide the concrete representation of the sum type will be. + ; _concrete_ev <- hasFixedRuntimeRep FRRUnboxedSum res_ty ; return $ mkHsWrapCo coi (ExplicitSum arg_tys' alt arity expr' ) } @@ -938,12 +948,17 @@ tcTupArgs :: [HsTupArg GhcRn] -> [TcSigmaType] -> TcM [HsTupArg GhcTc] tcTupArgs args tys = do massert (equalLength args tys) checkTupSize (length args) - mapM go (args `zip` tys) + zipWith3M go [1,2..] args tys where - go (Missing {}, arg_ty) = do { mult <- newFlexiTyVarTy multiplicityTy - ; return (Missing (Scaled mult arg_ty)) } - go (Present x expr, arg_ty) = do { expr' <- tcCheckPolyExpr expr arg_ty - ; return (Present x expr') } + go :: Int -> HsTupArg GhcRn -> TcType -> TcM (HsTupArg GhcTc) + go i (Missing {}) arg_ty + = do { mult <- newFlexiTyVarTy multiplicityTy + ; _concrete_ev <- hasFixedRuntimeRep (FRRTupleSection i) arg_ty + ; return (Missing (Scaled mult arg_ty)) } + go i (Present x expr) arg_ty + = do { expr' <- tcCheckPolyExpr expr arg_ty + ; _concrete_ev <- hasFixedRuntimeRep (FRRTupleArg i) arg_ty + ; return (Present x expr') } --------------------------- -- See TcType.SyntaxOpType also for commentary @@ -1003,8 +1018,8 @@ tcSynArgE :: CtOrigin -- ^ returns a wrapper :: (type of right shape) "->" (type passed in) tcSynArgE orig sigma_ty syn_ty thing_inside = do { (skol_wrap, (result, ty_wrapper)) - <- tcSkolemise GenSigCtxt sigma_ty $ \ rho_ty -> - go rho_ty syn_ty + <- tcSkolemise GenSigCtxt sigma_ty + (\ rho_ty -> go rho_ty syn_ty) ; return (result, skol_wrap <.> ty_wrapper) } where go rho_ty SynAny @@ -1046,13 +1061,11 @@ tcSynArgE orig sigma_ty syn_ty thing_inside do { result <- thing_inside (arg_results ++ res_results) ([arg_mult] ++ arg_res_mults ++ res_res_mults) ; return (result, arg_tc_ty, res_tc_ty, arg_mult) }} - ; return ( result - , match_wrapper <.> - mkWpFun (arg_wrapper2 <.> arg_wrapper1) res_wrapper - (Scaled op_mult arg_ty) res_ty doc ) } + ; fun_wrap <- mkWpFun (arg_wrapper2 <.> arg_wrapper1) res_wrapper + (Scaled op_mult arg_ty) res_ty (WpFunSyntaxOp orig) + ; return (result, match_wrapper <.> fun_wrap) } where herald = text "This rebindable syntax expects a function with" - doc = text "When checking a rebindable syntax operator arising from" <+> ppr orig go rho_ty (SynType the_ty) = do { wrap <- tcSubTypePat orig GenSigCtxt the_ty rho_ty @@ -1374,6 +1387,9 @@ tcRecordField con_like flds_w_tys (L loc (FieldOcc sel_name lbl)) rhs | Just field_ty <- assocMaybe flds_w_tys sel_name = addErrCtxt (fieldCtxt field_lbl) $ do { rhs' <- tcCheckPolyExprNC rhs field_ty + ; _concrete_ev <- + hasFixedRuntimeRep (FRRRecordUpdate (unLoc lbl) (unLoc rhs)) + field_ty ; let field_id = mkUserLocal (nameOccName sel_name) (nameUnique sel_name) Many field_ty loc diff --git a/compiler/GHC/Tc/Gen/Head.hs b/compiler/GHC/Tc/Gen/Head.hs index 78f9b0265a..bfaba5efcc 100644 --- a/compiler/GHC/Tc/Gen/Head.hs +++ b/compiler/GHC/Tc/Gen/Head.hs @@ -22,6 +22,7 @@ module GHC.Tc.Gen.Head , splitHsApps, rebuildHsApps , addArgWrap, isHsValArg , countLeadingValArgs, isVisibleArg, pprHsExprArgTc + , countVisAndInvisValArgs, countHsWrapperInvisArgs , tcInferAppHead, tcInferAppHead_maybe , tcInferId, tcCheckId @@ -75,6 +76,7 @@ import GHC.Types.SrcLoc import GHC.Utils.Misc import GHC.Data.Maybe import GHC.Utils.Outputable as Outputable +import GHC.Utils.Panic import GHC.Utils.Panic.Plain import Control.Monad @@ -323,6 +325,36 @@ isVisibleArg (EValArg {}) = True isVisibleArg (ETypeArg {}) = True isVisibleArg _ = False +-- | Count visible and invisible value arguments in a list +-- of 'HsExprArg' arguments. +countVisAndInvisValArgs :: [HsExprArg id] -> Arity +countVisAndInvisValArgs [] = 0 +countVisAndInvisValArgs (EValArg {} : args) = 1 + countVisAndInvisValArgs args +countVisAndInvisValArgs (EWrap wrap : args) = + case wrap of { EHsWrap hsWrap -> countHsWrapperInvisArgs hsWrap + countVisAndInvisValArgs args + ; EPar {} -> countVisAndInvisValArgs args + ; EExpand {} -> countVisAndInvisValArgs args } +countVisAndInvisValArgs (EPrag {} : args) = countVisAndInvisValArgs args +countVisAndInvisValArgs (ETypeArg {}: args) = countVisAndInvisValArgs args + +-- | Counts the number of invisible term-level arguments applied by an 'HsWrapper'. +-- Precondition: this wrapper contains no abstractions. +countHsWrapperInvisArgs :: HsWrapper -> Arity +countHsWrapperInvisArgs = go + where + go WpHole = 0 + go (WpCompose wrap1 wrap2) = go wrap1 + go wrap2 + go fun@(WpFun {}) = nope fun + go (WpCast {}) = 0 + go evLam@(WpEvLam {}) = nope evLam + go (WpEvApp _) = 1 + go tyLam@(WpTyLam {}) = nope tyLam + go (WpTyApp _) = 0 + go (WpLet _) = 0 + go (WpMultCoercion {}) = 0 + + nope x = pprPanic "countHsWrapperInvisApps" (ppr x) + instance OutputableBndrId (XPass p) => Outputable (HsExprArg p) where ppr (EValArg { eva_arg = arg }) = text "EValArg" <+> ppr arg ppr (EPrag _ p) = text "EPrag" <+> ppr p diff --git a/compiler/GHC/Tc/Gen/Match.hs b/compiler/GHC/Tc/Gen/Match.hs index c8eb8fd233..ab767b877c 100644 --- a/compiler/GHC/Tc/Gen/Match.hs +++ b/compiler/GHC/Tc/Gen/Match.hs @@ -49,6 +49,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 ) import GHC.Tc.Utils.Unify import GHC.Tc.Types.Origin import GHC.Tc.Types.Evidence @@ -226,6 +227,10 @@ tcMatches ctxt pat_tys rhs_ty (MG { mg_alts = L l matches = do { tcEmitBindingUsage bottomUE ; pat_tys <- mapM scaledExpTypeToType pat_tys ; rhs_ty <- expTypeToType rhs_ty + ; _concrete_evs <- zipWithM + (\ i (Scaled _ pat_ty) -> + hasFixedRuntimeRep (FRRMatch (mc_what ctxt) i) pat_ty) + [1..] pat_tys ; return (MG { mg_alts = L l [] , mg_ext = MatchGroupTc pat_tys rhs_ty , mg_origin = origin }) } @@ -236,6 +241,10 @@ tcMatches ctxt pat_tys rhs_ty (MG { mg_alts = L l matches ; tcEmitBindingUsage $ supUEs usages ; pat_tys <- mapM readScaledExpType pat_tys ; rhs_ty <- readExpType rhs_ty + ; _concrete_evs <- zipWithM + (\ i (Scaled _ pat_ty) -> + hasFixedRuntimeRep (FRRMatch (mc_what ctxt) i) pat_ty) + [1..] pat_tys ; return (MG { mg_alts = L l matches' , mg_ext = MatchGroupTc pat_tys rhs_ty , mg_origin = origin }) } @@ -431,6 +440,7 @@ tcGuardStmt ctxt (BindStmt _ pat rhs) res_ty thing_inside -- two multiplicity to still be the same. (rhs', rhs_ty) <- tcScalingUsage Many $ tcInferRhoNC rhs -- Stmt has a context already + ; _concrete_ev <- hasFixedRuntimeRep FRRBindStmtGuard rhs_ty ; (pat', thing) <- tcCheckPat_O (StmtCtxt ctxt) (lexprCtOrigin rhs) pat (unrestricted rhs_ty) $ thing_inside res_ty @@ -583,14 +593,16 @@ tcMcStmt _ (LastStmt x body noret return_op) res_ty thing_inside tcMcStmt ctxt (BindStmt xbsrn pat rhs) res_ty thing_inside -- (>>=) :: rhs_ty -> (pat_ty -> new_res_ty) -> res_ty - = do { ((rhs', pat_mult, pat', thing, new_res_ty), bind_op') + = do { ((rhs_ty, rhs', pat_mult, pat', thing, new_res_ty), bind_op') <- tcSyntaxOp MCompOrigin (xbsrn_bindOp xbsrn) [SynRho, SynFun SynAny SynRho] res_ty $ \ [rhs_ty, pat_ty, new_res_ty] [rhs_mult, fun_mult, pat_mult] -> do { rhs' <- tcScalingUsage rhs_mult $ tcCheckMonoExprNC rhs rhs_ty ; (pat', thing) <- tcScalingUsage fun_mult $ tcCheckPat (StmtCtxt ctxt) pat (Scaled pat_mult pat_ty) $ thing_inside (mkCheckExpType new_res_ty) - ; return (rhs', pat_mult, pat', thing, new_res_ty) } + ; return (rhs_ty, rhs', pat_mult, pat', thing, new_res_ty) } + + ; _concrete_ev <- hasFixedRuntimeRep (FRRBindStmt MonadComprehension) rhs_ty -- If (but only if) the pattern can fail, typecheck the 'fail' operator ; fail_op' <- fmap join . forM (xbsrn_failOp xbsrn) $ \fail -> @@ -613,17 +625,23 @@ tcMcStmt _ (BodyStmt _ rhs then_op guard_op) res_ty thing_inside -- guard_op :: test_ty -> rhs_ty -- then_op :: rhs_ty -> new_res_ty -> res_ty -- Where test_ty is, for example, Bool - ; ((thing, rhs', rhs_ty, guard_op'), then_op') + ; ((thing, rhs', rhs_ty, new_res_ty, test_ty, guard_op'), then_op') <- tcSyntaxOp MCompOrigin then_op [SynRho, SynRho] res_ty $ \ [rhs_ty, new_res_ty] [rhs_mult, fun_mult] -> - do { (rhs', guard_op') + do { ((rhs', test_ty), guard_op') <- tcScalingUsage rhs_mult $ tcSyntaxOp MCompOrigin guard_op [SynAny] (mkCheckExpType rhs_ty) $ - \ [test_ty] [test_mult] -> - tcScalingUsage test_mult $ tcCheckMonoExpr rhs test_ty + \ [test_ty] [test_mult] -> do + rhs' <- tcScalingUsage test_mult $ tcCheckMonoExpr rhs test_ty + return $ (rhs', test_ty) ; thing <- tcScalingUsage fun_mult $ thing_inside (mkCheckExpType new_res_ty) - ; return (thing, rhs', rhs_ty, guard_op') } + ; return (thing, rhs', rhs_ty, new_res_ty, test_ty, guard_op') } + + ; _evTerm1 <- hasFixedRuntimeRep FRRBodyStmtGuard test_ty + ; _evTerm2 <- hasFixedRuntimeRep (FRRBodyStmt MonadComprehension 1) rhs_ty + ; _evTerm3 <- hasFixedRuntimeRep (FRRBodyStmt MonadComprehension 2) new_res_ty + ; return (BodyStmt rhs_ty rhs' then_op' guard_op', thing) } -- Grouping statements @@ -850,13 +868,15 @@ tcDoStmt ctxt (BindStmt xbsrn pat rhs) res_ty thing_inside -- This level of generality is needed for using do-notation -- in full generality; see #1537 - ((rhs', pat_mult, pat', new_res_ty, thing), bind_op') + ((rhs_ty, rhs', pat_mult, pat', new_res_ty, thing), bind_op') <- tcSyntaxOp DoOrigin (xbsrn_bindOp xbsrn) [SynRho, SynFun SynAny SynRho] res_ty $ \ [rhs_ty, pat_ty, new_res_ty] [rhs_mult,fun_mult,pat_mult] -> do { rhs' <-tcScalingUsage rhs_mult $ tcCheckMonoExprNC rhs rhs_ty ; (pat', thing) <- tcScalingUsage fun_mult $ tcCheckPat (StmtCtxt ctxt) pat (Scaled pat_mult pat_ty) $ thing_inside (mkCheckExpType new_res_ty) - ; return (rhs', pat_mult, pat', new_res_ty, thing) } + ; return (rhs_ty, rhs', pat_mult, pat', new_res_ty, thing) } + + ; _concrete_ev <- hasFixedRuntimeRep (FRRBindStmt DoNotation) rhs_ty -- If (but only if) the pattern can fail, typecheck the 'fail' operator ; fail_op' <- fmap join . forM (xbsrn_failOp xbsrn) $ \fail -> @@ -884,12 +904,14 @@ tcDoStmt ctxt (ApplicativeStmt _ pairs mb_join) res_ty thing_inside tcDoStmt _ (BodyStmt _ rhs then_op _) res_ty thing_inside = do { -- Deal with rebindable syntax; -- (>>) :: rhs_ty -> new_res_ty -> res_ty - ; ((rhs', rhs_ty, thing), then_op') + ; ((rhs', rhs_ty, new_res_ty, thing), then_op') <- tcSyntaxOp DoOrigin then_op [SynRho, SynRho] res_ty $ \ [rhs_ty, new_res_ty] [rhs_mult,fun_mult] -> do { rhs' <- tcScalingUsage rhs_mult $ tcCheckMonoExprNC rhs rhs_ty ; thing <- tcScalingUsage fun_mult $ thing_inside (mkCheckExpType new_res_ty) - ; return (rhs', rhs_ty, thing) } + ; return (rhs', rhs_ty, new_res_ty, thing) } + ; _evTerm1 <- hasFixedRuntimeRep (FRRBodyStmt DoNotation 1) rhs_ty + ; _evTerm2 <- hasFixedRuntimeRep (FRRBodyStmt DoNotation 2) new_res_ty ; return (BodyStmt rhs_ty rhs' then_op' noSyntaxExpr, thing) } tcDoStmt ctxt (RecStmt { recS_stmts = L l stmts, recS_later_ids = later_names diff --git a/compiler/GHC/Tc/Gen/Pat.hs b/compiler/GHC/Tc/Gen/Pat.hs index 78a4e22901..332ea601b1 100644 --- a/compiler/GHC/Tc/Gen/Pat.hs +++ b/compiler/GHC/Tc/Gen/Pat.hs @@ -36,6 +36,7 @@ import GHC.Rename.Utils import GHC.Tc.Errors.Types import GHC.Tc.Utils.Zonk import GHC.Tc.Gen.Sig( TcPragEnv, lookupPragEnv, addInlinePrags ) +import GHC.Tc.Utils.Concrete ( mkWpFun ) import GHC.Tc.Utils.Monad import GHC.Tc.Utils.Instantiate import GHC.Types.Error @@ -445,12 +446,12 @@ tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of ; let Scaled w h_pat_ty = pat_ty ; pat_ty <- readExpType h_pat_ty - ; let expr_wrap2' = mkWpFun expr_wrap2 idHsWrapper - (Scaled w pat_ty) inf_res_sigma doc - -- expr_wrap2' :: (inf_arg_ty -> inf_res_sigma) "->" - -- (pat_ty -> inf_res_sigma) + ; expr_wrap2' <- mkWpFun expr_wrap2 idHsWrapper + (Scaled w pat_ty) inf_res_sigma (WpFunViewPat $ unLoc expr) + -- expr_wrap2' :: (inf_arg_ty -> inf_res_sigma) "->" + -- (pat_ty -> inf_res_sigma) + ; let expr_wrap = expr_wrap2' <.> expr_wrap1 <.> mult_wrap - doc = text "When checking the view pattern function:" <+> (ppr expr) ; return $ (ViewPat pat_ty (mkLHsWrap expr_wrap expr') pat', res) } @@ -656,6 +657,7 @@ AST is used for the subtraction operation. ; return (lit2', wrap, bndr_id) } ; pat_ty <- readExpType pat_exp_ty + -- The Report says that n+k patterns must be in Integral -- but it's silly to insist on this in the RebindableSyntax case ; unlessM (xoptM LangExt.RebindableSyntax) $ diff --git a/compiler/GHC/Tc/Gen/Rule.hs b/compiler/GHC/Tc/Gen/Rule.hs index 73dedfbaf5..46b1e16313 100644 --- a/compiler/GHC/Tc/Gen/Rule.hs +++ b/compiler/GHC/Tc/Gen/Rule.hs @@ -477,12 +477,17 @@ getRuleQuantCts wc new_skol_tvs = skol_tvs `extendVarSetList` ic_skols imp rule_quant_ct :: TcTyCoVarSet -> Ct -> Bool - rule_quant_ct skol_tvs ct - | EqPred _ t1 t2 <- classifyPredType (ctPred ct) - , not (ok_eq t1 t2) - = False -- Note [RULE quantification over equalities] - | otherwise - = tyCoVarsOfCt ct `disjointVarSet` skol_tvs + rule_quant_ct skol_tvs ct = case classifyPredType (ctPred ct) of + EqPred _ t1 t2 + | not (ok_eq t1 t2) + -> False -- Note [RULE quantification over equalities] + SpecialPred {} + -- RULES must never quantify over special predicates, as that + -- would leak internal GHC implementation details to the user. + -- + -- Tests (for Concrete# predicates): RepPolyRule{1,2,3}. + -> False + _ -> tyCoVarsOfCt ct `disjointVarSet` skol_tvs ok_eq t1 t2 | t1 `tcEqType` t2 = False diff --git a/compiler/GHC/Tc/Gen/Sig.hs b/compiler/GHC/Tc/Gen/Sig.hs index 67715e9b5b..bec5af03b0 100644 --- a/compiler/GHC/Tc/Gen/Sig.hs +++ b/compiler/GHC/Tc/Gen/Sig.hs @@ -32,15 +32,15 @@ import GHC.Driver.Backend import GHC.Hs -import GHC.Tc.Errors.Types ( TcRnMessage(..), LevityCheckProvenance(..) ) +import GHC.Tc.Errors.Types ( FixedRuntimeRepProvenance(..), TcRnMessage(..) ) import GHC.Tc.Gen.HsType import GHC.Tc.Types import GHC.Tc.Solver( pushLevelAndSolveEqualitiesX, reportUnsolvedEqualities ) import GHC.Tc.Utils.Monad +import GHC.Tc.Utils.TcMType ( checkTypeHasFixedRuntimeRep ) import GHC.Tc.Utils.Zonk import GHC.Tc.Types.Origin import GHC.Tc.Utils.TcType -import GHC.Tc.Utils.TcMType import GHC.Tc.Validity ( checkValidType ) import GHC.Tc.Utils.Unify( tcSkolemise, unifyType ) import GHC.Tc.Utils.Instantiate( topInstantiate, tcInstTypeBndrs ) @@ -452,10 +452,15 @@ tcPatSynSig name sig_ty@(L _ (HsSig{sig_bndrs = hs_outer_bndrs, sig_body = hs_ty ; checkValidType ctxt $ build_patsyn_type implicit_bndrs univ_bndrs req ex_bndrs prov body_ty - -- arguments become the types of binders. We thus cannot allow - -- representation polymorphism here - ; let (arg_tys, _) = tcSplitFunTys body_ty - ; mapM_ (checkForLevPoly LevityCheckPatSynSig . scaledThing) arg_tys + -- Neither argument types nor the return type may be representation polymorphic. + -- This is because, when creating a matcher: + -- - the argument types become the the binder types (see test RepPolyPatySynArg), + -- - the return type becomes the scrutinee type (see test RepPolyPatSynRes). + ; let (arg_tys, res_ty) = tcSplitFunTys body_ty + ; mapM_ + (\(Scaled _ arg_ty) -> checkTypeHasFixedRuntimeRep FixedRuntimeRepPatSynSigArg arg_ty) + arg_tys + ; checkTypeHasFixedRuntimeRep FixedRuntimeRepPatSynSigRes res_ty ; traceTc "tcTySig }" $ vcat [ text "kvs" <+> ppr_tvs (binderVars kv_bndrs) |