[Git][ghc/ghc][wip/T24359] Add -Wrule-lhs-equalities warning

sheaf (@sheaf) gitlab at gitlab.haskell.org
Mon Dec 30 12:18:56 UTC 2024



sheaf pushed to branch wip/T24359 at Glasgow Haskell Compiler / GHC


Commits:
6e088685 by sheaf at 2024-12-30T13:18:46+01:00
Add -Wrule-lhs-equalities warning

This commit adds a new warning flag, -Wrule-lhs-equalities, which
controls the warning message that is emitted when the LHS of a RULE
gives rise to equality constraints that previous GHC versions would
have quantified over.

GHC instead discards such RULES, as GHC was never able to generate
a rule template that would ever fire; it's better to be explicit about
the fact that the RULE doesn't work.

- - - - -


11 changed files:

- compiler/GHC/Driver/Flags.hs
- compiler/GHC/Driver/Session.hs
- compiler/GHC/Tc/Errors/Ppr.hs
- compiler/GHC/Tc/Errors/Types.hs
- compiler/GHC/Tc/Gen/Sig.hs
- compiler/GHC/Types/Error/Codes.hs
- docs/users_guide/9.14.1-notes.rst
- docs/users_guide/using-warnings.rst
- + testsuite/tests/typecheck/should_compile/RuleEqs.hs
- + testsuite/tests/typecheck/should_compile/RuleEqs.stderr
- testsuite/tests/typecheck/should_compile/all.T


Changes:

=====================================
compiler/GHC/Driver/Flags.hs
=====================================
@@ -1073,6 +1073,7 @@ data WarningFlag =
    | Opt_WarnViewPatternSignatures                   -- Since 9.12
    | Opt_WarnUselessSpecialisations                  -- Since 9.14
    | Opt_WarnDeprecatedPragmas                       -- Since 9.14
+   | Opt_WarnRuleLhsEqualities                       -- Since 9.14
    deriving (Eq, Ord, Show, Enum, Bounded)
 
 -- | Return the names of a WarningFlag
@@ -1191,6 +1192,7 @@ warnFlagNames wflag = case wflag of
   Opt_WarnViewPatternSignatures                   -> "view-pattern-signatures" :| []
   Opt_WarnUselessSpecialisations                  -> "useless-specialisations" :| ["useless-specializations"]
   Opt_WarnDeprecatedPragmas                       -> "deprecated-pragmas" :| []
+  Opt_WarnRuleLhsEqualities                       -> "rule-lhs-equalities" :| []
 
 -- -----------------------------------------------------------------------------
 -- Standard sets of warning options
@@ -1334,7 +1336,8 @@ standardWarnings -- see Note [Documenting warning flags]
         Opt_WarnTypeEqualityOutOfScope,
         Opt_WarnViewPatternSignatures,
         Opt_WarnUselessSpecialisations,
-        Opt_WarnDeprecatedPragmas
+        Opt_WarnDeprecatedPragmas,
+        Opt_WarnRuleLhsEqualities
       ]
 
 -- | Things you get with -W


=====================================
compiler/GHC/Driver/Session.hs
=====================================
@@ -2361,6 +2361,7 @@ wWarningFlagsDeps = [minBound..maxBound] >>= \x -> case x of
   Opt_WarnViewPatternSignatures -> warnSpec x
   Opt_WarnUselessSpecialisations -> warnSpec x
   Opt_WarnDeprecatedPragmas -> warnSpec x
+  Opt_WarnRuleLhsEqualities -> warnSpec x
 
 warningGroupsDeps :: [(Deprecation, FlagSpec WarningGroup)]
 warningGroupsDeps = map mk warningGroups


=====================================
compiler/GHC/Tc/Errors/Ppr.hs
=====================================
@@ -1418,6 +1418,14 @@ instance Diagnostic TcRnMessage where
         err = case errReason of
           UnboundVariable uv nis -> pprScopeError uv nis
           IllegalExpression -> text "Illegal expression:" <+> ppr bad_e
+    TcRnRuleLhsEqualities ruleName _lhs cts -> mkSimpleDecorated $
+      text "Discarding RULE" <+> doubleQuotes (ftext ruleName) <> dot
+      $$
+      hang
+        (sep [ text "The LHS of this rule gave rise to equality constraints"
+             , text "that GHC was unable to quantify over:" ]
+        )
+        4 (pprWithArising $ NE.toList cts)
     TcRnDuplicateRoleAnnot list -> mkSimpleDecorated $
       hang (text "Duplicate role annotations for" <+>
             quotes (ppr $ roleAnnotDeclName first_decl) <> colon)
@@ -2424,6 +2432,8 @@ instance Diagnostic TcRnMessage where
       -> ErrorWithoutFlag
     TcRnIllegalRuleLhs{}
       -> ErrorWithoutFlag
+    TcRnRuleLhsEqualities{}
+      -> WarningWithFlag Opt_WarnRuleLhsEqualities
     TcRnDuplicateRoleAnnot{}
       -> ErrorWithoutFlag
     TcRnDuplicateKindSig{}
@@ -3099,6 +3109,8 @@ instance Diagnostic TcRnMessage where
       -> [suggestExtension LangExt.StandaloneKindSignatures]
     TcRnIllegalRuleLhs{}
       -> noHints
+    TcRnRuleLhsEqualities{}
+      -> noHints
     TcRnDuplicateRoleAnnot{}
       -> noHints
     TcRnDuplicateKindSig{}


=====================================
compiler/GHC/Tc/Errors/Types.hs
=====================================
@@ -3275,9 +3275,21 @@ data TcRnMessage where
   -}
   TcRnIllegalRuleLhs
     :: RuleLhsErrReason
-    -> FastString -- Rule name
-    -> LHsExpr GhcRn -- Full expression
-    -> HsExpr GhcRn -- Bad expression
+    -> FastString -- ^ Rule name
+    -> LHsExpr GhcRn -- ^ Full expression
+    -> HsExpr GhcRn -- ^ Bad expression
+    -> TcRnMessage
+
+  {-| TcRnRuleLhsEqualities is a warning, controlled by '-Wrule-lhs-equalities',
+      that is triggered by a RULE whose LHS contains equality constraints
+      (of a certain form, such as @F a ~ b@ for a type family @F@).
+
+      Test case: typecheck/should_compile/RuleEqs
+  -}
+  TcRnRuleLhsEqualities
+    :: FastString -- ^ rule name
+    -> LHsExpr GhcRn -- ^ LHS expression
+    -> NE.NonEmpty Ct -- ^ LHS equality constraints
     -> TcRnMessage
 
   {-| TcRnDuplicateRoleAnnot is an error triggered by two or more role


=====================================
compiler/GHC/Tc/Gen/Sig.hs
=====================================
@@ -82,9 +82,10 @@ import GHC.Utils.Panic
 import GHC.Data.Bag
 import GHC.Data.Maybe( orElse, whenIsJust )
 
-import Data.Maybe( mapMaybe )
-import qualified Data.List.NonEmpty as NE
 import Control.Monad( unless )
+import Data.Foldable ( toList )
+import qualified Data.List.NonEmpty as NE
+import Data.Maybe( mapMaybe )
 
 
 {- -------------------------------------------------------------
@@ -1195,18 +1196,17 @@ tcRule (HsRule { rd_ext  = ext
                                   vcat [ ppr id <+> dcolon <+> ppr (idType id) | id <- tpl_ids ]
                   ])
 
-       -- /Temporarily/ deal with the fact that we previously accepted a RULE that quantified
-       -- over equalities.  If all the residual LHS constraints are previously-quantifiable
-       -- equalities, and the RHS constraints are not insoluble (if they are, just report those
-       -- errors), then emit a warning and discard the rule entirely.
-       -- Eliminate this deprecation warning in due course!
+       -- /Temporarily/ deal with the fact that we previously accepted
+       -- rules that quantify over certain equality constraints.
+       --
+       -- See Note [Quantifying over equalities in RULES].
        ; case allPreviouslyQuantifiableEqualities residual_lhs_wanted of {
            Just cts | not (insolubleWC rhs_wanted)
-                    -> pprTrace "tcRule: discarding" (ppr cts) $
-                       return Nothing ;
-           Nothing  ->
+                    -> do { addDiagnostic $ TcRnRuleLhsEqualities name lhs cts
+                          ; return Nothing } ;
+           _  ->
 
-   do  { -- SimplfyRule Plan, step 5
+   do  { -- SimplifyRule Plan, step 5
        -- Simplify the LHS and RHS constraints:
        -- For the LHS constraints we must solve the remaining constraints
        -- (a) so that we report insoluble ones
@@ -1553,24 +1553,85 @@ getRuleQuantCts wc
      | otherwise
      = pprPanic "getRuleQuantCts" (ppr ct)
 
-allPreviouslyQuantifiableEqualities :: WantedConstraints -> Maybe [Ct]
+
+{- Note [Quantifying over equalities in RULES]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Up until version 9.12 (included), GHC would happily quantify over certain Wanted
+equalities in the LHS of a RULE. This was incorrect behaviour that lead to a
+RULE that would never fire, so GHC 9.14 and above no longer allow such RULES.
+However, instead of throwing an error, GHC will /temporarily/ emit a warning
+and drop the rule instead, in order to ease migration for library maintainers
+(NB: this warning is not emitted when the RHS constraints are insoluble; in that
+case we simply report those constraints as errors instead).
+
+The function 'allPreviouslyQuantifiableEqualities' computes the equality
+constraints that previous (<= 9.12) versions of GHC accepted quantifying over.
+
+
+  Example (test case 'RuleEqs', extracted from the 'mono-traversable' library):
+
+    type family Element mono
+    type instance Element [a] = a
+
+    class MonoFoldable mono where
+        otoList :: mono -> [Element mono]
+    instance MonoFoldable [a] where
+        otoList = id
+
+    ointercalate :: (MonoFoldable mono, Monoid (Element mono))
+                 => Element mono -> mono -> Element mono
+    {-# RULES "ointercalate list" forall x. ointercalate x = Data.List.intercalate x . otoList #-}
+
+  Now, because Data.List.intercalate has the type signature
+
+    forall a. [a] -> [[a]] -> [a]
+
+  typechecking the LHS of this rule would give rise to the Wanted equality
+
+    [W] Element mono ~ [a]
+
+  Due to the type family, GHC 9.12 and below accepted to quantify over this
+  equality, which would lead to a rule LHS template of the form:
+
+    forall (@mono) (@a)
+           ($dMonoFoldable :: MonoFoldable mono)
+           ($dMonoid :: Monoid (Element mono))
+           (co :: [a] ~ Element mono)
+           (x :: [a]).
+      ointercalate @mono $dMonoFoldable $dMonoid
+        (x `cast` (Sub co))
+
+  Matching against this template would match on the structure of a coercion,
+  which goes against Note [Casts in the template] in GHC.Core.Rules.
+  In practice, this meant that this RULE would never fire.
+-}
+
+-- | Computes all equality constraints that GHC doesn't accept, but previously
+-- did accept (until GHC 9.12 (included)), when deciding what to quantify over
+-- in the LHS of a RULE.
+--
+-- See Note [Quantifying over equalities in RULES].
+allPreviouslyQuantifiableEqualities :: WantedConstraints -> Maybe (NE.NonEmpty Ct)
 allPreviouslyQuantifiableEqualities wc = go emptyVarSet wc
   where
+    go :: TyVarSet -> WantedConstraints -> Maybe (NE.NonEmpty Ct)
     go skol_tvs (WC { wc_simple = simples, wc_impl = implics })
-      = do { cts1 <- mapM (go_simple skol_tvs) simples
-           ; cts2 <- mapM (go_implic skol_tvs) implics
-           ; return (concat cts1 ++ concat cts2) }
+      = do { cts1 <-       mapM (go_simple skol_tvs) simples
+           ; cts2 <- concatMapM (go_implic skol_tvs) implics
+           ; NE.nonEmpty $ toList cts1 ++ toList cts2 }
 
+    go_simple :: TyVarSet -> Ct -> Maybe Ct
     go_simple skol_tvs ct
       | not (tyCoVarsOfCt ct `disjointVarSet` skol_tvs)
       = Nothing
       | EqPred _ t1 t2 <- classifyPredType (ctPred ct), ok_eq t1 t2
-      = Just [ct]
+      = Just ct
       | otherwise
       = Nothing
 
+    go_implic :: TyVarSet -> Implication -> Maybe [Ct]
     go_implic skol_tvs (Implic { ic_skols = skols, ic_wanted = wc })
-      = go (skol_tvs `extendVarSetList` skols) wc
+      = fmap toList $ go (skol_tvs `extendVarSetList` skols) wc
 
     ok_eq t1 t2
        | t1 `tcEqType` t2 = False


=====================================
compiler/GHC/Types/Error/Codes.hs
=====================================
@@ -535,6 +535,7 @@ type family GhcDiagnosticCode c = n | n -> c where
   GhcDiagnosticCode "TcRnUnusedVariableInRuleDecl"                  = 65669
   GhcDiagnosticCode "TcRnUnexpectedStandaloneKindSig"               = 45906
   GhcDiagnosticCode "TcRnIllegalRuleLhs"                            = 63294
+  GhcDiagnosticCode "TcRnRuleLhsEqualities"                         = 53522
   GhcDiagnosticCode "TcRnDuplicateRoleAnnot"                        = 97170
   GhcDiagnosticCode "TcRnDuplicateKindSig"                          = 43371
   GhcDiagnosticCode "TcRnIllegalDerivStrategy"                      = 87139


=====================================
docs/users_guide/9.14.1-notes.rst
=====================================
@@ -25,9 +25,17 @@ Language
   This deprecation is controlled by the newly introduced ``-Wdeprecated-pragmas``
   flag in ``-Wdefault``.
 
-* A new flag, `-Wuseless-specialisations`, controls warnings emitted when GHC
+* A new flag, ``-Wuseless-specialisations``, controls warnings emitted when GHC
   determines that a SPECIALISE pragma would have no effect.
 
+* A new flag, ``-Wrule-lhs-equalities``, controls warnings emitted for RULES
+  whose left-hand side attempts to quantify over equality constraints that
+  previous GHC versions accepted quantifying over. GHC will now drop such RULES,
+  emitting a warning message controlled by this flag.
+
+  This warning is intended to give visibility to the fact that the RULES that
+  previous GHC versions generated in such circumstances could never fire.
+
 * ``-Wincomplete-record-selectors`` is now part of `-Wall`, as specified
   by `GHC Proposal 516: add warning for incomplete record selectors <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0516-incomplete-record-selectors.rst>`_.
   Hence, if a library is compiled with ``-Werror``, compilation may now fail. Solution: fix the library.


=====================================
docs/users_guide/using-warnings.rst
=====================================
@@ -436,6 +436,24 @@ of ``-W(no-)*``.
     uses multiple comma-separated type signatures (deprecated and scheduled
     to be removed in GHC 9.18).
 
+.. ghc-flag:: -Wrule-lhs-equalities
+    :shortdesc: warn about rules whose LHS contains equality constraints
+    :type: dynamic
+    :reverse: -Wno-rule-lhs-equalities
+    :category:
+
+    :since: 9.14
+
+    :default: on
+
+    When GHC encounters a RULE whose left-hand side gives rise to equality
+    constraints that previous GHC versions (``<= 9.12``) accepted quantifying
+    over, GHC will instead drop the rule and emit a warning message, with the
+    warning message being controlled by this flag.
+
+    This warning is intended to give visibility to the fact that the RULES that
+    previous GHC versions generated in such circumstances could never fire.
+
 .. ghc-flag:: -Wmissed-specialisations
     :shortdesc: warn when specialisation of an imported, overloaded function
         fails.


=====================================
testsuite/tests/typecheck/should_compile/RuleEqs.hs
=====================================
@@ -0,0 +1,24 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeFamilies     #-}
+{-# LANGUAGE TypeOperators    #-}
+
+module RuleEqs where
+
+import qualified Data.List
+
+type family Element mono
+type instance Element [a] = a
+
+class MonoFoldable mono where
+  otoList :: mono -> [Element mono]
+
+instance MonoFoldable [a] where
+  otoList = id
+
+ointercalate :: (MonoFoldable mono, Monoid (Element mono))
+             => Element mono
+             -> mono
+             -> Element mono
+ointercalate x = mconcat . Data.List.intersperse x . otoList
+{-# INLINE [0] ointercalate #-}
+{-# RULES "ointercalate list" forall x. ointercalate x = Data.List.intercalate x . otoList #-}


=====================================
testsuite/tests/typecheck/should_compile/RuleEqs.stderr
=====================================
@@ -0,0 +1,6 @@
+RuleEqs.hs:24:11: warning: [GHC-53522] [-Wrule-lhs-equalities (in -Wdefault)]
+    Discarding RULE "ointercalate list".
+    The LHS of this rule gave rise to equality constraints
+    that GHC was unable to quantify over:
+        [a0] ~ Element mono0
+


=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -737,6 +737,7 @@ test('T19042', normal, compile, [''])
 test('ExplicitSpecificityA1', normal, compile, [''])
 test('ExplicitSpecificityA2', normal, compile, [''])
 test('ExplicitSpecificity4', normal, compile, [''])
+test('RuleEqs', normal, compile, [''])
 test('T17775-viewpats-a', normal, compile, [''])
 test('T17775-viewpats-b', normal, compile_fail, [''])
 test('T17775-viewpats-c', normal, compile_fail, [''])



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/6e0886858c2732d68109bb253a702365ae259918

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/6e0886858c2732d68109bb253a702365ae259918
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/20241230/c7488469/attachment-0001.html>


More information about the ghc-commits mailing list