1 files changed, 129 insertions, 0 deletions
diff --git a/compiler/GHC/Tc/Solver/InertSet.hs b/compiler/GHC/Tc/Solver/InertSet.hs
index b2416e9915..cc2afc1b0e 100644
--- a/compiler/GHC/Tc/Solver/InertSet.hs
+++ b/compiler/GHC/Tc/Solver/InertSet.hs
@@ -1643,6 +1643,135 @@ prohibitedSuperClassSolve from_loc solve_loc
   | otherwise
   = False
 
+{- Note [What might equal later?]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We must determine whether a Given might later equal a Wanted. We
+definitely need to account for the possibility that any metavariable
+might be arbitrarily instantiated. Yet we do *not* want
+to allow skolems in 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  ~?  C Int
+
+   That given certainly might match later.
+
+2. C a  ~?  C Int
+
+   No. No new givens are going to arise that will get the `a` to rewrite
+   to Int.
+
+3. C alpha[tv]   ~?  C Int
+
+   That alpha[tv] is a TyVarTv, unifiable only with other type variables.
+   It cannot equal later.
+
+4. C (F alpha)   ~?   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)  ~?  C a
+
+   No, this won't match later. If we could rewrite (F a) or a, we would
+   have by now. But see also Red Herring below.
+
+7. C (Maybe alpha)  ~?  C alpha
+
+   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 let to #19107, tested in
+   typecheck/should_compile/T19107.
+
+8. C cbv   ~?  C Int
+   where cbv = F a
+
+   The cbv is a cycle-breaker var which stands for F a. See
+   Note [Type variable cycles] in GHC.Tc.Solver.Canonical.
+   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 cbv   ~?   C Int
+   where cbv = F alpha
+
+   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, Int)  ~?  C (Bool, F alpha)
+
+   This cannot equal later, because F a would have to equal both Bool and
+   Int.
+
+To deal with type family applications, we use the Core flattener. See
+Note [Flattening type-family applications when matching instances] in GHC.Core.Unify.
+The Core flattener replaces all type family applications with
+fresh variables. The next question: should we allow these fresh
+variables in the domain of a unifying substitution?
+
+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. 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.
+
+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.
+
+-}
+
 {- *********************************************************************
 *                                                                      *
     Cycle breakers