[Git][ghc/ghc][wip/marge_bot_batch_merge_job] 3 commits: Add a missing checkEscapingKind

Marge Bot (@marge-bot) gitlab at gitlab.haskell.org
Sat Jan 14 15:57:09 UTC 2023



Marge Bot pushed to branch wip/marge_bot_batch_merge_job at Glasgow Haskell Compiler / GHC


Commits:
496607fd by Simon Peyton Jones at 2023-01-13T16:52:07-05:00
Add a missing checkEscapingKind

Ticket #22743 pointed out that there is a missing check,
for type-inferred bindings, that the inferred type doesn't
have an escaping kind.

The fix is easy.

- - - - -
4b95792d by Ben Gamari at 2023-01-14T10:56:58-05:00
Bump ghc-tarballs to fix #22497

It turns out that gmp 6.2.1 uses the platform-reserved `x18` register on
AArch64/Darwin. This was fixed in upstream changeset 18164:5f32dbc41afc,
which was merged in 2020. Here I backport this patch although I do hope
that a new release is forthcoming soon.

- - - - -
ea9441f4 by Bodigrim at 2023-01-14T10:57:01-05:00
Bump submodule parsec to 3.1.16.1

- - - - -


9 changed files:

- compiler/GHC/Core/Type.hs
- compiler/GHC/Tc/Gen/Bind.hs
- compiler/GHC/Tc/TyCl.hs
- compiler/GHC/Tc/Validity.hs
- libraries/ghc-bignum/gmp/gmp-tarballs
- libraries/parsec
- + testsuite/tests/polykinds/T22743.hs
- + testsuite/tests/polykinds/T22743.stderr
- testsuite/tests/polykinds/all.T


Changes:

=====================================
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,


=====================================
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


=====================================
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


=====================================
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


=====================================
libraries/ghc-bignum/gmp/gmp-tarballs
=====================================
@@ -1 +1 @@
-Subproject commit 6bbea995472b6f4db172c3cd50aa3f515ddd221c
+Subproject commit 7bb13b556d81e60556db6b5ef8757f55a3925527


=====================================
libraries/parsec
=====================================
@@ -1 +1 @@
-Subproject commit 0e23b3246fd7f6d125129316dcbedd609e6d2dca
+Subproject commit 1f542120d9adc5e22f8791a6d595210e93c6c389


=====================================
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


=====================================
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


=====================================
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 it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/7c285f21be268dc37677f5b5c852d84518d04d8d...ea9441f4b63db4aaf6c5c2d6d0a9ac55f664bc20

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/7c285f21be268dc37677f5b5c852d84518d04d8d...ea9441f4b63db4aaf6c5c2d6d0a9ac55f664bc20
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/20230114/dbd8786e/attachment-0001.html>


More information about the ghc-commits mailing list