[Git][ghc/ghc][wip/T24176] Kind-check body of a required forall

Krzysztof Gogolewski (@monoidal) gitlab at gitlab.haskell.org
Thu Nov 30 12:39:52 UTC 2023



Krzysztof Gogolewski pushed to branch wip/T24176 at Glasgow Haskell Compiler / GHC


Commits:
65dec56b by Krzysztof Gogolewski at 2023-11-30T13:39: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,17 +1178,30 @@ 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
-  = do { (tv_bndrs, ty') <- tcTKTelescope mode tele $
-                            tc_lhs_type mode ty exp_kind
+tc_hs_type mode t@(HsForAllTy { hst_tele = tele, hst_body = ty }) exp_kind
+  | HsForAllInvis{} <- tele
+  = tc_hs_forall_ty tele ty exp_kind
+                 -- For an invisible forall, we allow the body to have
+                 -- an arbitrary kind (hence exp_kind above).
+                 -- See Note [Body kind of a HsForAllTy]
+
+  | HsForAllVis{} <- tele
+  = do { ek <- newOpenTypeKind
+       ; r <- tc_hs_forall_ty tele ty ek
+       ; checkExpectedKind t r ek exp_kind }
+                 -- For a visible forall, we require that the body is of kind TYPE r.
+                 -- See Note [Body kind of a HsForAllTy]
+
+  where
+    tc_hs_forall_ty tele ty ek
+      = do { (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
-                 -- Why exp_kind?  See Note [Body kind of a HsForAllTy]
 
-       -- Do not kind-generalise here!  See Note [Kind generalisation]
-
-       ; return (mkForAllTys tv_bndrs ty') }
+             -- Do not kind-generalise here!  See Note [Kind generalisation]
+           ; return (mkForAllTys tv_bndrs ty') }
 
 tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = rn_ty }) exp_kind
   | null (unLoc ctxt)
@@ -2042,25 +2055,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 ‘forall a -> 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/65dec56b91839befc28a09c1d90f671930341cee

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/65dec56b91839befc28a09c1d90f671930341cee
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/ffc00a1e/attachment-0001.html>


More information about the ghc-commits mailing list