[Git][ghc/ghc][wip/T24359] Warn about rules that previously quantified over equalities
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Tue Dec 24 11:32:12 UTC 2024
Simon Peyton Jones pushed to branch wip/T24359 at Glasgow Haskell Compiler / GHC
Commits:
01f996f4 by Simon Peyton Jones at 2024-12-24T11:31:36+00:00
Warn about rules that previously quantified over equalities
- - - - -
2 changed files:
- compiler/GHC/Core/Rules.hs
- compiler/GHC/Tc/Gen/Sig.hs
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/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
@@ -1194,23 +1195,36 @@ 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 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!
+ ; case allPreviouslyQuantifiableEqualities residual_lhs_wanted of {
+ Just cts | not (insolubleWC rhs_wanted)
+ -> pprTrace "tcRule: discarding" (ppr cts) $
+ return Nothing ;
+ Nothing ->
+
+ do { -- SimplfyRule 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' } } } }
@@ -1376,7 +1390,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`
@@ -1390,6 +1403,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.
@@ -1531,3 +1552,31 @@ getRuleQuantCts wc
| otherwise
= pprPanic "getRuleQuantCts" (ppr ct)
+
+allPreviouslyQuantifiableEqualities :: WantedConstraints -> Maybe [Ct]
+allPreviouslyQuantifiableEqualities wc = go emptyVarSet wc
+ where
+ 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) }
+
+ 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 skol_tvs (Implic { ic_skols = skols, ic_wanted = wc })
+ = 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
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/01f996f4217e6048bd9614c9380389a0ef2e630d
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/01f996f4217e6048bd9614c9380389a0ef2e630d
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/20241224/0c62a17c/attachment-0001.html>
More information about the ghc-commits
mailing list