summaryrefslogtreecommitdiff
path: root/compiler/GHC/Tc/Gen
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/GHC/Tc/Gen')
-rw-r--r--compiler/GHC/Tc/Gen/App.hs246
-rw-r--r--compiler/GHC/Tc/Gen/Arrow.hs32
-rw-r--r--compiler/GHC/Tc/Gen/Bind.hs11
-rw-r--r--compiler/GHC/Tc/Gen/Expr.hs42
-rw-r--r--compiler/GHC/Tc/Gen/Head.hs32
-rw-r--r--compiler/GHC/Tc/Gen/Match.hs44
-rw-r--r--compiler/GHC/Tc/Gen/Pat.hs12
-rw-r--r--compiler/GHC/Tc/Gen/Rule.hs17
-rw-r--r--compiler/GHC/Tc/Gen/Sig.hs17
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)