[Git][ghc/ghc][wip/T24359] Add -Wrule-lhs-equalities warning
sheaf (@sheaf)
gitlab at gitlab.haskell.org
Wed Mar 12 13:47:32 UTC 2025
sheaf pushed to branch wip/T24359 at Glasgow Haskell Compiler / GHC
Commits:
10f59a44 by Simon Peyton Jones at 2025-03-12T14:47:18+01:00
Add -Wrule-lhs-equalities warning
This commit adds a new warning, controlled by the warning flag,
-Wrule-lhs-equalities, which 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.
- - - - -
13 changed files:
- compiler/GHC/Core/Rules.hs
- compiler/GHC/Driver/Flags.hs
- compiler/GHC/Driver/Session.hs
- compiler/GHC/HsToCore/Binds.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/Core/Rules.hs
=====================================
@@ -1001,17 +1001,17 @@ In short, it is Very Deeply Suspicious for a rule to quantify over a coercion
variable. And SpecConstr no longer does so: see Note [SpecConstr and casts] in
SpecConstr.
-It is, however, OK for a cast to appear in a template. For example
- newtype N a = MkN (a,a) -- Axiom ax:N a :: (a,a) ~R N a
- f :: N a -> bah
- RULE forall b x:b y:b. f @b ((x,y) |> (axN @b)) = ...
-
-When matching we can just move these casts to the other side:
- match (tmpl |> co) tgt --> match tmpl (tgt |> sym co)
-See matchTemplateCast.
-
Wrinkles:
+(CT0) It is, however, OK for a cast to appear in a template provided the cast mentions
+ none of the template variables. For example
+ newtype N a = MkN (a,a) -- Axiom ax:N a :: (a,a) ~R N a
+ f :: N a -> bah
+ RULE forall b x:b y:b. f @b ((x,y) |> (axN @b)) = ...
+ When matching we can just move these casts to the other side:
+ match (tmpl |> co) tgt --> match tmpl (tgt |> sym co)
+ See matchTemplateCast.
+
(CT1) We need to be careful about scoping, and to match left-to-right, so that we
know the substitution [a :-> b] before we meet (co :: (a,a) ~R N a), and so we
can apply that substitition
@@ -1496,11 +1496,12 @@ matchTemplateCast renv subst e1 co1 e2 mco
filterFV (`elemVarSet` rv_tmpls renv) $ -- Check that the coercion does not
tyCoFVsOfCo substed_co -- mention any of the template variables
= -- This is the good path
- -- See Note [Casts in the template]
+ -- See Note [Casts in the template] wrinkle (CT0)
match renv subst e1 e2 (checkReflexiveMCo (mkTransMCoL mco (mkSymCo substed_co)))
| otherwise
= -- This is the Deeply Suspicious Path
+ -- See Note [Casts in the template]
do { let co2 = case mco of
MRefl -> mkRepReflCo (exprType e2)
MCo co2 -> co2
=====================================
compiler/GHC/Driver/Flags.hs
=====================================
@@ -1080,6 +1080,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
@@ -1198,6 +1199,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
@@ -1341,7 +1343,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
=====================================
@@ -2360,6 +2360,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/HsToCore/Binds.hs
=====================================
@@ -996,7 +996,13 @@ prepareSpecLHS poly_id evs the_call
= go qevs (bind:acc) e
| otherwise
- = go (qevs `extendVarSetList` bndrs) acc e
+ = pprPanic "prepareSpecLHS" $
+ vcat [ text "poly_id:" <+> ppr poly_id
+ , text "the_call:" <+> ppr the_call
+ , text "bind:" <+> ppr bind
+ , text "bndrs:" <+> ppr bndrs
+ ]
+ --go (qevs `extendVarSetList` bndrs) acc e
where
bndrs = bindersOf bind
=====================================
compiler/GHC/Tc/Errors/Ppr.hs
=====================================
@@ -1426,6 +1426,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{}
@@ -3097,6 +3107,8 @@ instance Diagnostic TcRnMessage where
-> [suggestExtension LangExt.StandaloneKindSignatures]
TcRnIllegalRuleLhs{}
-> noHints
+ TcRnRuleLhsEqualities{}
+ -> noHints
TcRnDuplicateRoleAnnot{}
-> noHints
TcRnDuplicateKindSig{}
=====================================
compiler/GHC/Tc/Errors/Types.hs
=====================================
@@ -3302,9 +3302,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
=====================================
@@ -61,6 +61,7 @@ import GHC.Core.Type
import GHC.Core.Multiplicity
import GHC.Core.Predicate
import GHC.Core.TyCo.Rep( mkNakedFunTy )
+import GHC.Core.TyCon( isTypeFamilyTyCon )
import GHC.Types.Var
import GHC.Types.Var.Set
@@ -81,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 )
{- -------------------------------------------------------------
Note [Overview of type signatures]
@@ -1278,23 +1280,35 @@ tcRule (HsRule { rd_ext = ext
vcat [ ppr id <+> dcolon <+> ppr (idType id) | id <- tpl_ids ]
])
- -- SimplfyRule Plan, step 5
+ -- /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)
+ -> do { addDiagnostic $ TcRnRuleLhsEqualities name lhs cts
+ ; return Nothing } ;
+ _ ->
+
+ 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
-- (b) so that we bind any soluble ones
- ; (lhs_implic, lhs_binds) <- buildImplicationFor tc_lvl (getSkolemInfo skol_info) qtkvs
+ (lhs_implic, lhs_binds) <- buildImplicationFor tc_lvl (getSkolemInfo skol_info) qtkvs
lhs_evs residual_lhs_wanted
; (rhs_implic, rhs_binds) <- buildImplicationFor tc_lvl (getSkolemInfo skol_info) qtkvs
lhs_evs rhs_wanted
+
; emitImplications (lhs_implic `unionBags` rhs_implic)
- ; return $ Just $ HsRule { rd_ext = ext
- , rd_name = rname
- , rd_act = act
- , rd_bndrs = bndrs { rb_ext = qtkvs ++ tpl_ids }
- , rd_lhs = mkHsDictLet lhs_binds lhs'
- , rd_rhs = mkHsDictLet rhs_binds rhs' } }
+ ; return $ Just $
+ HsRule { rd_ext = ext
+ , rd_name = rname
+ , rd_act = act
+ , rd_bndrs = bndrs { rb_ext = qtkvs ++ tpl_ids }
+ , rd_lhs = mkHsDictLet lhs_binds lhs'
+ , rd_rhs = mkHsDictLet rhs_binds rhs' } } } }
{- ********************************************************************************
* *
@@ -1453,7 +1467,6 @@ RHS constraints. Actually much of this is done by the on-the-fly
constraint solving, so the same order must be observed in
tcRule.
-
Note [RULE quantification over equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
At the moment a RULE never quantifies over an equality; see `rule_quant_ct`
@@ -1467,6 +1480,14 @@ in `getRuleQuantCts`. Why not?
(b) because if such things end up in 'givens' we get a bogus
"inaccessible code" error
+ * Matching on coercions is Deeply Suspicious. We don't want to generate a
+ RULE like
+ forall a (co :: F a ~ Int).
+ foo (x |> Sym co) = ...co...
+ because matching on that template, to bind `co`, would require us to
+ match on the /structure/ of a coercion, which we must never do.
+ See GHC.Core.Rules Note [Casts in the template]
+
* Equality constraints are unboxed, and that leads to complications
For example equality constraints from the LHS will emit coercion hole
Wanteds. These don't have a name, so we can't quantify over them directly.
@@ -1595,3 +1616,91 @@ getRuleQuantCts wc
= case classifyPredType (ctPred ct) of
EqPred {} -> False -- Note [RULE quantification over equalities]
_ -> tyCoVarsOfCt ct `disjointVarSet` skol_tvs
+
+{- 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 <- 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
+ | otherwise
+ = Nothing
+
+ go_implic :: TyVarSet -> Implication -> Maybe [Ct]
+ go_implic skol_tvs (Implic { ic_skols = skols, ic_wanted = wc })
+ = fmap toList $ go (skol_tvs `extendVarSetList` skols) wc
+
+ ok_eq t1 t2
+ | t1 `tcEqType` t2 = False
+ | otherwise = is_fun_app t1 || is_fun_app t2
+
+ is_fun_app ty -- ty is of form (F tys) where F is a type function
+ = case tyConAppTyCon_maybe ty of
+ Just tc -> isTypeFamilyTyCon tc
+ Nothing -> False
=====================================
compiler/GHC/Types/Error/Codes.hs
=====================================
@@ -610,6 +610,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
=====================================
@@ -739,6 +739,7 @@ test('ExplicitSpecificityA1', normal, compile, [''])
test('ExplicitSpecificityA2', normal, compile, [''])
test('ExplicitSpecificity4', normal, compile, [''])
test('TcSpecPragmas', 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/10f59a447c4061804cb5e8f52f3c640b93e68cf4
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/10f59a447c4061804cb5e8f52f3c640b93e68cf4
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/20250312/e0ab602e/attachment-0001.html>
More information about the ghc-commits
mailing list