[Git][ghc/ghc][master] Don't report redundant Givens from quantified constraints
Marge Bot (@marge-bot)
gitlab at gitlab.haskell.org
Thu Jun 8 22:41:08 UTC 2023
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
2b0c9f5e by Simon Peyton Jones at 2023-06-08T07:52:34+00:00
Don't report redundant Givens from quantified constraints
This fixes #23323
See (RC4) in Note [Tracking redundant constraints]
- - - - -
6 changed files:
- compiler/GHC/Tc/Errors.hs
- compiler/GHC/Tc/Solver.hs
- compiler/GHC/Tc/Solver/Solve.hs
- compiler/GHC/Tc/Types/Constraint.hs
- + testsuite/tests/quantified-constraints/T23323.hs
- testsuite/tests/quantified-constraints/all.T
Changes:
=====================================
compiler/GHC/Tc/Errors.hs
=====================================
@@ -352,8 +352,9 @@ reportImplic ctxt implic@(Implic { ic_skols = tvs
-- Do /not/ use the tidied tvs because then are in the
-- wrong order, so tidying will rename things wrongly
; reportWanteds ctxt' tc_lvl wanted
- ; when (cec_warn_redundant ctxt) $
- warnRedundantConstraints ctxt' ct_loc_env info' dead_givens }
+
+ -- Report redundant (unused) constraints
+ ; warnRedundantConstraints ctxt' ct_loc_env info' dead_givens }
where
insoluble = isInsolubleStatus status
(env1, tvs') = tidyVarBndrs (cec_tidy ctxt) $
@@ -390,9 +391,19 @@ reportImplic ctxt implic@(Implic { ic_skols = tvs
warnRedundantConstraints :: SolverReportErrCtxt -> CtLocEnv -> SkolemInfoAnon -> [EvVar] -> TcM ()
-- See Note [Tracking redundant constraints] in GHC.Tc.Solver
warnRedundantConstraints ctxt env info redundant_evs
+ | not (cec_warn_redundant ctxt)
+ = return ()
+
| null redundant_evs
= return ()
+ -- Do not report redundant constraints for quantified constraints
+ -- See (RC4) in Note [Tracking redundant constraints]
+ -- Fortunately it is easy to spot implications constraints that arise
+ -- from quantified constraints, from their SkolInfo
+ | InstSkol (IsQC {}) _ <- info
+ = return ()
+
| SigSkol user_ctxt _ _ <- info
-- When dealing with a user-written type signature,
-- we want to add "In the type signature for f".
@@ -404,7 +415,7 @@ warnRedundantConstraints ctxt env info redundant_evs
-- "In the instance declaration for Eq [a]" context
-- and we don't want to say it twice. Seems a bit ad-hoc
= report_redundant_msg False env
- -- ^^^^^ don't add "In the type signature..."
+ -- ^^^^^ don't add "In the type signature..."
where
report_redundant_msg :: Bool -- whether to add "In the type signature..." to the diagnostic
-> CtLocEnv
=====================================
compiler/GHC/Tc/Solver.hs
=====================================
@@ -3228,39 +3228,54 @@ others).
----- How tracking works
-* When two Givens are the same, we drop the evidence for the one
+(RC1) When two Givens are the same, we drop the evidence for the one
that requires more superclass selectors. This is done
- according to Note [Replacement vs keeping] in GHC.Tc.Solver.InertSet.
+ according to 2(c) of Note [Replacement vs keeping] in GHC.Tc.Solver.InertSet.
-* The ic_need fields of an Implic records in-scope (given) evidence
+(RC2) The ic_need fields of an Implic records in-scope (given) evidence
variables bound by the context, that were needed to solve this
implication (so far). See the declaration of Implication.
-* When the constraint solver finishes solving all the wanteds in
+(RC3) setImplicationStatus:
+ When the constraint solver finishes solving all the wanteds in
an implication, it sets its status to IC_Solved
- The ics_dead field, of IC_Solved, records the subset of this
implication's ic_given that are redundant (not needed).
-* We compute which evidence variables are needed by an implication
- in setImplicationStatus. A variable is needed if
+ - We compute which evidence variables are needed by an implication
+ in setImplicationStatus. A variable is needed if
a) it is free in the RHS of a Wanted EvBind,
b) it is free in the RHS of an EvBind whose LHS is needed, or
c) it is in the ics_need of a nested implication.
-* After computing which variables are needed, we then look at the
- remaining variables for internal redundancies. This is case (b)
- from above. This is also done in setImplicationStatus.
- Note that we only look for case (b) if case (a) shows up empty,
- as exemplified below.
-
-* We need to be careful not to discard an implication
- prematurely, even one that is fully solved, because we might
- thereby forget which variables it needs, and hence wrongly
- report a constraint as redundant. But we can discard it once
- its free vars have been incorporated into its parent; or if it
- simply has no free vars. This careful discarding is also
- handled in setImplicationStatus.
+ - After computing which variables are needed, we then look at the
+ remaining variables for internal redundancies. This is case (b)
+ from above. This is also done in setImplicationStatus.
+ Note that we only look for case (b) if case (a) shows up empty,
+ as exemplified below.
+
+ - We need to be careful not to discard an implication
+ prematurely, even one that is fully solved, because we might
+ thereby forget which variables it needs, and hence wrongly
+ report a constraint as redundant. But we can discard it once
+ its free vars have been incorporated into its parent; or if it
+ simply has no free vars. This careful discarding is also
+ handled in setImplicationStatus.
+
+(RC4) We do not want to report redundant constraints for implications
+ that come from quantified constraints. Example #23323:
+ data T a
+ instance Show (T a) where ... -- No context!
+ foo :: forall f c. (forall a. c a => Show (f a)) => Proxy c -> f Int -> Int
+ bar = foo @T @Eq
+
+ The call to `foo` gives us
+ [W] d : (forall a. Eq a => Show (T a))
+ To solve this, GHC.Tc.Solver.Solve.solveForAll makes an implication constraint:
+ forall a. Eq a => [W] ds : Show (T a)
+ and because of the degnerate instance for `Show (T a)`, we don't need the `Eq a`
+ constraint. But we don't want to report it as redundant!
* Examples:
=====================================
compiler/GHC/Tc/Solver/Solve.hs
=====================================
@@ -425,8 +425,7 @@ solveForAll ev@(CtWanted { ctev_dest = dest, ctev_rewriters = rewriters, ctev_lo
; return ( ctEvEvId wanted_ev
, unitBag (mkNonCanonical wanted_ev)) }
- ; ev_binds <- emitImplicationTcS lvl (getSkolemInfo skol_info) skol_tvs
- given_ev_vars wanteds
+ ; ev_binds <- emitImplicationTcS lvl skol_info_anon skol_tvs given_ev_vars wanteds
; setWantedEvTerm dest IsCoherent $
EvFun { et_tvs = skol_tvs, et_given = given_ev_vars
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -1479,6 +1479,7 @@ data Implication
-- NB: including stuff used by nested implications that have since
-- been discarded
-- See Note [Needed evidence variables]
+ -- and (RC2) in Note [Tracking redundant constraints]a
ic_need_inner :: VarSet, -- Includes all used Given evidence
ic_need_outer :: VarSet, -- Includes only the free Given evidence
-- i.e. ic_need_inner after deleting
=====================================
testsuite/tests/quantified-constraints/T23323.hs
=====================================
@@ -0,0 +1,17 @@
+{-# OPTIONS_GHC -Werror -Wredundant-constraints #-}
+{-# LANGUAGE QuantifiedConstraints, TypeApplications, UndecidableInstances #-}
+
+module Lib where
+
+import Data.Kind
+import Data.Proxy
+
+data T a
+instance Show (T a) where { show x = "no" }
+
+foo :: forall f c. (forall a. c a => Show (f a)) => Proxy c -> f Int -> Int
+foo = foo
+
+bar = foo @T @Eq
+-- We dont' want to report a redundance (Eq a) constraint
+
=====================================
testsuite/tests/quantified-constraints/all.T
=====================================
@@ -42,3 +42,4 @@ test('T22216e', normal, compile, [''])
test('T22223', normal, compile, [''])
test('T19690', normal, compile_fail, [''])
test('T23333', normal, compile, [''])
+test('T23323', normal, compile, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2b0c9f5ef026df6dd2637aacce05a11d74146296
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2b0c9f5ef026df6dd2637aacce05a11d74146296
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/20230608/19e93f8d/attachment-0001.html>
More information about the ghc-commits
mailing list