[Git][ghc/ghc][wip/T25243] Only allow (a => b) :: Constraint rather than CONSTRAINT rep

[Krzysztof Gogolewski (@monoidal)]

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


Commits:
1e41f636 by Krzysztof Gogolewski at 2024-09-16T23:55:57+02:00
Only allow (a => b) :: Constraint rather than CONSTRAINT rep

Fixes #25243

- - - - -


4 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


Changes:

=====================================
compiler/GHC/Tc/Gen/HsType.hs
=====================================
@@ -1158,10 +1158,13 @@ tcHsType mode (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
+  | 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') }
+      ; let res_ty = tcMkDFunPhiTy ctxt' ty'
+      ; checkExpKind (unLoc rn_ty) res_ty
+                     constraintKind exp_kind }
 
   | otherwise
   = do { ctxt' <- tc_hs_context mode ctxt
@@ -2110,7 +2113,7 @@ 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.
 
@@ -2121,11 +2124,14 @@ should be '*' we risk getting TWO error messages, one saying that Eq
 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.)
+kludge: I just look at the expected kind.  If we are in checking mode
+(`exp_kind` = `Check k`), and the pushed-in kind `k` is `Constraint`, 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.
+Actually, we only check whether `k` is a `CONSTRAINT rep`, but in that
+case enforce that `rep` is a LiftedRep. This gives a better error message
+in T25243.
 
 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,5 @@
+T25243.hs:8:14: error: [GHC-83865]
+    • Expected an IntRep constraint, but ‘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, [''])



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/1e41f6367a01a3068390cfbc8baa1702d9138b76

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/1e41f6367a01a3068390cfbc8baa1702d9138b76
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/20240916/c5e85ebe/attachment-0001.html>