When we add a new /given/ implicit parameter to the inert set, it /replaces/
any existing givens for the same implicit parameter. This makes a difference
in two places:
* In `GHC.Tc.Solver.InertSet.solveOneFromTheOther`, be careful when we have
(?x :: ty) in the inert set and an identical (?x :: ty) as the work item.
* In `updInertDicts`, in this module, when adding [G] (?x :: ty), remove any
existing [G] (?x :: ty'), regardless of ty'.
* Wrinkle (SIP1): we must be careful of superclasses. Consider
f,g :: (?x::Int, C a) => a -> a
f v = let ?x = 4 in g v
The call to 'g' gives rise to a Wanted constraint (?x::Int, C a).
We must /not/ solve this from the Given (?x::Int, C a), because of
the intervening binding for (?x::Int). #14218.
We deal with this by arranging that when we add [G] (?x::ty) we delete
* from the inert_cans, and
* from the inert_solved_dicts
any existing [G] (?x::ty) /and/ any [G] D tys, where (D tys) has a superclass
with (?x::ty). See Note [Local implicit parameters] in GHC.Core.Predicate.
An important special case is constraint tuples like [G] (% ?x::ty, Eq a %).
But it could happen for `class xx => D xx where ...` and the constraint D
(?x :: int). This corner (constraint-kinded variables instantiated with
implicit parameter constraints) is not well explored.
Example in #14218, and #23761
The code that accounts for (SIP1) is in updInertDicts; in particular the call to
GHC.Core.Predicate.mentionsIP.
* Wrinkle (SIP2): we must apply this update semantics for `inert_solved_dicts`
as well as `inert_cans`.
You might think that wouldn't be necessary, because an element of
`inert_solved_dicts` is never an implicit parameter (see
Note [Solved dictionaries] in GHC.Tc.Solver.InertSet).
While that is true, dictionaries in `inert_solved_dicts` may still have
implicit parameters as a /superclass/! For example:
class c => C c where ...
f :: C (?x::Int) => blah
Now (C (?x::Int)) has a superclass (?x::Int). This may look exotic, but it
happens particularly for constraint tuples, like `(% ?x::Int, Eq a %)`.
Example 1:
Suppose we have (typecheck/should_compile/ImplicitParamFDs)
flub :: (?x :: Int) => (Int, Integer)
flub = (?x, let ?x = 5 in ?x)
When we are checking the last ?x occurrence, we guess its type to be a fresh
unification variable alpha and emit an (IP "x" alpha) constraint. But the given
(?x :: Int) has been translated to an IP "x" Int constraint, which has a
functional dependency from the name to the type. So if that (?x::Int) is still
in the inert set, we'd get a fundep interaction that tells us that alpha ~ Int,
and we get a type error. This is bad. The "replacement" semantics stops this
happening.
Example 2:
f :: (?x :: Char) => Char
f = let ?x = 'a' in ?x
The "let ?x = ..." generates an implication constraint of the form:
?x :: Char => ?x :: Char
Furthermore, the signature for `f` also generates an implication
constraint, so we end up with the following nested implication:
?x :: Char => (?x :: Char => ?x :: Char)
Note that the wanted (?x :: Char) constraint may be solved in two incompatible
ways: either by using the parameter from the signature, or by using the local
definition. Our intention is that the local definition should "shadow" the
parameter of the signature. The "replacement" semantics for implicit parameters
does this.
Example 3:
Similarly, consider
f :: (?x::a) => Bool -> a
g v = let ?x::Int = 3
in (f v, let ?x::Bool = True in f v)
This should probably be well typed, with
g :: Bool -> (Int, Bool)
So the inner binding for ?x::Bool *overrides* the outer one.
See ticket #17104 for a rather tricky example of this overriding
behaviour.
All this works for the normal cases but it has an odd side effect in
some pathological programs like this:
This is accepted, the second parameter shadows
f1 :: (?x :: Int, ?x :: Char) => Char
f1 = ?x
This is rejected, the second parameter shadows
f2 :: (?x :: Int, ?x :: Char) => Int
f2 = ?x
Both of these are actually wrong: when we try to use either one,
we'll get two incompatible wanted constraints (?x :: Int, ?x :: Char),
which would lead to an error.
I can think of two ways to fix this:
1. Simply disallow multiple constraints for the same implicit
parameter---this is never useful, and it can be detected completely
syntactically.
2. Move the shadowing machinery to the location where we nest
implications, and add some code here that will produce an
error if we get multiple givens for the same implicit parameter.