Make matchableGivens more reliably correct.

This has two fixes:

1. Take TyVarTvs into account in matchableGivens. This
   fixes #19106.

2. Don't allow unifying alpha ~ Maybe alpha. This fixes
   #19107.

This patch also removes a redundant Note and redirects
references to a better replacement.

Also some refactoring/improvements around the BindFun
in the pure unifier, which now can take the RHS type
into account.

Close #19106.
Close #19107.

Test case: partial-sigs/should_compile/T19106,
           typecheck/should_compile/T19107

2 files changed, 140 insertions, 71 deletions

diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs
index 62e289b543..b1eb5bd712 100644
--- a/compiler/GHC/Tc/Solver/Interact.hs
+++ b/compiler/GHC/Tc/Solver/Interact.hs
@@ -2151,7 +2151,7 @@ Other notes:
      - natural numbers
      - Typeable
 
-* See also Note [What might match later?] in GHC.Tc.Solver.Monad.
+* See also Note [What might equal later?] in GHC.Tc.Solver.Monad.
 
 * The given-overlap problem is arguably not easy to appear in practice
   due to our aggressive prioritization of equality solving over other
@@ -2263,8 +2263,8 @@ matchLocalInst :: TcPredType -> CtLoc -> TcS ClsInstResult
 -- Look up the predicate in Given quantified constraints,
 -- which are effectively just local instance declarations.
 matchLocalInst pred loc
-  = do { ics <- getInertCans
-       ; case match_local_inst (inert_insts ics) of
+  = do { inerts@(IS { inert_cans = ics }) <- getTcSInerts
+       ; case match_local_inst inerts (inert_insts ics) of
            ([], False) -> do { traceTcS "No local instance for" (ppr pred)
                              ; return NoInstance }
            ([(dfun_ev, inst_tys)], unifs)
@@ -2281,14 +2281,15 @@ matchLocalInst pred loc
   where
     pred_tv_set = tyCoVarsOfType pred
 
-    match_local_inst :: [QCInst]
+    match_local_inst :: InertSet
+                     -> [QCInst]
                      -> ( [(CtEvidence, [DFunInstType])]
                         , Bool )      -- True <=> Some unify but do not match
-    match_local_inst []
+    match_local_inst _inerts []
       = ([], False)
-    match_local_inst (qci@(QCI { qci_tvs = qtvs, qci_pred = qpred
+    match_local_inst inerts (qci@(QCI { qci_tvs = qtvs, qci_pred = qpred
                                , qci_ev = ev })
-                     : qcis)
+                             : qcis)
       | let in_scope = mkInScopeSet (qtv_set `unionVarSet` pred_tv_set)
       , Just tv_subst <- ruleMatchTyKiX qtv_set (mkRnEnv2 in_scope)
                                         emptyTvSubstEnv qpred pred
@@ -2303,5 +2304,5 @@ matchLocalInst pred loc
         (matches, unif || this_unif)
       where
         qtv_set = mkVarSet qtvs
-        this_unif = mightMatchLater qpred (ctEvLoc ev) pred loc
-        (matches, unif) = match_local_inst qcis
+        this_unif = mightEqualLater inerts qpred (ctEvLoc ev) pred loc
+        (matches, unif) = match_local_inst inerts qcis
diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs
index 3f7be9a822..c5e9c343ae 100644
--- a/compiler/GHC/Tc/Solver/Monad.hs
+++ b/compiler/GHC/Tc/Solver/Monad.hs
@@ -63,7 +63,7 @@ module GHC.Tc.Solver.Monad (
     getInertEqs, getInertCans, getInertGivens,
     getInertInsols, getInnermostGivenEqLevel,
     getTcSInerts, setTcSInerts,
-    matchableGivens, prohibitedSuperClassSolve, mightMatchLater,
+    matchableGivens, prohibitedSuperClassSolve, mightEqualLater,
     getUnsolvedInerts,
     removeInertCts, getPendingGivenScs,
     addInertCan, insertFunEq, addInertForAll,
@@ -2322,7 +2322,7 @@ isOuterTyVar tclvl tv
 -- Given might overlap with an instance. See Note [Instance and Given overlap]
 -- in "GHC.Tc.Solver.Interact"
 matchableGivens :: CtLoc -> PredType -> InertSet -> Cts
-matchableGivens loc_w pred_w (IS { inert_cans = inert_cans })
+matchableGivens loc_w pred_w inerts@(IS { inert_cans = inert_cans })
   = filterBag matchable_given all_relevant_givens
   where
     -- just look in class constraints and irreds. matchableGivens does get called
@@ -2340,50 +2340,81 @@ matchableGivens loc_w pred_w (IS { inert_cans = inert_cans })
     matchable_given :: Ct -> Bool
     matchable_given ct
       | CtGiven { ctev_loc = loc_g, ctev_pred = pred_g } <- ctEvidence ct
-      = mightMatchLater pred_g loc_g pred_w loc_w
+      = mightEqualLater inerts pred_g loc_g pred_w loc_w
 
       | otherwise
       = False
 
-mightMatchLater :: TcPredType -> CtLoc -> TcPredType -> CtLoc -> Bool
--- See Note [What might match later?]
-mightMatchLater given_pred given_loc wanted_pred wanted_loc
+mightEqualLater :: InertSet -> TcPredType -> CtLoc -> TcPredType -> CtLoc -> Bool
+-- See Note [What might equal later?]
+-- Used to implement logic in Note [Instance and Given overlap] in GHC.Tc.Solver.Interact
+mightEqualLater (IS { inert_cycle_breakers = cbvs })
+                given_pred given_loc wanted_pred wanted_loc
   | prohibitedSuperClassSolve given_loc wanted_loc
   = False
 
-  | SurelyApart <- tcUnifyTysFG bind_meta_tv [flattened_given] [flattened_wanted]
-  = False
-
   | otherwise
-  = True   -- safe answer
+  = case tcUnifyTysFG bind_fun [flattened_given] [flattened_wanted] of
+      SurelyApart              -> False  -- types that are surely apart do not equal later
+      MaybeApart MARInfinite _ -> False  -- see Example 7 in the Note.
+      _                        -> True
+
   where
     in_scope  = mkInScopeSet $ tyCoVarsOfTypes [given_pred, wanted_pred]
 
     -- NB: flatten both at the same time, so that we can share mappings
     -- from type family applications to variables, and also to guarantee
     -- that the fresh variables are really fresh between the given and
-    -- the wanted.
+    -- the wanted. Flattening both at the same time is needed to get
+    -- Example 10 from the Note.
     ([flattened_given, flattened_wanted], var_mapping)
       = flattenTysX in_scope [given_pred, wanted_pred]
 
-    bind_meta_tv :: TcTyVar -> BindFlag
-    -- Any meta tyvar may be unified later, so we treat it as
-    -- bindable when unifying with givens. That ensures that we
-    -- conservatively assume that a meta tyvar might get unified with
-    -- something that matches the 'given', until demonstrated
-    -- otherwise.  More info in Note [Instance and Given overlap]
-    -- in GHC.Tc.Solver.Interact
-    bind_meta_tv tv | is_meta_tv tv = BindMe
+    bind_fun :: BindFun
+    bind_fun tv rhs_ty
+      | isMetaTyVar tv
+      , can_unify tv (metaTyVarInfo tv) rhs_ty
+         -- this checks for CycleBreakerTvs and TyVarTvs; forgetting
+         -- the latter was #19106.
+      = BindMe
 
-                    | Just (_fam_tc, fam_args) <- lookupVarEnv var_mapping tv
-                    , anyFreeVarsOfTypes is_meta_tv fam_args
-                    = BindMe
+         -- See Examples 4, 5, and 6 from the Note
+      | Just (_fam_tc, fam_args) <- lookupVarEnv var_mapping tv
+      , anyFreeVarsOfTypes mentions_meta_ty_var fam_args
+      = BindMe
 
-                    | otherwise     = Skolem
+      | otherwise
+      = Apart
+
+    -- True for TauTv and TyVarTv (and RuntimeUnkTv) meta-tyvars
+    -- (as they can be unified)
+    -- and also for CycleBreakerTvs that mentions meta-tyvars
+    mentions_meta_ty_var :: TyVar -> Bool
+    mentions_meta_ty_var tv
+      | isMetaTyVar tv
+      = case metaTyVarInfo tv of
+          -- See Examples 8 and 9 in the Note
+          CycleBreakerTv
+            | Just tyfam_app <- lookup tv cbvs
+            -> anyFreeVarsOfType mentions_meta_ty_var tyfam_app
+            | otherwise
+            -> pprPanic "mightEqualLater finds an unbound cbv" (ppr tv $$ ppr cbvs)
+          _ -> True
+      | otherwise
+      = False
 
-     -- CycleBreakerTvs really stands for a type family application in
-     -- a given; these won't contain touchable meta-variables
-    is_meta_tv = isMetaTyVar <&&> not . isCycleBreakerTyVar
+    -- like canSolveByUnification, but allows cbv variables to unify
+    can_unify :: TcTyVar -> MetaInfo -> Type -> Bool
+    can_unify _lhs_tv TyVarTv rhs_ty  -- see Example 3 from the Note
+      | Just rhs_tv <- tcGetTyVar_maybe rhs_ty
+      = case tcTyVarDetails rhs_tv of
+          MetaTv { mtv_info = TyVarTv } -> True
+          MetaTv {}                     -> False  -- could unify with anything
+          SkolemTv {}                   -> True
+          RuntimeUnk                    -> True
+      | otherwise  -- not a var on the RHS
+      = False
+    can_unify lhs_tv _other _rhs_ty = mentions_meta_ty_var lhs_tv
 
 prohibitedSuperClassSolve :: CtLoc -> CtLoc -> Bool
 -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
@@ -2401,50 +2432,87 @@ because it is a candidate for floating out of this implication.  We
 only float equalities with a meta-tyvar on the left, so we only pull
 those out here.
 
-Note [What might match later?]
+Note [What might equal later?]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We must determine whether a Given might later match a Wanted. We
+We must determine whether a Given might later equal a Wanted. We
 definitely need to account for the possibility that any metavariable
-in the Wanted might be arbitrarily instantiated. We do *not* want
-to allow skolems in the Given to be instantiated. But what about
-type family applications? (Examples are below the explanation.)
+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 Givens] 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 allow flexibility in how type family applications unify we use
-the Core flattener. See
+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 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.
-
-Examples:
-    [G] C a
-    [W] C alpha
-  This easily might match later.
-
-    [G] C a
-    [W] C (F alpha)
-  This might match later, too, but we need to flatten the (F alpha)
-  to a fresh variable so that the unifier can connect the two.
-
-    [G] C (F alpha)
-    [W] C a
-  This also might match later. Again, we will need to flatten to
-  find this out. (Surprised about a metavariable in a Given? That
-  can easily happen -- See Note [GivenInv] in GHC.Tc.Utils.TcType.)
-
-    [G] C (F a)
-    [W] C a
-  This won't match later. We're not going to get new Givens that
-  can inform the F a, and so this is a no-go.
+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}