[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 09:29:15 UTC 2023
Andrei Borzenkov pushed to branch wip/sand-witch/#16635-improve-errors at Glasgow Haskell Compiler / GHC
Commits:
c4232c36 by Andrei Borzenkov at 2023-06-08T13:29:01+04:00
Capture scoped kind variables at type-checking phase (#16635)
Like descibed in new Note [A 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.
- - - - -
14 changed files:
- compiler/GHC/Hs/Type.hs
- compiler/GHC/Rename/HsType.hs
- compiler/GHC/Tc/Errors/Ppr.hs
- compiler/GHC/Tc/Errors/Types.hs
- compiler/GHC/Tc/Gen/HsType.hs
- compiler/GHC/Tc/Gen/Splice.hs
- compiler/GHC/Tc/Types/BasicTypes.hs
- compiler/GHC/Tc/Utils/Env.hs
- compiler/GHC/Types/Error/Codes.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
=====================================
@@ -1826,6 +1826,11 @@ instance Diagnostic TcRnMessage where
TcRnIllegalQuasiQuotes -> mkSimpleDecorated $
text "Quasi-quotes are not permitted without QuasiQuotes"
TcRnTHError err -> pprTHError err
+ TcRnAScopingError where_ty tv_name -> mkSimpleDecorated $
+ vcat
+ [ text "Cannot generalise type" <+> ppr where_ty
+ , text "to /\\" <+> ppr tv_name <+> text "->" <+> ppr where_ty
+ ]
TcRnIllegalInvisTyVarBndr bndr ->
mkSimpleDecorated $
@@ -2467,6 +2472,8 @@ instance Diagnostic TcRnMessage where
-> ErrorWithoutFlag
TcRnInvisBndrWithoutSig{}
-> ErrorWithoutFlag
+ TcRnAScopingError{}
+ -> ErrorWithoutFlag
diagnosticHints = \case
TcRnUnknownMessage m
@@ -3130,6 +3137,8 @@ instance Diagnostic TcRnMessage where
-> noHints
TcRnInvisBndrWithoutSig name _
-> [SuggestAddStandaloneKindSignature name]
+ TcRnAScopingError{}
+ -> noHints
diagnosticCode :: TcRnMessage -> Maybe DiagnosticCode
diagnosticCode = constructorCode
=====================================
compiler/GHC/Tc/Errors/Types.hs
=====================================
@@ -4094,6 +4094,24 @@ data TcRnMessage where
-}
TcRnMissingRoleAnnotation :: Name -> [Role] -> TcRnMessage
+ {-| TcRnAScopingError is an error that occurs when type mentions
+ kind variables bringed by the forall of kind signature.
+ For more information see Note [Scoping errors during type check] in GHC.Tc.Types.BasicTypes
+
+ Example:
+
+ type F = '[Left @a :: forall a. a -> Either a ()]
+ -- ^ rejected
+
+ Test cases:
+ T16635a
+ T16635b
+ -}
+ TcRnAScopingError
+ :: LHsType GhcRn -- where
+ -> Name -- what
+ -> TcRnMessage
+
deriving Generic
=====================================
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 ty $
+ tc_lhs_type mode ty sig'
; return (ty', sig') }
-- HsSpliced is an annotation produced by 'GHC.Rename.Splice.rnSpliceType' to communicate
@@ -1994,6 +1995,8 @@ tcTyVar name -- Could be a tyvar, a tycon, or a datacon
APromotionErr err -> promotionErr name err
+ AScopingError ty -> failWithTc (TcRnAScopingError ty name)
+
_ -> wrongThingErr WrongThingType thing name }
{-
=====================================
compiler/GHC/Tc/Gen/Splice.hs
=====================================
@@ -2830,6 +2830,7 @@ reifyTypeOfThing th_name = do
AGlobal (ACoAxiom _) -> panic "reifyTypeOfThing: ACoAxiom"
ATcTyCon _ -> panic "reifyTypeOfThing: ATcTyCon"
APromotionErr _ -> panic "reifyTypeOfThing: APromotionErr"
+ AScopingError{} -> panic "reifyTypeOfThing: AScopingError"
------------------------------
lookupThAnnLookup :: TH.AnnLookup -> TcM CoreAnnTarget
=====================================
compiler/GHC/Tc/Types/BasicTypes.hs
=====================================
@@ -39,7 +39,7 @@ import GHC.Tc.Utils.TcType
import GHC.Hs.Extension ( GhcRn )
-import Language.Haskell.Syntax.Type ( LHsSigWcType )
+import Language.Haskell.Syntax.Type ( LHsSigWcType, LHsType )
import GHC.Tc.Errors.Types.PromotionErr (PromotionErr, peCategory)
@@ -298,6 +298,10 @@ data TcTyThing
| APromotionErr PromotionErr
+ | AScopingError (LHsType GhcRn) -- See Note [Scoping errors during type check]
+ -- The argument is the type where scoping error may occur,
+ -- and is only required for error reporting.
+
-- | Matches on either a global 'TyCon' or a 'TcTyCon'.
tcTyThingTyCon_maybe :: TcTyThing -> Maybe TyCon
tcTyThingTyCon_maybe (AGlobal (ATyCon tc)) = Just tc
@@ -314,6 +318,7 @@ instance Outputable TcTyThing where -- Debugging only
<+> dcolon <+> ppr (varType tv)
ppr (ATcTyCon tc) = text "ATcTyCon" <+> ppr tc <+> dcolon <+> ppr (tyConKind tc)
ppr (APromotionErr err) = text "APromotionErr" <+> ppr err
+ ppr (AScopingError ty) = text "AScopingError" <+> ppr ty
-- | IdBindingInfo describes how an Id is bound.
--
@@ -480,6 +485,45 @@ in the type environment.
type environment so in the latter case it always stays as a
unification variable, although that variable may be later
unified with a type (such as Int in 'g2').
+
+Note [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
+`AScopingError` 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 - like in `APromotionErr`.
-}
instance Outputable IdBindingInfo where
@@ -497,4 +541,5 @@ 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
+tcTyThingCategory AScopingError{} = "type variable"
=====================================
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
@@ -509,7 +509,7 @@ getInLocalScope = do { lcl_env <- getLclTypeEnv
tcExtendKindEnvList :: [(Name, TcTyThing)] -> TcM r -> TcM r
-- Used only during kind checking, for TcThings that are
--- ATcTyCon or APromotionErr
+-- ATcTyCon, APromotionErr or AScopingError
-- No need to update the global tyvars, or tcl_th_bndrs, or tcl_rdr
tcExtendKindEnvList things thing_inside
= do { traceTc "tcExtendKindEnvList" (ppr things)
@@ -705,6 +705,12 @@ tcAddPatSynPlaceholders pat_syns thing_inside
| PSB{ psb_id = L _ name } <- pat_syns ]
thing_inside
+tcAddKindSigPlaceholders :: LHsKind GhcRn -> LHsType GhcRn -> TcM a -> TcM a
+tcAddKindSigPlaceholders kind_sig type_we_traverse_in thing_inside
+ = tcExtendKindEnvList [ (name, AScopingError type_we_traverse_in)
+ | name <- hsScopedKiVs kind_sig ]
+ thing_inside
+
getTypeSigNames :: [LSig GhcRn] -> NameSet
-- Get the names that have a user type sig
getTypeSigNames sigs
=====================================
compiler/GHC/Types/Error/Codes.hs
=====================================
@@ -591,6 +591,7 @@ type family GhcDiagnosticCode c = n | n -> c where
GhcDiagnosticCode "TcRnArityMismatch" = 27346
GhcDiagnosticCode "TcRnSimplifiableConstraint" = 62412
GhcDiagnosticCode "TcRnIllegalQuasiQuotes" = 77343
+ GhcDiagnosticCode "TcRnAScopingError" = 34573
-- TcRnTypeApplicationsDisabled
GhcDiagnosticCode "TypeApplication" = 23482
=====================================
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-34573]
+ • Cannot generalise type Just @a
+ to /\ a -> Just @a
+ • 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/c4232c36ca88cb34fcc9d8889bd21290b0c5f742
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/c4232c36ca88cb34fcc9d8889bd21290b0c5f742
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/a490beb7/attachment-0001.html>
More information about the ghc-commits
mailing list