[Git][ghc/ghc][wip/sand-witch/DIB-instances] Implement the -Wimplicit-rhs-quantification warning (#23510)

Andrei Borzenkov (@sand-witch) gitlab at gitlab.haskell.org
Wed Jun 14 11:42:31 UTC 2023



Andrei Borzenkov pushed to branch wip/sand-witch/DIB-instances at Glasgow Haskell Compiler / GHC


Commits:
17b2cd17 by Andrei Borzenkov at 2023-06-14T15:42:00+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.

- - - - -


19 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/ghci/scripts/ghci024.stdout-mingw32
- + 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.8
    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 =
+      addDiagnosticAt (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.8
+    :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/ghci/scripts/ghci024.stdout-mingw32
=====================================
@@ -17,6 +17,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/17b2cd17089f1822d2d487af45d48c6cfc96349e

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/17b2cd17089f1822d2d487af45d48c6cfc96349e
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/20230614/5369f66c/attachment-0001.html>


More information about the ghc-commits mailing list