[Git][ghc/ghc][master] Only allow (a => b) :: Constraint rather than CONSTRAINT rep
Marge Bot (@marge-bot)
gitlab at gitlab.haskell.org
Sun Oct 6 13:52:55 UTC 2024
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
92f8939a by Krzysztof Gogolewski at 2024-10-06T09:52:22-04:00
Only allow (a => b) :: Constraint rather than CONSTRAINT rep
Fixes #25243
- - - - -
5 changed files:
- compiler/GHC/Tc/Gen/HsType.hs
- + testsuite/tests/quantified-constraints/T25243.hs
- + testsuite/tests/quantified-constraints/T25243.stderr
- testsuite/tests/quantified-constraints/all.T
- testsuite/tests/rename/should_fail/rnfail026.stderr
Changes:
=====================================
compiler/GHC/Tc/Gen/HsType.hs
=====================================
@@ -1154,14 +1154,17 @@ tcHsType mode t@(HsForAllTy { hst_tele = tele, hst_body = ty }) exp_kind
-- Do not kind-generalise here! See Note [Kind generalisation]
; return (mkForAllTys tv_bndrs ty') }
-tcHsType mode (HsQualTy { hst_ctxt = ctxt, hst_body = rn_ty }) exp_kind
+tcHsType mode t@(HsQualTy { hst_ctxt = ctxt, hst_body = rn_ty }) exp_kind
| null (unLoc ctxt)
= tcLHsType mode rn_ty exp_kind
- -- See Note [Body kind of a HsQualTy]
- | Check kind <- exp_kind, isConstraintLikeKind kind
+ -- See Note [Body kind of a HsQualTy], point (BK1)
+ | Check kind <- exp_kind -- Checking mode
+ , isConstraintLikeKind kind -- CONSTRAINT rep
= do { ctxt' <- tc_hs_context mode ctxt
- ; ty' <- tc_check_lhs_type mode rn_ty constraintKind
- ; return (tcMkDFunPhiTy ctxt' ty') }
+ -- See Note [Body kind of a HsQualTy], point (BK2)
+ ; ty' <- tc_check_lhs_type mode rn_ty constraintKind
+ ; let res_ty = tcMkDFunPhiTy ctxt' ty'
+ ; checkExpKind t res_ty constraintKind exp_kind }
| otherwise
= do { ctxt' <- tc_hs_context mode ctxt
@@ -1170,8 +1173,7 @@ tcHsType mode (HsQualTy { hst_ctxt = ctxt, hst_body = rn_ty }) exp_kind
-- be TYPE r, for any r, hence newOpenTypeKind
; ty' <- tc_check_lhs_type mode rn_ty ek
; let res_ty = tcMkPhiTy ctxt' ty'
- ; checkExpKind (unLoc rn_ty) res_ty
- liftedTypeKind exp_kind }
+ ; checkExpKind t res_ty liftedTypeKind exp_kind }
--------- Lists, arrays, and tuples
tcHsType mode rn_ty@(HsListTy _ elt_ty) exp_kind
@@ -2110,22 +2112,36 @@ However, consider
instance Eq a => Eq [a] where ...
or
f :: (Eq a => Eq [a]) => blah
-Here both body-kind of the HsQualTy is Constraint rather than *.
+Here both body-kind and result kind of the HsQualTy is Constraint rather than *.
Rather crudely we tell the difference by looking at exp_kind. It's
very convenient to typecheck instance types like any other HsSigType.
-Admittedly the '(Eq a => Eq [a]) => blah' case is erroneous, but it's
-better to reject in checkValidType. If we say that the body kind
-should be '*' we risk getting TWO error messages, one saying that Eq
-[a] doesn't have kind '*', and one saying that we need a Constraint to
-the left of the outer (=>).
-
-How do we figure out the right body kind? Well, it's a bit of a
-kludge: I just look at the expected kind. If it's Constraint, we
-must be in this instance situation context. It's a kludge because it
-wouldn't work if any unification was involved to compute that result
-kind -- but it isn't. (The true way might be to use the 'mode'
-parameter, but that seemed like a sledgehammer to crack a nut.)
+(BK1) How do we figure out the right body kind?
+
+Well, it's a bit of a kludge: I just look at the expected kind, `exp_kind`.
+If we are in checking mode (`exp_kind` = `Check k`), and the pushed-in kind
+`k` is `CONSTRAINT rep`, then we check that the body type has kind `Constraint` too.
+
+This is a kludge because it wouldn't work if any unification was
+involved to compute that result kind -- but it isn't.
+
+Note that in the kludgy "figure out whether we are in a type or constraint"
+check, we only check if `k` is a `CONSTRAINT rep`, not `Constraint`.
+That turns out to give a better error message in T25243.
+
+(BK2)
+
+Note that, once we are in the constraint case, we check that the body has
+kind Constraint; see the call to tc_check_lhs_type. (In contrast, for
+types we check that the body has kind TYPE kappa for some fresh unification
+variable kappa.)
+Reason: we don't yet have support for constraints that are not lifted: it's
+not possible to declare a class returning a different type than CONSTRAINT LiftedRep.
+Evidence is always lifted, the fat arrow c => t requires c to be
+a lifted constraint. In a far future, if we add support for non-lifted
+constraints, we could allow c1 => c2 where
+c1 :: CONSTRAINT rep1, c2 :: CONSTRAINT rep2
+have arbitrary representations rep1 and rep2.
Note [Inferring tuple kinds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
=====================================
testsuite/tests/quantified-constraints/T25243.hs
=====================================
@@ -0,0 +1,8 @@
+{-# LANGUAGE DataKinds, QuantifiedConstraints, UndecidableInstances #-}
+module T25243 where
+
+import GHC.Exts
+import Data.Kind
+
+type T :: Constraint -> Constraint -> CONSTRAINT IntRep
+type T a b = a => b
=====================================
testsuite/tests/quantified-constraints/T25243.stderr
=====================================
@@ -0,0 +1,6 @@
+T25243.hs:8:14: error: [GHC-83865]
+ • Expected an IntRep constraint,
+ but ‘a => b’ is a lifted constraint
+ • In the type ‘a => b’
+ In the type declaration for ‘T’
+
=====================================
testsuite/tests/quantified-constraints/all.T
=====================================
@@ -45,3 +45,4 @@ test('T23143', normal, compile, [''])
test('T23333', normal, compile, [''])
test('T23323', normal, compile, [''])
test('T22238', normal, compile, [''])
+test('T25243', normal, compile_fail, [''])
=====================================
testsuite/tests/rename/should_fail/rnfail026.stderr
=====================================
@@ -1,6 +1,6 @@
-
rnfail026.hs:16:27: error: [GHC-83865]
- • Expected kind ‘* -> *’, but ‘Set a’ has kind ‘*’
+ • Expected kind ‘* -> *’, but ‘Eq a => Set a’ has kind ‘*’
• In the first argument of ‘Monad’, namely
‘(forall a. Eq a => Set a)’
In the instance declaration for ‘Monad (forall a. Eq a => Set a)’
+
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/92f8939a5fa689dc0143501cfeac0b3b2cd7abd6
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/92f8939a5fa689dc0143501cfeac0b3b2cd7abd6
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/20241006/51ecf0a9/attachment-0001.html>
More information about the ghc-commits
mailing list