summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSimon Peyton Jones <simon.peytonjones@gmail.com>2022-01-31 17:58:22 +0000
committerMarge Bot <ben+marge-bot@smart-cactus.org>2022-02-02 19:27:56 -0500
commit6438fed95af5297f847b9bce06e27f6437e35b4e (patch)
tree85f7077106b269d7f6cfe91a636f88a16e5fe3b6
parentd2cce4532947367a5305783bd3e93c1858cded2e (diff)
downloadhaskell-6438fed95af5297f847b9bce06e27f6437e35b4e.tar.gz
Refactor the escaping kind check for data constructors
As #20929 pointed out, we were in-elegantly checking for escaping kinds in `checkValidType`, even though that check was guaranteed to succeed for type signatures -- it's part of kind-checking a type. But for /data constructors/ we kind-check the pieces separately, so we still need the check. This MR is a pure refactor, moving the test from `checkValidType` to `checkValidDataCon`. No new tests; external behaviour doesn't change.
-rw-r--r--compiler/GHC/Tc/TyCl.hs72
-rw-r--r--compiler/GHC/Tc/Validity.hs50
2 files changed, 64 insertions, 58 deletions
diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs
index 3ada6b6dc3..e184bd178f 100644
--- a/compiler/GHC/Tc/TyCl.hs
+++ b/compiler/GHC/Tc/TyCl.hs
@@ -4350,7 +4350,9 @@ checkValidDataCon dflags existential_ok tc con
addErrCtxt (dataConCtxt [L (noAnnSrcSpan con_loc) con_name]) $
do { let tc_tvs = tyConTyVars tc
res_ty_tmpl = mkFamilyTyConApp tc (mkTyVarTys tc_tvs)
- orig_res_ty = dataConOrigResTy con
+ arg_tys = dataConOrigArgTys con
+ orig_res_ty = dataConOrigResTy con
+
; traceTc "checkValidDataCon" (vcat
[ ppr con, ppr tc, ppr tc_tvs
, ppr res_ty_tmpl <+> dcolon <+> ppr (tcTypeKind res_ty_tmpl)
@@ -4387,15 +4389,20 @@ checkValidDataCon dflags existential_ok tc con
-- Reason: it's really the argument of an equality constraint
; checkValidMonoType orig_res_ty
- -- If we are dealing with a newtype, we allow representation
- -- polymorphism regardless of whether or not UnliftedNewtypes
- -- is enabled. A later check in checkNewDataCon handles this,
- -- producing a better error message than checkTypeHasFixedRuntimeRep would.
+ -- Check for an escaping result kind
+ -- See Note [Check for escaping result kind]
+ ; checkEscapingKind con
+
+ -- For /data/ types check that each argument has a fixed runtime rep
+ -- If we are dealing with a /newtype/, we allow representation
+ -- polymorphism regardless of whether or not UnliftedNewtypes
+ -- is enabled. A later check in checkNewDataCon handles this,
+ -- producing a better error message than checkTypeHasFixedRuntimeRep would.
+ ; let check_rr = checkTypeHasFixedRuntimeRep FixedRuntimeRepDataConField
; unless (isNewTyCon tc) $
- checkNoErrs $
- mapM_ (checkTypeHasFixedRuntimeRep FixedRuntimeRepDataConField)
- (map scaledThing $ dataConOrigArgTys con)
- -- the checkNoErrs is to prevent a panic in isVanillaDataCon
+ checkNoErrs $
+ mapM_ (check_rr . scaledThing) arg_tys
+ -- The checkNoErrs is to prevent a panic in isVanillaDataCon
-- (called a a few lines down), which can fall over if there is a
-- bang on a representation-polymorphic argument. This is #18534,
-- typecheck/should_fail/T18534
@@ -4489,9 +4496,9 @@ checkValidDataCon dflags existential_ok tc con
}
where
bang_opts = initBangOpts dflags
- con_name = dataConName con
- con_loc = nameSrcSpan con_name
- ctxt = ConArgCtxt con_name
+ con_name = dataConName con
+ con_loc = nameSrcSpan con_name
+ ctxt = ConArgCtxt con_name
is_strict = \case
NoSrcStrict -> bang_opt_strict_data bang_opts
bang -> isSrcStrict bang
@@ -4554,6 +4561,47 @@ checkNewDataCon con
ok_mult One = True
ok_mult _ = False
+
+-- | Reject nullary data constructors where a type variables
+-- would escape through the result kind
+-- See Note [Check for escaping result kind]
+checkEscapingKind :: DataCon -> TcM ()
+checkEscapingKind data_con
+ | null eq_spec, null theta, null arg_tys
+ , let tau_kind = tcTypeKind res_ty
+ , Nothing <- occCheckExpand (univ_tvs ++ ex_tvs) tau_kind
+ -- Ensure that none of the tvs occur in the kind of the forall
+ -- /after/ expanding type synonyms.
+ -- See Note [Phantom type variables in kinds] in GHC.Core.Type
+ = failWithTc $ TcRnForAllEscapeError (dataConWrapperType data_con) tau_kind
+ | otherwise
+ = return ()
+ where
+ (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, res_ty)
+ = dataConFullSig data_con
+
+{- Note [Check for escaping result kind]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider:
+ type T :: TYPE (BoxedRep l)
+ data T = MkT
+This is not OK: we get
+ MkT :: forall l. T @l :: TYPE (BoxedRep l)
+which is ill-kinded.
+
+For ordinary type signatures f :: blah, we make this check as part of kind-checking
+the type signature; see Note [Escaping kind in type signatures] in GHC.Tc.Gen.HsType.
+But for data constructors we check the type piecemeal, and there is no very
+convenient place to do it. For example, note that it only applies for /nullary/
+constructors. If we had
+ data T = MkT Int
+then the type of MkT would be MkT :: forall l. Int -> T @l, which is fine.
+
+So we make the check in checkValidDataCon.
+
+Historical note: we used to do the check in checkValidType (#20929 discusses).
+-}
+
-------------------------------
checkValidClass :: Class -> TcM ()
checkValidClass cls
diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index 898a716980..9d6a05c7aa 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -345,6 +345,8 @@ This might not necessarily show up in kind checking.
checkValidType :: UserTypeCtxt -> Type -> TcM ()
-- Checks that a user-written type is valid for the given context
-- Assumes argument is fully zonked
+-- Assumes arugment is well-kinded;
+-- that is, checkValidType doesn't need to do kind checking
-- Not used for instance decls; checkValidInstance instead
checkValidType ctxt ty
= do { traceTc "checkValidType" (ppr ty <+> text "::" <+> ppr (tcTypeKind ty))
@@ -738,11 +740,11 @@ check_type ve@(ValidityEnv{ ve_tidy_env = env, ve_ctxt = ctxt
; check_type (ve{ve_tidy_env = env'}) tau
-- Allow foralls to right of arrow
- ; checkEscapingKind env' tvbs' theta tau }
+ }
where
(tvbs, phi) = tcSplitForAllTyVarBinders ty
(theta, tau) = tcSplitPhiTy phi
- (env', tvbs') = tidyTyCoVarBinders env tvbs
+ (env', _) = tidyTyCoVarBinders env tvbs
check_type (ve@ValidityEnv{ ve_tidy_env = env, ve_ctxt = ctxt
, ve_rank = rank })
@@ -908,50 +910,6 @@ check_arg_type type_syn (ve@ValidityEnv{ve_ctxt = ctxt, ve_rank = rank}) ty
; check_type (ve{ve_ctxt = ctxt', ve_rank = rank'}) ty }
----------------------------------------
-
--- | Reject type variables that would escape their escape through a kind.
--- See @Note [Type variables escaping through kinds]@.
-checkEscapingKind :: TidyEnv -> [TyVarBinder] -> ThetaType -> Type -> TcM ()
-checkEscapingKind env tvbs theta tau =
- case occCheckExpand (binderVars tvbs) phi_kind of
- -- Ensure that none of the tvs occur in the kind of the forall
- -- /after/ expanding type synonyms.
- -- See Note [Phantom type variables in kinds] in GHC.Core.Type
- Nothing -> failWithTcM $ forAllEscapeErr env tvbs theta tau tau_kind
- Just _ -> pure ()
- where
- tau_kind = tcTypeKind tau
- phi_kind | null theta = tau_kind
- | otherwise = liftedTypeKind
- -- If there are any constraints, the kind is *. (#11405)
-
-forAllEscapeErr :: TidyEnv -> [TyVarBinder] -> ThetaType -> Type -> Kind
- -> (TidyEnv, TcRnMessage)
-forAllEscapeErr env tvbs theta tau tau_kind
- -- NB: Don't tidy the sigma type since the tvbs were already tidied
- -- previously, and re-tidying them will make the names of type
- -- variables different from tau_kind.
- = (env, TcRnForAllEscapeError (mkSigmaTy tvbs theta tau) (tidyType env tau_kind))
-
-{-
-Note [Type variables escaping through kinds]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider:
-
- type family T (r :: RuntimeRep) :: TYPE r
- foo :: forall r. T r
-
-Something smells funny about the type of `foo`. If you spell out the kind
-explicitly, it becomes clearer from where the smell originates:
-
- foo :: ((forall r. T r) :: TYPE r)
-
-The type variable `r` appears in the result kind, which escapes the scope of
-its binding site! This is not desirable, so we establish a validity check
-(`checkEscapingKind`) to catch any type variables that might escape through
-kinds in this way.
--}
-
checkConstraintsOK :: ValidityEnv -> ThetaType -> Type -> TcM ()
checkConstraintsOK ve theta ty
| null theta = return ()