Add Red Herring to Note [What might equal later?]

Close #21208.

5 files changed, 149 insertions, 87 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
diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs
index 75a117798e..5c4b18621f 100644
--- a/compiler/GHC/Tc/Solver/Interact.hs
+++ b/compiler/GHC/Tc/Solver/Interact.hs
@@ -2352,7 +2352,7 @@ Other notes:
      - natural numbers
      - Typeable
 
-* See also Note [What might equal later?] in GHC.Tc.Solver.Monad.
+* See also Note [What might equal later?] in GHC.Tc.Solver.InertSet.
 
 * The given-overlap problem is arguably not easy to appear in practice
   due to our aggressive prioritization of equality solving over other
diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs
index c253770616..a039630887 100644
--- a/compiler/GHC/Tc/Solver/Monad.hs
+++ b/compiler/GHC/Tc/Solver/Monad.hs
@@ -631,92 +631,6 @@ getHasGivenEqs tclvl
     insoluble_given_equality ct
        = insolubleEqCt ct && isGivenCt ct
 
-{- 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.
-
-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}
--}
-
 removeInertCts :: [Ct] -> InertCans -> InertCans
 -- ^ Remove inert constraints from the 'InertCans', for use when a
 -- typechecker plugin wishes to discard a given.
diff --git a/testsuite/tests/typecheck/should_compile/T21208.hs b/testsuite/tests/typecheck/should_compile/T21208.hs
new file mode 100644
index 0000000000..fc90f99693
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T21208.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE FlexibleInstances #-}
+
+module T21208 where
+
+type family F a
+
+inject :: a -> F a
+inject = undefined
+
+class C a where
+  meth :: a -> ()
+
+instance C a where
+  meth _ = ()
+
+g :: C a => a -> ()
+g x = meth (inject x)
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 24574892e7..64828410f9 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -560,6 +560,7 @@ test('T11525', normal, multi_compile,
      [None, [('T11525_Plugin.hs', '-package ghc'), ('T11525.hs', '')],
       '-dynamic' if have_dynamic() else ''])
 test('T12923_1', normal, compile, [''])
+test('T21208', normal, compile, [''])
 test('T12923_2', normal, compile, [''])
 test('T12923_3', normal, compile, [''])
 test('T13381', normal, compile_fail, [''])