[Git][ghc/ghc][wip/sand-witch/DIB-instances] Implement the -Wimplicit-rhs-quantification warning (#23510)
Andrei Borzenkov (@sand-witch)
gitlab at gitlab.haskell.org
Mon Jun 12 13:08:44 UTC 2023
Andrei Borzenkov pushed to branch wip/sand-witch/DIB-instances at Glasgow Haskell Compiler / GHC
Commits:
e2c49dce by Andrei Borzenkov at 2023-06-12T17:08:29+04:00
Implement the -Wimplicit-rhs-quantification warning (#23510)
GHC Proposal #425 "Invisible binders in type declarations" forbids
implicit quantification of type variables that occur free on the
right-hand side of a type synonym but are not mentioned on the left-hand side.
The users are expected to rewrite this using invisible binders:
type T1 :: forall a . Maybe a
type T1 = 'Nothing :: Maybe a -- old
type T1 @a = 'Nothing :: Maybe a -- new
Since the @k-binders are a new feature, we need to wait for three releases
before we require the use of the new syntax. In the meantime, we ought to
provide users with a new warning, -Wimplicit-rhs-quantification, that would
detect when such implicit quantification takes place, and include it in -Wcompat.
- - - - -
18 changed files:
- compiler/GHC/Driver/Flags.hs
- compiler/GHC/Driver/Session.hs
- compiler/GHC/Rename/HsType.hs
- compiler/GHC/Rename/Module.hs
- compiler/GHC/Tc/Errors/Ppr.hs
- compiler/GHC/Tc/Errors/Types.hs
- compiler/GHC/Types/Error/Codes.hs
- compiler/GHC/Types/Hint.hs
- compiler/GHC/Types/Hint/Ppr.hs
- docs/users_guide/using-warnings.rst
- testsuite/tests/dependent/should_compile/T16391a.hs
- testsuite/tests/ghci/scripts/ghci024.stdout
- + testsuite/tests/rename/should_compile/T23510b.hs
- testsuite/tests/rename/should_compile/all.T
- + testsuite/tests/rename/should_fail/T23510a.hs
- + testsuite/tests/rename/should_fail/T23510a.stderr
- testsuite/tests/rename/should_fail/all.T
- testsuite/tests/typecheck/should_compile/T13343.hs
Changes:
=====================================
compiler/GHC/Driver/Flags.hs
=====================================
@@ -641,6 +641,7 @@ data WarningFlag =
| Opt_WarnLoopySuperclassSolve -- Since 9.6
| Opt_WarnTermVariableCapture -- Since 9.8
| Opt_WarnMissingRoleAnnotations -- Since 9.8
+ | Opt_WarnImplicitRhsQuantification -- Since 9.10
deriving (Eq, Ord, Show, Enum)
-- | Return the names of a WarningFlag
@@ -748,6 +749,7 @@ warnFlagNames wflag = case wflag of
Opt_WarnLoopySuperclassSolve -> "loopy-superclass-solve" :| []
Opt_WarnTypeEqualityRequiresOperators -> "type-equality-requires-operators" :| []
Opt_WarnMissingRoleAnnotations -> "missing-role-annotations" :| []
+ Opt_WarnImplicitRhsQuantification -> "implicit-rhs-quantification" :| []
-- -----------------------------------------------------------------------------
-- Standard sets of warning options
@@ -939,6 +941,7 @@ minusWcompatOpts
, Opt_WarnNonCanonicalMonadInstances
, Opt_WarnCompatUnqualifiedImports
, Opt_WarnTypeEqualityOutOfScope
+ , Opt_WarnImplicitRhsQuantification
]
-- | Things you get with -Wunused-binds
=====================================
compiler/GHC/Driver/Session.hs
=====================================
@@ -2259,7 +2259,8 @@ wWarningFlagsDeps = mconcat [
warnSpec Opt_WarnTypeEqualityOutOfScope,
warnSpec Opt_WarnTypeEqualityRequiresOperators,
warnSpec Opt_WarnTermVariableCapture,
- warnSpec Opt_WarnMissingRoleAnnotations
+ warnSpec Opt_WarnMissingRoleAnnotations,
+ warnSpec Opt_WarnImplicitRhsQuantification
]
warningGroupsDeps :: [(Deprecation, FlagSpec WarningGroup)]
=====================================
compiler/GHC/Rename/HsType.hs
=====================================
@@ -918,8 +918,8 @@ bindHsQTyVars :: forall a b.
-> Maybe a -- Just _ => an associated type decl
-> FreeKiTyVars -- Kind variables from scope
-> LHsQTyVars GhcPs
- -> (LHsQTyVars GhcRn -> Bool -> RnM (b, FreeVars))
- -- The Bool is True <=> all kind variables used in the
+ -> (LHsQTyVars GhcRn -> FreeKiTyVars -> RnM (b, FreeVars))
+ -- The FreeKiTyVars is null <=> all kind variables used in the
-- kind signature are bound on the left. Reason:
-- the last clause of Note [CUSKs: complete user-supplied kind signatures]
-- in GHC.Hs.Decls
@@ -942,7 +942,6 @@ bindHsQTyVars doc mb_assoc body_kv_occs hsq_bndrs thing_inside
bndr_kv_occs ++ body_kv_occs
body_remaining = filterFreeVarsToBind bndr_kv_occs $
filterFreeVarsToBind bndrs body_kv_occs
- all_bound_on_lhs = null body_remaining
; traceRn "checkMixedVars3" $
vcat [ text "bndrs" <+> ppr hs_tv_bndrs
@@ -969,7 +968,7 @@ bindHsQTyVars doc mb_assoc body_kv_occs hsq_bndrs thing_inside
; traceRn "bindHsQTyVars" (ppr hsq_bndrs $$ ppr implicit_kv_nms $$ ppr rn_bndrs)
; thing_inside (HsQTvs { hsq_ext = implicit_kv_nms
, hsq_explicit = rn_bndrs })
- all_bound_on_lhs } }
+ body_remaining } }
where
hs_tv_bndrs = hsQTvExplicit hsq_bndrs
@@ -1802,12 +1801,15 @@ one exists:
The logic resides in extractHsTyRdrTyVarsKindVars. We use it both for type
synonyms and type family instances.
-This is something of a stopgap solution until we can explicitly bind invisible
+This was a stopgap solution until we could explicitly bind invisible
type/kind variables:
type TySyn3 :: forall a. Maybe a
type TySyn3 @a = 'Just ('Nothing :: Maybe a)
+Now that the new syntax was proposed in #425 and implemented in 9.8, we issue a warning
+-Wimplicit-rhs-quantification for TySyn2 and TySyn4 and will eventually disallow them.
+
Note [Implicit quantification in type synonyms: non-taken alternatives]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
=====================================
compiler/GHC/Rename/Module.hs
=====================================
@@ -1709,11 +1709,16 @@ rnTyClDecl (SynDecl { tcdLName = tycon, tcdTyVars = tyvars,
; let kvs = extractHsTyRdrTyVarsKindVars rhs
doc = TySynCtx tycon
; traceRn "rntycl-ty" (ppr tycon <+> ppr kvs)
- ; bindHsQTyVars doc Nothing kvs tyvars $ \ tyvars' _ ->
- do { (rhs', fvs) <- rnTySyn doc rhs
+ ; bindHsQTyVars doc Nothing kvs tyvars $ \ tyvars' free_rhs_kvs ->
+ do { mapM_ warn_implicit_kvs (nubL free_rhs_kvs)
+ ; (rhs', fvs) <- rnTySyn doc rhs
; return (SynDecl { tcdLName = tycon', tcdTyVars = tyvars'
, tcdFixity = fixity
, tcdRhs = rhs', tcdSExt = fvs }, fvs) } }
+ where
+ warn_implicit_kvs :: LocatedN RdrName -> RnM ()
+ warn_implicit_kvs kv =
+ addErrAt (getLocA kv) (TcRnImplicitRhsQuantification kv)
-- "data", "newtype" declarations
rnTyClDecl (DataDecl
@@ -1725,12 +1730,12 @@ rnTyClDecl (DataDecl
doc = TyDataCtx tycon
new_or_data = dataDefnConsNewOrData cons
; traceRn "rntycl-data" (ppr tycon <+> ppr kvs)
- ; bindHsQTyVars doc Nothing kvs tyvars $ \ tyvars' no_rhs_kvs ->
+ ; bindHsQTyVars doc Nothing kvs tyvars $ \ tyvars' free_rhs_kvs ->
do { (defn', fvs) <- rnDataDefn doc defn
- ; cusk <- data_decl_has_cusk tyvars' new_or_data no_rhs_kvs kind_sig
+ ; cusk <- data_decl_has_cusk tyvars' new_or_data (null free_rhs_kvs) kind_sig
; let rn_info = DataDeclRn { tcdDataCusk = cusk
, tcdFVs = fvs }
- ; traceRn "rndata" (ppr tycon <+> ppr cusk <+> ppr no_rhs_kvs)
+ ; traceRn "rndata" (ppr tycon <+> ppr cusk <+> ppr free_rhs_kvs)
; return (DataDecl { tcdLName = tycon'
, tcdTyVars = tyvars'
, tcdFixity = fixity
=====================================
compiler/GHC/Tc/Errors/Ppr.hs
=====================================
@@ -1851,6 +1851,11 @@ instance Diagnostic TcRnMessage where
, text "or a complete user-supplied kind (CUSK, legacy feature)"
, text "is required to use invisible binders." ]
+ TcRnImplicitRhsQuantification kv -> mkSimpleDecorated $
+ vcat [ text "The variable" <+> quotes (ppr kv) <+> text "occurs free on the RHS of the type declaration"
+ , text "In the future GHC will no longer implicitly quantify over such variables"
+ ]
+
diagnosticReason = \case
TcRnUnknownMessage m
-> diagnosticReason m
@@ -2467,6 +2472,8 @@ instance Diagnostic TcRnMessage where
-> ErrorWithoutFlag
TcRnInvisBndrWithoutSig{}
-> ErrorWithoutFlag
+ TcRnImplicitRhsQuantification{}
+ -> WarningWithFlag Opt_WarnImplicitRhsQuantification
diagnosticHints = \case
TcRnUnknownMessage m
@@ -3130,6 +3137,8 @@ instance Diagnostic TcRnMessage where
-> noHints
TcRnInvisBndrWithoutSig name _
-> [SuggestAddStandaloneKindSignature name]
+ TcRnImplicitRhsQuantification kv
+ -> [SuggestBindTyVarOnLhs (unLoc kv)]
diagnosticCode :: TcRnMessage -> Maybe DiagnosticCode
diagnosticCode = constructorCode
=====================================
compiler/GHC/Tc/Errors/Types.hs
=====================================
@@ -4094,6 +4094,23 @@ data TcRnMessage where
-}
TcRnMissingRoleAnnotation :: Name -> [Role] -> TcRnMessage
+ {-| TcRnImplicitRhsQuantification is a warning that occurs when GHC implicitly
+ quantifies over a type variable that occurs free on the RHS of the type declaration
+ that is not mentioned on the LHS
+
+ Example:
+
+ type T = 'Nothing :: Maybe a
+
+ Controlled by flags:
+ - Wimplicit-rhs-quantification
+
+ Test cases:
+ T23510a
+ T23510b
+ -}
+ TcRnImplicitRhsQuantification :: LocatedN RdrName -> TcRnMessage
+
deriving Generic
=====================================
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 "TcRnImplicitRhsQuantification" = 16382
-- TcRnTypeApplicationsDisabled
GhcDiagnosticCode "TypeApplication" = 23482
=====================================
compiler/GHC/Types/Hint.hs
=====================================
@@ -465,6 +465,9 @@ data GhcHint
{-| Suggest eta-reducing a type synonym used in the implementation
of abstract data. -}
| SuggestEtaReduceAbsDataTySyn TyCon
+ {-| Suggest binding the type variable on the LHS of the type declaration
+ -}
+ | SuggestBindTyVarOnLhs RdrName
-- | An 'InstantiationSuggestion' for a '.hsig' file. This is generated
-- by GHC in case of a 'DriverUnexpectedSignature' and suggests a way
=====================================
compiler/GHC/Types/Hint/Ppr.hs
=====================================
@@ -251,6 +251,8 @@ instance Outputable GhcHint where
SuggestEtaReduceAbsDataTySyn tc
-> text "If possible, eta-reduce the type synonym" <+> ppr_tc <+> text "so that it is nullary."
where ppr_tc = quotes (ppr $ tyConName tc)
+ SuggestBindTyVarOnLhs tv
+ -> text "Bind" <+> quotes (ppr tv) <+> text "on the LHS of the type declaration"
perhapsAsPat :: SDoc
perhapsAsPat = text "Perhaps you meant an as-pattern, which must not be surrounded by whitespace"
=====================================
docs/users_guide/using-warnings.rst
=====================================
@@ -166,6 +166,7 @@ as ``-Wno-...`` for every individual warning in the group.
* :ghc-flag:`-Wnoncanonical-monad-instances`
* :ghc-flag:`-Wcompat-unqualified-imports`
* :ghc-flag:`-Wtype-equality-out-of-scope`
+ * :ghc-flag:`-Wimplicit-rhs-quantification`
.. ghc-flag:: -w
:shortdesc: disable all warnings
@@ -2415,6 +2416,28 @@ of ``-W(no-)*``.
In other words the type-class role cannot be accidentally left
representational or phantom, which could affected the code correctness.
+.. ghc-flag:: -Wimplicit-rhs-quantification
+ :shortdesc: warn when type variables on the RHS of a type synonym are implicitly quantified
+ :type: dynamic
+ :reverse: -Wno-implicit-rhs-quantification
+ :category:
+
+ :since: 9.10
+ :default: off
+
+ In accordance with `GHC Proposal #425
+ <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0425-decl-invis-binders.rst>`__,
+ GHC will stop implicitly quantifying over type variables that occur free on the
+ right-hand side of a type synonym but are not mentioned on the left-hand side.
+ Type synonym declarations that rely on this form of quantification should be rewritten with invisible binders.
+
+ For example: ::
+
+ type T1 :: forall a . Maybe a
+ type T1 = 'Nothing :: Maybe a -- old
+ type T1 @a = 'Nothing :: Maybe a -- new
+
+ This warning detects code that will be affected by this breaking change.
If you're feeling really paranoid, the :ghc-flag:`-dcore-lint` option is a good choice.
It turns on heavyweight intra-pass sanity-checking within GHC. (It checks GHC's
=====================================
testsuite/tests/dependent/should_compile/T16391a.hs
=====================================
@@ -9,7 +9,8 @@ import Data.Kind
type Const (a :: Type) (b :: Type) = a
type family F :: Const Type a where
F = Int
-type TS = (Int :: Const Type a)
+type TS :: forall a . Const Type a
+type TS @a = (Int :: Const Type a)
data T1 :: Const Type a where
MkT1 :: T1
data T2 :: Const Type a -> Type where
=====================================
testsuite/tests/ghci/scripts/ghci024.stdout
=====================================
@@ -18,6 +18,7 @@ warning settings:
-Wsemigroup
-Wcompat-unqualified-imports
-Wtype-equality-out-of-scope
+ -Wimplicit-rhs-quantification
~~~~~~~~~~ Testing :set -a
options currently set: none.
base language is: GHC2021
=====================================
testsuite/tests/rename/should_compile/T23510b.hs
=====================================
@@ -0,0 +1,14 @@
+{-# OPTIONS -Wimplicit-rhs-quantification #-}
+{-# LANGUAGE DataKinds, TypeAbstractions #-}
+module T23510b where
+
+import Data.Proxy
+
+type T1 :: forall k . Maybe k
+type T1 @a = 'Nothing :: Maybe a
+
+type T2 :: forall k j . k -> Either k j
+type T2 @a @b = 'Left :: a -> Either a b
+
+type T3 :: forall {k} (d :: k) . Proxy k
+type T3 @(a :: k) = 'Proxy :: Proxy k
=====================================
testsuite/tests/rename/should_compile/all.T
=====================================
@@ -212,3 +212,4 @@ test('T22122', [expect_broken(22122), extra_files(['T22122_aux.hs'])], multimod_
test('T23240', [req_th, extra_files(['T23240_aux.hs'])], multimod_compile, ['T23240', '-v0'])
test('T23318', normal, compile, ['-Wduplicate-exports'])
test('T23434', normal, compile, [''])
+test('T23510b', normal, compile, [''])
=====================================
testsuite/tests/rename/should_fail/T23510a.hs
=====================================
@@ -0,0 +1,17 @@
+{-# OPTIONS -Wimplicit-rhs-quantification #-}
+{-# LANGUAGE DataKinds #-}
+module T23510a where
+
+import Data.Proxy
+import GHC.Types
+
+type T1 = 'Nothing :: Maybe a
+
+type T2 = 'Left :: a -> Either a b
+
+type T3 = 'Proxy :: Proxy k
+
+type Const (a :: Type) (b :: Type) = a
+type TS = (Int :: Const Type a)
+
+type Bad = (forall (v1 :: RuntimeRep) (a1 :: TYPE v). a1) :: TYPE v
=====================================
testsuite/tests/rename/should_fail/T23510a.stderr
=====================================
@@ -0,0 +1,30 @@
+
+T23510a.hs:8:29: error: [GHC-16382] [-Wimplicit-rhs-quantification (in -Wcompat), Werror=implicit-rhs-quantification]
+ The variable ‘a’ occurs free on the RHS of the type declaration
+ In the future GHC will no longer implicitly quantify over such variables
+ Suggested fix: Bind ‘a’ on the LHS of the type declaration
+
+T23510a.hs:10:20: error: [GHC-16382] [-Wimplicit-rhs-quantification (in -Wcompat), Werror=implicit-rhs-quantification]
+ The variable ‘a’ occurs free on the RHS of the type declaration
+ In the future GHC will no longer implicitly quantify over such variables
+ Suggested fix: Bind ‘a’ on the LHS of the type declaration
+
+T23510a.hs:10:34: error: [GHC-16382] [-Wimplicit-rhs-quantification (in -Wcompat), Werror=implicit-rhs-quantification]
+ The variable ‘b’ occurs free on the RHS of the type declaration
+ In the future GHC will no longer implicitly quantify over such variables
+ Suggested fix: Bind ‘b’ on the LHS of the type declaration
+
+T23510a.hs:12:27: error: [GHC-16382] [-Wimplicit-rhs-quantification (in -Wcompat), Werror=implicit-rhs-quantification]
+ The variable ‘k’ occurs free on the RHS of the type declaration
+ In the future GHC will no longer implicitly quantify over such variables
+ Suggested fix: Bind ‘k’ on the LHS of the type declaration
+
+T23510a.hs:15:30: error: [GHC-16382] [-Wimplicit-rhs-quantification (in -Wcompat), Werror=implicit-rhs-quantification]
+ The variable ‘a’ occurs free on the RHS of the type declaration
+ In the future GHC will no longer implicitly quantify over such variables
+ Suggested fix: Bind ‘a’ on the LHS of the type declaration
+
+T23510a.hs:17:67: error: [GHC-16382] [-Wimplicit-rhs-quantification (in -Wcompat), Werror=implicit-rhs-quantification]
+ The variable ‘v’ occurs free on the RHS of the type declaration
+ In the future GHC will no longer implicitly quantify over such variables
+ Suggested fix: Bind ‘v’ on the LHS of the type declaration
=====================================
testsuite/tests/rename/should_fail/all.T
=====================================
@@ -198,3 +198,4 @@ test('RnUnexpectedStandaloneDeriving', normal, compile_fail, [''])
test('RnStupidThetaInGadt', normal, compile_fail, [''])
test('PackageImportsDisabled', normal, compile_fail, [''])
test('ImportLookupIllegal', normal, compile_fail, [''])
+test('T23510a', normal, compile_fail, [''])
=====================================
testsuite/tests/typecheck/should_compile/T13343.hs
=====================================
@@ -4,6 +4,7 @@ module Bug where
import GHC.Exts
-type Bad = (forall (v1 :: RuntimeRep) (a1 :: TYPE v). a1) :: TYPE v
+type Bad :: forall v . TYPE v
+type Bad @v = (forall (v1 :: RuntimeRep) (a1 :: TYPE v). a1) :: TYPE v
--- should be accepted because GHC will generalize over v. Note v /= v1.
+-- Note v /= v1.
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/e2c49dce45b11f18d24b082edd9bcba25fad82a1
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/e2c49dce45b11f18d24b082edd9bcba25fad82a1
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/20230612/89dd7532/attachment-0001.html>
More information about the ghc-commits
mailing list