[Git][ghc/ghc][wip/sand-witch/#16635-improve-errors] Capture scoped kind variables at type-checking phase (#16635)
Andrei Borzenkov (@sand-witch)
gitlab at gitlab.haskell.org
Thu Jun 8 13:33:45 UTC 2023
Andrei Borzenkov pushed to branch wip/sand-witch/#16635-improve-errors at Glasgow Haskell Compiler / GHC
Commits:
5e5df728 by Andrei Borzenkov at 2023-06-08T17:32:47+04:00
Capture scoped kind variables at type-checking phase (#16635)
Like descibed in new Note [Type variable scoping errors during type check] in
GHC.Tc.Types, I made ScopedTypeVariables work on type level like in
term level.
For now that only means, that the error about kind variables scoped
into type are rejected at the elaboration time, because we can't
generalize the type by adding type-level lambda - we simply have no one.
- - - - -
12 changed files:
- compiler/GHC/Hs/Type.hs
- compiler/GHC/Rename/HsType.hs
- compiler/GHC/Tc/Errors/Ppr.hs
- compiler/GHC/Tc/Errors/Types/PromotionErr.hs
- compiler/GHC/Tc/Gen/HsType.hs
- compiler/GHC/Tc/Types/BasicTypes.hs
- compiler/GHC/Tc/Utils/Env.hs
- + testsuite/tests/rename/should_fail/T16635a.hs
- + testsuite/tests/rename/should_fail/T16635a.stderr
- + testsuite/tests/rename/should_fail/T16635b.hs
- + testsuite/tests/rename/should_fail/T16635b.stderr
- testsuite/tests/rename/should_fail/all.T
Changes:
=====================================
compiler/GHC/Hs/Type.hs
=====================================
@@ -73,7 +73,7 @@ module GHC.Hs.Type (
mkHsForAllVisTele, mkHsForAllInvisTele,
mkHsQTvs, hsQTvExplicit, emptyLHsQTvs,
isHsKindedTyVar, hsTvbAllKinded,
- hsScopedTvs, hsWcScopedTvs, dropWildCards,
+ hsScopedTvs, hsScopedKiVs, hsWcScopedTvs, dropWildCards,
hsTyVarName, hsAllLTyVarNames, hsLTyVarLocNames,
hsLTyVarName, hsLTyVarNames, hsLTyVarLocName, hsExplicitLTyVarNames,
splitLHsInstDeclTy, getLHsInstDeclHead, getLHsInstDeclClass_maybe,
@@ -431,6 +431,14 @@ hsScopedTvs (L _ (HsSig{sig_bndrs = outer_bndrs}))
= hsLTyVarNames (hsOuterExplicitBndrs outer_bndrs)
-- See Note [hsScopedTvs and visible foralls]
+hsScopedKiVs :: LHsKind GhcRn -> [Name]
+-- here we should fuse two actions, performed for
+-- type signatures, but not for kind ones: `hsTypeToHsSigType`
+-- (but in GhcRn phase) and `hsScopedTvs`
+hsScopedKiVs (L _ HsForAllTy { hst_tele = HsForAllInvis { hsf_invis_bndrs = bndrs }})
+ = hsLTyVarNames bndrs
+hsScopedKiVs _ = []
+
---------------------
hsTyVarName :: HsTyVarBndr flag (GhcPass p) -> IdP (GhcPass p)
hsTyVarName (UserTyVar _ _ (L _ n)) = n
=====================================
compiler/GHC/Rename/HsType.hs
=====================================
@@ -647,8 +647,9 @@ rnHsTyKi env listTy@(HsListTy x ty)
rnHsTyKi env (HsKindSig x ty k)
= do { kind_sigs_ok <- xoptM LangExt.KindSignatures
; unless kind_sigs_ok (badKindSigErr (rtke_ctxt env) ty)
- ; (ty', lhs_fvs) <- rnLHsTyKi env ty
; (k', sig_fvs) <- rnLHsTyKi (env { rtke_level = KindLevel }) k
+ ; (ty', lhs_fvs) <- bindSigTyVarsFV (hsScopedKiVs k')
+ (rnLHsTyKi env ty)
; return (HsKindSig x ty' k', lhs_fvs `plusFV` sig_fvs) }
-- Unboxed tuples are allowed to have poly-typed arguments. These
@@ -1937,8 +1938,7 @@ extract_lty (L _ ty) acc
HsExplicitTupleTy _ tys -> extract_ltys tys acc
HsTyLit _ _ -> acc
HsStarTy _ _ -> acc
- HsKindSig _ ty ki -> extract_lty ty $
- extract_lty ki acc
+ HsKindSig _ ty ki -> extract_kind_sig ty ki acc
HsForAllTy { hst_tele = tele, hst_body = ty }
-> extract_hs_for_all_telescope tele acc $
extract_lty ty []
@@ -1949,6 +1949,17 @@ extract_lty (L _ ty) acc
-- We deal with these separately in rnLHsTypeWithWildCards
HsWildCardTy {} -> acc
+extract_kind_sig :: LHsType GhcPs -- type
+ -> LHsType GhcPs -- kind
+ -> FreeKiTyVars -> FreeKiTyVars
+extract_kind_sig
+ ty
+ (L _ HsForAllTy { hst_tele = HsForAllInvis { hsf_invis_bndrs = bndrs }, hst_body = ki_body })
+ acc
+ = extract_hs_tv_bndrs bndrs acc (extract_lty ty $ extract_lty ki_body [])
+extract_kind_sig ty ki acc = extract_lty ty $
+ extract_lty ki acc
+
extract_lhs_sig_ty :: LHsSigType GhcPs -> FreeKiTyVars
extract_lhs_sig_ty (L _ (HsSig{sig_bndrs = outer_bndrs, sig_body = body})) =
extractHsOuterTvBndrs outer_bndrs $ extract_lty body []
=====================================
compiler/GHC/Tc/Errors/Ppr.hs
=====================================
@@ -1046,6 +1046,7 @@ instance Diagnostic TcRnMessage where
ClassPE -> same_rec_group_msg
TyConPE -> same_rec_group_msg
TermVariablePE -> text "term variables cannot be promoted"
+ TypeVariablePE -> text "forall-bound variables cannot be used in kinds"
same_rec_group_msg = text "it is defined and used in the same recursive group"
TcRnMatchesHaveDiffNumArgs argsContext (MatchArgMatches match1 bad_matches)
-> mkSimpleDecorated $
=====================================
compiler/GHC/Tc/Errors/Types/PromotionErr.hs
=====================================
@@ -25,6 +25,7 @@ data PromotionErr
-- See Note [Recursion and promoting data constructors] in GHC.Tc.TyCl
| TermVariablePE -- See Note [Promoted variables in types]
| NoDataKindsDC -- -XDataKinds not enabled (for a datacon)
+ | TypeVariablePE -- See Note [Type variable scoping errors during type check]
instance Outputable PromotionErr where
ppr ClassPE = text "ClassPE"
@@ -35,6 +36,7 @@ instance Outputable PromotionErr where
ppr RecDataConPE = text "RecDataConPE"
ppr NoDataKindsDC = text "NoDataKindsDC"
ppr TermVariablePE = text "TermVariablePE"
+ ppr TypeVariablePE = text "TypeVariablePE"
pprPECategory :: PromotionErr -> SDoc
pprPECategory = text . capitalise . peCategory
@@ -47,4 +49,47 @@ peCategory FamDataConPE = "data constructor"
peCategory ConstrainedDataConPE{} = "data constructor"
peCategory RecDataConPE = "data constructor"
peCategory NoDataKindsDC = "data constructor"
-peCategory TermVariablePE = "term variable"
\ No newline at end of file
+peCategory TermVariablePE = "term variable"
+peCategory TypeVariablePE = "type variable"
+
+
+{-
+Note [Type variable scoping errors during type check]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider you have such function at the term level:
+
+ -- f :: [forall b . Either b ()]
+ f = [Right @a @() () :: forall a. Either a ()]
+
+Here `@a` in the type application and `a` in the type signature are the same
+type variable, so `forall a` introduces the type variable `a` in the
+term context. This is a binder in the surface language.
+
+After elaboration in Core, the binder change would be changed to the
+lambda abstraction:
+
+ f = [(\@a -> Right @a @() ()) :: forall a . Either a ()]
+
+So, in Core, only lambda brings new variables into scope, not `forall`.
+But how does this work with types?
+
+ type F = '[Right @a @() () :: forall a. Either a ()]
+
+If we look at this through the prism of surface language, then `a`
+should obviously be in the scope of `Right`, because that's what forall does.
+But if we take elaboration into account things get trickier -
+we need some sort of lambda in types to do such elaboration,
+like this:
+
+ type F = '[(/\ a . Right @a @() ()) :: forall a. Either a ()] -- Bogus
+
+Core has no such construct, so this is not a valid type.
+
+So, in the surface language `a` definitely IS in scope, and in the core language
+`a` definitely IS NOT in scope - we can't add a new binder.
+
+The solution is to reject such programs at elaboration time, and this is where
+`TypeVariablePE` comes in. We add forall'd type variables from the kind
+signature with such a placeholder into the scope of the type-checker and report an
+error with an explanation of the problem.
+-}
=====================================
compiler/GHC/Tc/Gen/HsType.hs
=====================================
@@ -1042,7 +1042,8 @@ tc_infer_hs_type mode (HsKindSig _ ty sig)
-- things like instantiate its foralls, so it needs
-- to be fully determined (#14904)
; traceTc "tc_infer_hs_type:sig" (ppr ty $$ ppr sig')
- ; ty' <- tc_lhs_type mode ty sig'
+ ; ty' <- tcAddKindSigPlaceholders sig $
+ tc_lhs_type mode ty sig'
; return (ty', sig') }
-- HsSpliced is an annotation produced by 'GHC.Rename.Splice.rnSpliceType' to communicate
=====================================
compiler/GHC/Tc/Types/BasicTypes.hs
=====================================
@@ -497,4 +497,4 @@ tcTyThingCategory (AGlobal thing) = tyThingCategory thing
tcTyThingCategory (ATyVar {}) = "type variable"
tcTyThingCategory (ATcId {}) = "local identifier"
tcTyThingCategory (ATcTyCon {}) = "local tycon"
-tcTyThingCategory (APromotionErr pe) = peCategory pe
\ No newline at end of file
+tcTyThingCategory (APromotionErr pe) = peCategory pe
=====================================
compiler/GHC/Tc/Utils/Env.hs
=====================================
@@ -43,7 +43,7 @@ module GHC.Tc.Utils.Env(
getInLocalScope,
wrongThingErr, pprBinders,
- tcAddDataFamConPlaceholders, tcAddPatSynPlaceholders,
+ tcAddDataFamConPlaceholders, tcAddPatSynPlaceholders, tcAddKindSigPlaceholders,
getTypeSigNames,
tcExtendRecEnv, -- For knot-tying
@@ -705,6 +705,12 @@ tcAddPatSynPlaceholders pat_syns thing_inside
| PSB{ psb_id = L _ name } <- pat_syns ]
thing_inside
+tcAddKindSigPlaceholders :: LHsKind GhcRn -> TcM a -> TcM a
+tcAddKindSigPlaceholders kind_sig thing_inside
+ = tcExtendKindEnvList [ (name, APromotionErr TypeVariablePE)
+ | name <- hsScopedKiVs kind_sig ]
+ thing_inside
+
getTypeSigNames :: [LSig GhcRn] -> NameSet
-- Get the names that have a user type sig
getTypeSigNames sigs
=====================================
testsuite/tests/rename/should_fail/T16635a.hs
=====================================
@@ -0,0 +1,11 @@
+{-# LANGUAGE NoScopedTypeVariables, ExplicitForAll #-}
+{-# LANGUAGE DataKinds, PolyKinds, TypeApplications #-}
+
+module T16635a where
+
+data Unit = U
+data P a = MkP
+
+-- ScopedTypeVariables are disabled.
+-- Fails because because @a is not in scope.
+type F = (Just @a :: forall a. a -> Maybe a) U
=====================================
testsuite/tests/rename/should_fail/T16635a.stderr
=====================================
@@ -0,0 +1,3 @@
+
+T16635a.hs:11:17: error: [GHC-76037]
+ Not in scope: type variable ‘a’
=====================================
testsuite/tests/rename/should_fail/T16635b.hs
=====================================
@@ -0,0 +1,14 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE DataKinds, PolyKinds, TypeApplications #-}
+
+module T16635b where
+
+data Unit = U
+data P a = MkP
+
+-- OK.
+f = (Just @a :: forall a. a -> Maybe a) U
+
+-- Fails because we cannot generalize to (/\a. Just @a)
+-- but NOT because @a is not in scope.
+type F = (Just @a :: forall a. a -> Maybe a) U
=====================================
testsuite/tests/rename/should_fail/T16635b.stderr
=====================================
@@ -0,0 +1,7 @@
+
+T16635b.hs:14:17: error: [GHC-88634]
+ • Type variable ‘a’ cannot be used here
+ (forall-bound variables cannot be used in kinds)
+ • In the first argument of ‘Just’, namely ‘a’
+ In the type ‘(Just @a :: forall a. a -> Maybe a) U’
+ In the type declaration for ‘F’
=====================================
testsuite/tests/rename/should_fail/all.T
=====================================
@@ -198,3 +198,5 @@ test('RnUnexpectedStandaloneDeriving', normal, compile_fail, [''])
test('RnStupidThetaInGadt', normal, compile_fail, [''])
test('PackageImportsDisabled', normal, compile_fail, [''])
test('ImportLookupIllegal', normal, compile_fail, [''])
+test('T16635a', normal, compile_fail, [''])
+test('T16635b', normal, compile_fail, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/5e5df728a2ec82b6c5bc3d9d1fd0feb958e292a1
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/5e5df728a2ec82b6c5bc3d9d1fd0feb958e292a1
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/20230608/6ae1967c/attachment-0001.html>
More information about the ghc-commits
mailing list