summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--compiler/GHC/Core/Type.hs2
-rw-r--r--compiler/GHC/Tc/Gen/Bind.hs5
-rw-r--r--compiler/GHC/Tc/TyCl.hs46
-rw-r--r--compiler/GHC/Tc/Validity.hs52
-rw-r--r--testsuite/tests/polykinds/T22743.hs10
-rw-r--r--testsuite/tests/polykinds/T22743.stderr7
-rw-r--r--testsuite/tests/polykinds/all.T1
7 files changed, 74 insertions, 49 deletions
diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index 7c36dfe02c..81b0f1e31b 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/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,
diff --git a/compiler/GHC/Tc/Gen/Bind.hs b/compiler/GHC/Tc/Gen/Bind.hs
index 6441fe991a..c4269c984d 100644
--- a/compiler/GHC/Tc/Gen/Bind.hs
+++ b/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
diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs
index 19b19e36c7..25900f2103 100644
--- a/compiler/GHC/Tc/TyCl.hs
+++ b/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
diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index 6bd86a81f0..dcbe78cf31 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/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
diff --git a/testsuite/tests/polykinds/T22743.hs b/testsuite/tests/polykinds/T22743.hs
new file mode 100644
index 0000000000..55ed0f4a24
--- /dev/null
+++ b/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
diff --git a/testsuite/tests/polykinds/T22743.stderr b/testsuite/tests/polykinds/T22743.stderr
new file mode 100644
index 0000000000..cb097568e4
--- /dev/null
+++ b/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
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 721e41cebd..b23e76c025 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/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 Lorry Controller Status