[Git][ghc/ghc][master] Add a missing checkEscapingKind
Marge Bot (@marge-bot)
gitlab at gitlab.haskell.org
Fri Jan 13 21:52:27 UTC 2023
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
496607fd by Simon Peyton Jones at 2023-01-13T16:52:07-05:00
Add a missing checkEscapingKind
Ticket #22743 pointed out that there is a missing check,
for type-inferred bindings, that the inferred type doesn't
have an escaping kind.
The fix is easy.
- - - - -
7 changed files:
- compiler/GHC/Core/Type.hs
- compiler/GHC/Tc/Gen/Bind.hs
- compiler/GHC/Tc/TyCl.hs
- compiler/GHC/Tc/Validity.hs
- + testsuite/tests/polykinds/T22743.hs
- + testsuite/tests/polykinds/T22743.stderr
- testsuite/tests/polykinds/all.T
Changes:
=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -50,7 +50,7 @@ module GHC.Core.Type (
mkSpecForAllTy, mkSpecForAllTys,
mkVisForAllTys, mkTyCoInvForAllTy,
mkInfForAllTy, mkInfForAllTys,
- splitForAllTyCoVars,
+ splitForAllTyCoVars, splitForAllTyVars,
splitForAllReqTyBinders, splitForAllInvisTyBinders,
splitForAllForAllTyBinders,
splitForAllTyCoVar_maybe, splitForAllTyCoVar,
=====================================
compiler/GHC/Tc/Gen/Bind.hs
=====================================
@@ -49,7 +49,7 @@ import GHC.Tc.Gen.Pat
import GHC.Tc.Utils.TcMType
import GHC.Tc.Instance.Family( tcGetFamInstEnvs )
import GHC.Tc.Utils.TcType
-import GHC.Tc.Validity (checkValidType)
+import GHC.Tc.Validity (checkValidType, checkEscapingKind)
import GHC.Core.Predicate
import GHC.Core.Reduction ( Reduction(..) )
@@ -906,7 +906,8 @@ mkInferredPolyId residual insoluble qtvs inferred_theta poly_name mb_sig_inst mo
, ppr inferred_poly_ty])
; unless insoluble $
addErrCtxtM (mk_inf_msg poly_name inferred_poly_ty) $
- checkValidType (InfSigCtxt poly_name) inferred_poly_ty
+ do { checkEscapingKind inferred_poly_ty
+ ; checkValidType (InfSigCtxt poly_name) inferred_poly_ty }
-- See Note [Validity of inferred types]
-- If we found an insoluble error in the function definition, don't
-- do this check; otherwise (#14000) we may report an ambiguity
=====================================
compiler/GHC/Tc/TyCl.hs
=====================================
@@ -4408,10 +4408,7 @@ checkValidDataCon dflags existential_ok tc con
-- e.g. reject this: MkT :: T (forall a. a->a)
-- Reason: it's really the argument of an equality constraint
; checkValidMonoType orig_res_ty
-
- -- Check for an escaping result kind
- -- See Note [Check for escaping result kind]
- ; checkEscapingKind con
+ ; checkEscapingKind (dataConWrapperType con)
-- For /data/ types check that each argument has a fixed runtime rep
-- If we are dealing with a /newtype/, we allow representation
@@ -4576,47 +4573,6 @@ checkNewDataCon con
ok_mult OneTy = True
ok_mult _ = False
-
--- | Reject nullary data constructors where a type variable
--- 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 = typeKind 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
=====================================
compiler/GHC/Tc/Validity.hs
=====================================
@@ -12,7 +12,7 @@ module GHC.Tc.Validity (
Rank(..), UserTypeCtxt(..), checkValidType, checkValidMonoType,
checkValidTheta,
checkValidInstance, checkValidInstHead, validDerivPred,
- checkTySynRhs,
+ checkTySynRhs, checkEscapingKind,
checkValidCoAxiom, checkValidCoAxBranch,
checkValidTyFamEqn, checkValidAssocTyFamDeflt, checkConsistentFamInst,
arityErr,
@@ -466,6 +466,53 @@ checkTySynRhs ctxt ty
where
actual_kind = typeKind ty
+{- 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 /user-written type signatures f :: blah, we make this
+check as part of kind-checking the type signature in tcHsSigType; see
+Note [Escaping kind in type signatures] in GHC.Tc.Gen.HsType.
+
+But in two other places we need to check for an escaping result kind:
+
+* 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.
+
+* When inferring the type of a function, there is no user-written type
+ that we are checking. Forgetting this led to #22743. Now we call
+ checkEscapingKind in GHC.Tc.Gen.Bind.mkInferredPolyId
+
+Historical note: we used to do the escaping-kind check in
+checkValidType (#20929 discusses), but that is now redundant.
+-}
+
+checkEscapingKind :: Type -> TcM ()
+-- Give a sigma-type (forall a1 .. an. ty), where (ty :: ki),
+-- check that `ki` does not mention any of the binders a1..an.
+-- Otherwise the type is ill-kinded
+-- See Note [Check for escaping result kind]
+checkEscapingKind poly_ty
+ | (tvs, tau) <- splitForAllTyVars poly_ty
+ , let tau_kind = typeKind tau
+ , Nothing <- occCheckExpand 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 poly_ty tau_kind
+ | otherwise
+ = return ()
+
funArgResRank :: Rank -> (Rank, Rank) -- Function argument and result
funArgResRank (LimitedRank _ arg_rank) = (arg_rank, LimitedRank (forAllAllowed arg_rank) arg_rank)
funArgResRank other_rank = (other_rank, other_rank)
@@ -762,6 +809,9 @@ check_type ve@(ValidityEnv{ ve_tidy_env = env
; check_type (ve{ve_tidy_env = env'}) tau
-- Allow foralls to right of arrow
+ -- Note: skolem-escape in types (e.g. forall r (a::r). a) is handled
+ -- by tcHsSigType and the constraint solver, so no need to
+ -- check it here; c.f. #20929
}
where
(tvbs, phi) = tcSplitForAllTyVarBinders ty
=====================================
testsuite/tests/polykinds/T22743.hs
=====================================
@@ -0,0 +1,10 @@
+{-# LANGUAGE DataKinds #-}
+module M where
+
+import GHC.Exts
+import Data.Kind
+
+f :: forall f (g :: Type) (a :: TYPE (f g)). Int -> a
+f = f
+
+x = f 0
=====================================
testsuite/tests/polykinds/T22743.stderr
=====================================
@@ -0,0 +1,7 @@
+
+T22743.hs:10:1: error: [GHC-31147]
+ • Quantified type's kind mentions quantified type variable
+ type: ‘forall {f :: * -> RuntimeRep} {g} {a :: TYPE (f g)}. a’
+ where the body of the forall has this kind: ‘TYPE (f g)’
+ • When checking the inferred type
+ x :: forall {f :: * -> RuntimeRep} {g} {a :: TYPE (f g)}. a
=====================================
testsuite/tests/polykinds/all.T
=====================================
@@ -241,3 +241,4 @@ test('T19739c', normal, compile, [''])
test('T19739d', normal, compile, [''])
test('T22379a', normal, compile, [''])
test('T22379b', normal, compile, [''])
+test('T22743', normal, compile_fail, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/496607fdb77baf12e2fe263104ba5d0d700eee3b
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/496607fdb77baf12e2fe263104ba5d0d700eee3b
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20230113/c62fca48/attachment-0001.html>
More information about the ghc-commits
mailing list