Note [Instance and Given overlap]
Example, from the OutsideIn(X) paper:
instance P x => Q [x]
instance (x ~ y) => R y [x]
wob :: forall a b. (Q [b], R b a) => a -> Int
g :: forall a. Q [a] => [a] -> Int
g x = wob x
From 'g' we get the implication constraint:
forall a. Q [a] => (Q [beta], R beta [a])
If we react (Q [beta]) with its top-level axiom, we end up with a
(P beta), which we have no way of discharging. On the other hand,
if we react R beta [a] with the top-level we get (beta ~ a), which
is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
now solvable by the given Q [a].
The partial solution is that:
In matchClassInst (and thus in topReact), we return a matching
instance only when there is no Given in the inerts which is
unifiable to this particular dictionary.
We treat any meta-tyvar as "unifiable" for this purpose,
*including* untouchable ones. But not skolems like 'a' in
the implication constraint above.
The end effect is that, much as we do for overlapping instances, we
delay choosing a class instance if there is a possibility of another
instance OR a given to match our constraint later on. This fixes
tickets #4981 and #5002.
Other notes:
* The check is done *first*, so that it also covers classes
with built-in instance solving, such as
- constraint tuples
- natural numbers
- Typeable
* See also Note [What might equal later?] in GHC.Tc.Utils.Unify
* The given-overlap problem is arguably not easy to appear in practice
due to our aggressive prioritization of equality solving over other
constraints, but it is possible. I've added a test case in
typecheck/should-compile/GivenOverlapping.hs
* Another "live" example is #10195; another is #10177.
* We ignore the overlap problem if -XIncoherentInstances is in force:
see #6002 for a worked-out example where this makes a
difference.
* Moreover notice that our goals here are different than the goals of
the top-level overlapping checks. There we are interested in
validating the following principle:
If we inline a function f at a site where the same global
instance environment is available as the instance environment at
the definition site of f then we should get the same behaviour.
But for the Given Overlap check our goal is just related to completeness of
constraint solving.
* The solution is only a partial one. Consider the above example with
g :: forall a. Q [a] => [a] -> Int
g x = let v = wob x
in v
and suppose we have -XNoMonoLocalBinds, so that we attempt to find the most
general type for 'v'. When generalising v's type we'll simplify its
Q [alpha] constraint, but we don't have Q [a] in the 'givens', so we
will use the instance declaration after all. #11948 was a case
in point.
All of this is disgustingly delicate, so to discourage people from writing
simplifiable class givens, we warn about signatures that contain them;
see GHC.Tc.Validity Note [Simplifiable given constraints]. References 2
- What might equal later? GHC.Tc.Utils.Unify
- Simplifiable given constraints GHC.Tc.Validity
Referenced by 10
- Solving equality classes GHC.Tc.Solver.Dict ×2
- GHC.Tc.Solver.Dict call site ×2
- Rules for instance lookup GHC.Core.InstEnv
- Eagerly expand given superclasses GHC.Tc.Solver.Dict
- Decomposing newtype equalities GHC.Tc.Solver.Equality
- What might equal later? GHC.Tc.Utils.Unify
- GHC.Tc.Utils.Unify call site
- Simplifiable given constraints GHC.Tc.Validity