We must determine whether a Given might later equal a Wanted:
see Note [Instance and Given overlap] in GHC.Tc.Solver.Dict
We definitely need to account for the possibility that any metavariable might be
arbitrarily instantiated. Yet we do *not* want to allow skolems to be
instantiated, as we've already rewritten with respect to any Givens. (We're
solving a Wanted here, and so all Givens have already been processed.)
This is best understood by example.
1. C alpha[tau] ~? C Int
That Given certainly might match later.
2. C a[sk] ~? C Int
No. No new givens are going to arise that will get the `a` to rewrite
to Int. Example:
f :: forall a. C a => blah
f = rhs -- Gives rise to [W] C Int
It would be silly to fail to solve ([W] C Int), just because we have
([G] C a) in the Givens!
3. C alpha[tv] ~? C Int
In this variant of (1) that alpha[tv] is a TyVarTv, unifiable only with
other type /variables/. It cannot equal Int later.
4. C (F alpha[tau]) ~? C Int
Sure -- that can equal later, if we learn something useful about alpha.
5. C (F alpha[tv]) ~? C Int
This, too, might equal later. Perhaps we have [G] F b ~ Int elsewhere.
Or maybe we have C (F alpha[tv] beta[tv]), these unify with each other,
and F x x = Int. Remember: returning True doesn't commit ourselves to
anything.
6. C (F a[sk]) ~? C Int. For example
f :: forall a. C (F a) => blah
f = rhs -- Gives rise to [W] C Int
No, this won't match later. If we could rewrite (F a), we would
have by now. But see also Red Herring below.
This arises in instance decls too. For example in GHC.Core.Ppr we see
instance Outputable (XTickishId pass)
=> Outputable (GenTickish pass) where
If we have [W] Outputable Int in the body, we don't want to fail to solve
it because (XTickishId pass) might simplify to Int.
7. C (Maybe alpha[tau]) ~? C alpha[tau]
We say this cannot equal later, because it would require
alpha := Maybe (Maybe (Maybe ...)). While such a type can be contrived,
we choose not to worry about it. See Note [Infinitary substitution in lookup]
in GHC.Core.InstEnv. Getting this wrong led to #19107, tested in
typecheck/should_compile/T19107.
8. C alpha[cbv] ~? C Int
where alpha[cbv] = F a
The alpha[cbv] is a cycle-breaker var which stands for F a. See
Note [Type equality cycles] in GHC.Tc.Solver.Equality
This is just like case 6, and we say "no". Saying "no" here is
essential in getting the parser to type-check, with its use of DisambECP.
9. C alpha[cbv] ~? C Int
where alpha[cbv] = F beta[tau]
Here, we might indeed equal later. Distinguishing between
this case and Example 8 is why we need the InertSet in mightEqualLater.
10. C (F alpha[tau], Int) ~? C (Bool, F alpha[tau])
This cannot equal later, because F alpha would have to equal both Bool and
Int.
To deal with type family applications, we use the "fine-grained" Core unifier.
See Note [Apartness and type families] in GHC.Core.Unify, controlled
by the `bind_fam :: BindFamFun` function defined in `mightEqualLater`.
One tricky point: a type family application that mentions only skolems (example
6) is settled: any skolems would have been rewritten w.r.t. Givens by now. These
type family applications match only themselves. However: a type family
application that mentions metavariables, on the other hand, can match
anything. So, if the original type family application contains a metavariable,
we use BindMe to tell the unifier to allow it in the substitution. On the other
hand, a type family application with only skolems is considered rigid. See the
use of `mentions_meta_ty_var` in `mightEqualLater`.
This treatment fixes #18910 and is tested in
typecheck/should_compile/InstanceGivenOverlap{,2}
Red Herring
~~~~~~~~~~~
In #21208, we have this scenario:
instance forall b. C b
[G] C a[sk]
[W] C (F a[sk])
What should we do with that wanted? According to the logic above, the Given
cannot match later (this is example 6), and so we use the global instance.
But wait, you say: What if we learn later (say by a future type instance F a = a)
that F a unifies with a? That looks like the Given might really match later!
This mechanism described in this Note is *not* about this kind of situation, however.
It is all asking whether a Given might match the Wanted *in this run of the solver*.
It is *not* about whether a variable might be instantiated so that the Given matches,
or whether a type instance introduced in a downstream module might make the Given match.
The reason we care about what might match later is only about avoiding order-dependence.
That is, we don't want to commit to a course of action that depends on seeing constraints
in a certain order. But an instantiation of a variable and a later type instance
don't introduce order dependency in this way, and so mightMatchLater is right to ignore
these possibilities.
Here is an example, with no type families, that is perhaps clearer:
instance forall b. C (Maybe b)
[G] C (Maybe Int)
[W] C (Maybe a)
What to do? We *might* say that the Given could match later and should thus block
us from using the global instance. But we don't do this. Instead, we rely on class
coherence to say that choosing the global instance is just fine, even if later we
call a function with (a := Int). After all, in this run of the solver, [G] C (Maybe Int)
will definitely never match [W] C (Maybe a). (Recall that we process Givens before
Wanteds, so there is no [G] a ~ Int hanging about unseen.)
Interestingly, in the first case (from #21208), the behavior changed between
GHC 8.10.7 and GHC 9.2, with the latter behaving correctly and the former
reporting overlapping instances.
Test case: typecheck/should_compile/T21208.