With Opt_WarnRedundantConstraints, GHC can report which constraints of a type
signature (or instance declaration) are redundant, and can be omitted. Here is
an overview of how it works.
This is all tested in typecheck/should_compile/T20602 (among others).
How tracking works:
* We maintain the `ic_need` field in an implication:
ic_need: the set of Given evidence variables that are needed somewhere
inside this implication; and are bound either by this implication
or by an enclosing one.
* `setImplicationStatus` does all the work:
- When the constraint solver finishes solving all the wanteds in
an implication, it sets its status to IC_Solved
- `neededEvVars`: computes which evidence variables are needed by an
implication in `setImplicationStatus`. A variable is needed if
a) It is in the ic_need field of this implication, computed in
a previous call to `setImplicationStatus`; see (TRC1)
b) It is in the ics_need of a nested implication; see `add_implic`
in `neededEvVars`
c) It is free in the RHS of any /Wanted/ EvBind; each such binding
solves a Wanted, so we want them all. See `add_wanted` in
`neededEvVars`
d) It is free in the RHS of a /Given/ EvBind whose LHS is needed:
see `findNeededGivenEvVars` called from `neededEvVars`.
- Next, if the final status is IC_Solved, `setImplicationStatus` uses
`findRedundantGivens` to decide which of this implication's Givens
are redundant.
- It also uses `pruneImplications` to discard any now-unnecessary child
implications.
* GHC.Tc.Errors does the actual warning, in `warnRedundantConstraints`.
Wrinkles:
(TRC1) `pruneImplications` drops any sub-implications of an Implication
that are irrelevant for error reporting:
- no unsolved wanteds
- no sub-implications
- no redundant givens to report
But in doing so we must not lose track of the variables that those implications
needed! So we track the ic_needs of all child implications in `ic_need_implics`.
Crucially, this set includes things need by child implications that have been
discarded by `pruneImplications`.
(TRC2) A Given can be redundant because it is implied by other Givens
f :: (Eq a, Ord a) => blah -- Eq a unnecessary
g :: (Eq a, a~b, Eq b) => blah -- Either Eq a or Eq b unnecessary
We nail this by using `mkMinimalBySCs` in `findRedundantGivens`.
(TRC2a) But NOTE that we only attempt this mkMinimalBySCs stuff if all Givens
used by evidence bindings. Example:
f :: (Eq a, Ord a) => a -> Bool
f x = x == x
We report (Ord a) as unused because it is. But we must not also report (Eq a)
as unused because it is a superclass of Ord!
(TRC3) When two Givens are the same, prefer one that does not involve superclass
selection, or more generally has shallower superclass-selection depth:
see 2(b,c) in Note [Replacement vs keeping] in GHC.Tc.Solver.InertSet.
e.g f :: (Eq a, Ord a) => a -> Bool
f x = x == x
Eager superclass expansion gives us two [G] Eq a constraints. We want to keep
the one from the user-written Eq a, not the superclass selection. This means
we report the Ord a as redundant with -Wredundant-constraints, not the Eq a.
Getting this wrong was #20602.
(TRC4) We don't compute redundant givens for *every* implication; only
for those which reply True to `warnRedundantGivens`:
- For example, in a class declaration, the default method *can*
use the class constraint, but it certainly doesn't *have* to,
and we don't want to report an error there. Ditto instance decls.
- More subtly, in a function definition
f :: (Ord a, Ord a, Ix a) => a -> a
f x = rhs
we do an ambiguity check on the type (which would find that one
of the Ord a constraints was redundant), and then we check that
the definition has that type (which might find that both are
redundant). We don't want to report the same error twice, so we
disable it for the ambiguity check. Hence using two different
FunSigCtxts, one with the warn-redundant field set True, and the
other set False in
- GHC.Tc.Gen.Bind.tcSpecPrag
- GHC.Tc.Gen.Bind.tcTySig
- 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!
(TRC5) Consider this (#25992), where `op2` has a default method
class C a where { op1, op2 :: a -> a
; op2 = op1 . op1 }
instance C a => C [a] where
op1 x = x
Plainly the (C a) constraint is unused; but the expanded decl will look like
$dmop2 :: C a => a -> a
$dmop2 = op1 . op1
$fCList :: forall a. C a => C [a]
$fCList @a (d::C a) = MkC (\(x:a).x) ($dmop2 @a d)
Notice that `d` gets passed to `$dmop`: it is "needed". But it's only
/really/ needed if some /other/ method (in this case `op1`) uses it.
So, rather than one set of "needed Givens" we use `EvNeedSet` to track
a /pair/ of sets:
ens_dms: needed /only/ by default-method calls
ens_fvs: needed by something other than a default-method call
It's a bit of a palaver, but not really difficult.
All the logic is localised in `neededEvVars`.
But NOTE that this only applies to /vanilla/ default methods.
For /generic/ default methods, like
class D a where { op1 :: blah
; default op1 :: Eq a => blah2 }
the (Eq a) constraint really is needed (e.g. class NFData and #25992).
Hence the `Bool` field of `MethSkol` indicates a /vanilla/ default method.
Examples
f, g, h :: (Eq a, Ord a) => a -> Bool
f x = x == x
g x = x > x
h x = x == x && x > x
All of f,g,h will discover that they have two [G] Eq a constraints: one as
given and one extracted from the Ord a constraint. They will both discard
the latter; see (TRC3).
The body of f uses the [G] Eq a, but not the [G] Ord a. It will report a
redundant Ord a.
The body of g uses the [G] Ord a, but not the [G] Eq a. It will report a
redundant Eq a.
The body of h uses both [G] Ord a and [G] Eq a; each is used in a solved
Wanted evidence binding. But (TRC2) kicks in and discovers the Eq a
is redundant.
Shortcomings
Shortcoming 1. Consider
j :: (Eq a, a ~ b) => a -> Bool
j x = x == x
k :: (Eq a, b ~ a) => a -> Bool
k x = x == x
Currently (Nov 2021), j issues no warning, while k says that b ~ a
is redundant. This is because j uses the a ~ b constraint to rewrite
everything to be in terms of b, while k does none of that. This is
ridiculous, but I (Richard E) don't see a good fix.
Shortcoming 2. Removing a redundant constraint can cause clients to fail to
compile, by making the function more polymorphic. Consider (#16154)
f :: (a ~ Bool) => a -> Int
f x = 3
g :: String -> Int
g s = f (read s)
The constraint in f's signature is redundant; not used to typecheck
`f`. And yet if you remove it, `g` won't compile, because there'll
be an ambiguous variable in `g`.
**********************************************************************
* *
* Main Solver *
* *
**********************************************************************