[Git][ghc/ghc][wip/T24176] Kind-check body of a required forall
Krzysztof Gogolewski (@monoidal)
gitlab at gitlab.haskell.org
Thu Nov 30 09:36:36 UTC 2023
Krzysztof Gogolewski pushed to branch wip/T24176 at Glasgow Haskell Compiler / GHC
Commits:
8e25ba79 by Krzysztof Gogolewski at 2023-11-30T10:33:38+01:00
Kind-check body of a required forall
We now require that in 'forall a -> ty', ty has kind TYPE r for some r.
Fixes #24176
- - - - -
5 changed files:
- compiler/GHC/Tc/Gen/HsType.hs
- testsuite/tests/dependent/should_fail/T16326_Fail12.stderr
- + testsuite/tests/vdq-rta/should_fail/T24176.hs
- + testsuite/tests/vdq-rta/should_fail/T24176.stderr
- testsuite/tests/vdq-rta/should_fail/all.T
Changes:
=====================================
compiler/GHC/Tc/Gen/HsType.hs
=====================================
@@ -1178,18 +1178,36 @@ tc_hs_type mode (HsOpTy _ _ ty1 (L _ op) ty2) exp_kind
= tc_fun_type mode (HsUnrestrictedArrow noHsUniTok) ty1 ty2 exp_kind
--------- Foralls
-tc_hs_type mode (HsForAllTy { hst_tele = tele, hst_body = ty }) exp_kind
+tc_hs_type mode (HsForAllTy { hst_tele = tele@(HsForAllInvis {}), hst_body = ty }) exp_kind
= do { (tv_bndrs, ty') <- tcTKTelescope mode tele $
tc_lhs_type mode ty exp_kind
-- Pass on the mode from the type, to any wildcards
-- in kind signatures on the forall'd variables
-- e.g. f :: _ -> Int -> forall (a :: _). blah
- -- Why exp_kind? See Note [Body kind of a HsForAllTy]
+ --
+ -- For an invisible forall, we allow the body to have
+ -- an arbitrary kind (hence exp_kind above).
+ -- See Note [Body kind of a HsForAllTy]
-- Do not kind-generalise here! See Note [Kind generalisation]
; return (mkForAllTys tv_bndrs ty') }
+tc_hs_type mode (HsForAllTy { hst_tele = tele@(HsForAllVis {}), hst_body = ty }) exp_kind
+ = do { ek <- newOpenTypeKind
+ ; (tv_bndrs, ty') <- tcTKTelescope mode tele $
+ tc_lhs_type mode ty ek
+ -- Pass on the mode from the type, to any wildcards
+ -- in kind signatures on the forall'd variables
+ -- e.g. f :: _ -> Int -> forall (a :: _). blah
+ --
+ -- For a visible forall, we require that the body is of kind TYPE r.
+ -- See Note [Body kind of a HsForAllTy]
+
+ -- Do not kind-generalise here! See Note [Kind generalisation]
+
+ ; checkExpectedKind (unLoc ty) (mkForAllTys tv_bndrs ty') ek exp_kind }
+
tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = rn_ty }) exp_kind
| null (unLoc ctxt)
= tc_lhs_type mode rn_ty exp_kind
@@ -2042,25 +2060,23 @@ examples.
Note [Body kind of a HsForAllTy]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The body of a forall is usually a type, but in principle
-there's no reason to prohibit *unlifted* types.
-In fact, GHC can itself construct a function with an
-unboxed tuple inside a for-all (via CPR analysis; see
+The body of a forall is usually a type.
+Because of representation polymorphism, it can be a TYPE r, for any r.
+(In fact, GHC can itself construct a function with an
+unboxed tuple inside a for-all via CPR analysis; see
typecheck/should_compile/tc170).
-Moreover in instance heads we get forall-types with
-kind Constraint.
-
-It's tempting to check that the body kind is (TYPE _). But this is
-wrong. For example:
+A forall can also be used in an instance head, then the body should
+be a constraint.
- class C a b
- newtype N = Mk Foo deriving (C a)
+Right now, we do not have any easy way to enforce that a type is
+either a TYPE something or CONSTRAINT something, so we accept any kind.
+This is unsound (#22063). We could fix this by implementing a TypeLike
+predicate, see see #20000.
-We're doing newtype-deriving for C. But notice how `a` isn't in scope in
-the predicate `C a`. So we quantify, yielding `forall a. C a` even though
-`C a` has kind `* -> Constraint`. The `forall a. C a` is a bit cheeky, but
-convenient. Bottom line: don't check for (TYPE _) here.
+For a forall with a required argument, we do not allow constraints;
+e.g. forall a -> Eq a is invalid. Therefore, we can enforce that the body
+is a TYPE something in this case (#24176).
Note [Body kind of a HsQualTy]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
=====================================
testsuite/tests/dependent/should_fail/T16326_Fail12.stderr
=====================================
@@ -1,8 +1,8 @@
-T16326_Fail12.hs:6:1: error: [GHC-51580]
- • Illegal visible, dependent quantification in the type of a term:
- forall a -> Show a
- • In the context: forall a -> Show a
- While checking the super-classes of class ‘C’
- In the class declaration for ‘C’
- Suggested fix: Perhaps you intended to use RequiredTypeArguments
+T16326_Fail12.hs:6:8: error: [GHC-83865]
+ • Expected a constraint, but ‘Show a’ is a type
+ • In the class declaration for ‘C’
+
+T16326_Fail12.hs:6:20: error: [GHC-83865]
+ • Expected a type, but ‘Show a’ is a constraint
+ • In the class declaration for ‘C’
=====================================
testsuite/tests/vdq-rta/should_fail/T24176.hs
=====================================
@@ -0,0 +1,5 @@
+{-# LANGUAGE QuantifiedConstraints, RequiredTypeArguments #-}
+module T24176 where
+
+f :: (forall a -> Eq a) => a
+f = f
=====================================
testsuite/tests/vdq-rta/should_fail/T24176.stderr
=====================================
@@ -0,0 +1,8 @@
+
+T24176.hs:4:7: error: [GHC-83865]
+ • Expected a constraint, but ‘Eq a’ is a type
+ • In the type signature: f :: (forall a -> Eq a) => a
+
+T24176.hs:4:19: error: [GHC-83865]
+ • Expected a type, but ‘Eq a’ is a constraint
+ • In the type signature: f :: (forall a -> Eq a) => a
=====================================
testsuite/tests/vdq-rta/should_fail/all.T
=====================================
@@ -14,4 +14,5 @@ test('T22326_fail_patsyn', normal, compile_fail, [''])
test('T22326_fail_match', normal, compile_fail, [''])
test('T23738_fail_wild', normal, compile_fail, [''])
test('T23738_fail_implicit_tv', normal, compile_fail, [''])
-test('T23738_fail_var', normal, compile_fail, [''])
\ No newline at end of file
+test('T23738_fail_var', normal, compile_fail, [''])
+test('T24176', normal, compile_fail, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/8e25ba7915ee3cf8f6420a7d862f072f14a49e32
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/8e25ba7915ee3cf8f6420a7d862f072f14a49e32
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/20231130/89428fa2/attachment-0001.html>
More information about the ghc-commits
mailing list