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

18 files changed, 282 insertions, 177 deletions

diff --git a/compiler/GHC/Core/Coercion/Opt.hs b/compiler/GHC/Core/Coercion/Opt.hs
index 108154e1c6..4353676af6 100644
--- a/compiler/GHC/Core/Coercion/Opt.hs
+++ b/compiler/GHC/Core/Coercion/Opt.hs
@@ -1005,7 +1005,7 @@ checkAxInstCo (AxiomInstCo ax ind cos)
     check_no_conflict _    [] = Nothing
     check_no_conflict flat (b@CoAxBranch { cab_lhs = lhs_incomp } : rest)
          -- See Note [Apartness] in GHC.Core.FamInstEnv
-      | SurelyApart <- tcUnifyTysFG (const BindMe) flat lhs_incomp
+      | SurelyApart <- tcUnifyTysFG alwaysBindFun flat lhs_incomp
       = check_no_conflict flat rest
       | otherwise
       = Just b
diff --git a/compiler/GHC/Core/FamInstEnv.hs b/compiler/GHC/Core/FamInstEnv.hs
index 0876cacf57..3e0fc7361d 100644
--- a/compiler/GHC/Core/FamInstEnv.hs
+++ b/compiler/GHC/Core/FamInstEnv.hs
@@ -522,7 +522,7 @@ compatibleBranches (CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 })
                    (CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 })
   = let (commonlhs1, commonlhs2) = zipAndUnzip lhs1 lhs2
              -- See Note [Compatibility of eta-reduced axioms]
-    in case tcUnifyTysFG (const BindMe) commonlhs1 commonlhs2 of
+    in case tcUnifyTysFG alwaysBindFun commonlhs1 commonlhs2 of
       SurelyApart -> True
       Unifiable subst
         | Type.substTyAddInScope subst rhs1 `eqType`
@@ -1204,7 +1204,7 @@ apartnessCheck :: [Type]
                -> Bool       -- ^ True <=> equation can fire
 apartnessCheck flattened_target (CoAxBranch { cab_incomps = incomps })
   = all (isSurelyApart
-         . tcUnifyTysFG (const BindMe) flattened_target
+         . tcUnifyTysFG alwaysBindFun flattened_target
          . coAxBranchLHS) incomps
   where
     isSurelyApart SurelyApart = True
diff --git a/compiler/GHC/Core/InstEnv.hs b/compiler/GHC/Core/InstEnv.hs
index 1d1d550aca..24e1d84107 100644
--- a/compiler/GHC/Core/InstEnv.hs
+++ b/compiler/GHC/Core/InstEnv.hs
@@ -1060,9 +1060,9 @@ incoherent instances as long as there are others.
 ************************************************************************
 -}
 
-instanceBindFun :: TyCoVar -> BindFlag
-instanceBindFun tv | isOverlappableTyVar tv = Skolem
-                   | otherwise              = BindMe
+instanceBindFun :: BindFun
+instanceBindFun tv _rhs_ty | isOverlappableTyVar tv = Apart
+                           | otherwise              = BindMe
    -- Note [Binding when looking up instances]
 
 {-
@@ -1085,7 +1085,7 @@ them in the unification test. These are called "super skolems". Example:
 The op [x,x] means we need (Foo [a]). This `a` will never be instantiated, and
 so it is a super skolem. (See the use of tcInstSuperSkolTyVarsX in
 GHC.Tc.Gen.Pat.tcDataConPat.) Super skolems respond True to
-isOverlappableTyVar, and the use of Skolem in instanceBindFun, above, means
+isOverlappableTyVar, and the use of Apart in instanceBindFun, above, means
 that these will be treated as fresh constants in the unification algorithm
 during instance lookup. Without this treatment, GHC would complain, saying
 that the choice of instance depended on the instantiation of 'a'; but of
diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs
index 104f53d8c9..14ebb47b1e 100644
--- a/compiler/GHC/Core/Lint.hs
+++ b/compiler/GHC/Core/Lint.hs
@@ -2472,7 +2472,7 @@ compatible_branches (CoAxBranch { cab_tvs = tvs1
         lhs2'          = substTys subst lhs2
         rhs2'          = substTy  subst rhs2
     in
-    case tcUnifyTys (const BindMe) lhs1 lhs2' of
+    case tcUnifyTys alwaysBindFun lhs1 lhs2' of
       Just unifying_subst -> substTy unifying_subst rhs1  `eqType`
                              substTy unifying_subst rhs2'
       Nothing             -> True
diff --git a/compiler/GHC/Core/Unify.hs b/compiler/GHC/Core/Unify.hs
index 0c8f82d0e4..81492afc86 100644
--- a/compiler/GHC/Core/Unify.hs
+++ b/compiler/GHC/Core/Unify.hs
@@ -17,7 +17,7 @@ module GHC.Core.Unify (
         -- Side-effect free unification
         tcUnifyTy, tcUnifyTyKi, tcUnifyTys, tcUnifyTyKis,
         tcUnifyTysFG, tcUnifyTyWithTFs,
-        BindFlag(..),
+        BindFun, BindFlag(..), matchBindFun, alwaysBindFun,
         UnifyResult, UnifyResultM(..), MaybeApartReason(..),
 
         -- Matching a type against a lifted type (coercion)
@@ -109,6 +109,16 @@ How do you choose between them?
    equals the kind of the target, then use the TyKi version.
 -}
 
+-- | Some unification functions are parameterised by a 'BindFun', which
+-- says whether or not to allow a certain unification to take place.
+-- A 'BindFun' takes the 'TyVar' involved along with the 'Type' it will
+-- potentially be bound to.
+--
+-- It is possible for the variable to actually be a coercion variable
+-- (Note [Matching coercion variables]), but only when one-way matching.
+-- In this case, the 'Type' will be a 'CoercionTy'.
+type BindFun = TyCoVar -> Type -> BindFlag
+
 -- | @tcMatchTy t1 t2@ produces a substitution (over fvs(t1))
 -- @s@ such that @s(t1)@ equals @t2@.
 -- The returned substitution might bind coercion variables,
@@ -124,7 +134,7 @@ How do you choose between them?
 tcMatchTy :: Type -> Type -> Maybe TCvSubst
 tcMatchTy ty1 ty2 = tcMatchTys [ty1] [ty2]
 
-tcMatchTyX_BM :: (TyVar -> BindFlag) -> TCvSubst
+tcMatchTyX_BM :: BindFun -> TCvSubst
               -> Type -> Type -> Maybe TCvSubst
 tcMatchTyX_BM bind_me subst ty1 ty2
   = tc_match_tys_x bind_me False subst [ty1] [ty2]
@@ -134,7 +144,7 @@ tcMatchTyX_BM bind_me subst ty1 ty2
 -- See also Note [tcMatchTy vs tcMatchTyKi]
 tcMatchTyKi :: Type -> Type -> Maybe TCvSubst
 tcMatchTyKi ty1 ty2
-  = tc_match_tys (const BindMe) True [ty1] [ty2]
+  = tc_match_tys alwaysBindFun True [ty1] [ty2]
 
 -- | This is similar to 'tcMatchTy', but extends a substitution
 -- See also Note [tcMatchTy vs tcMatchTyKi]
@@ -143,7 +153,7 @@ tcMatchTyX :: TCvSubst            -- ^ Substitution to extend
            -> Type                -- ^ Target
            -> Maybe TCvSubst
 tcMatchTyX subst ty1 ty2
-  = tc_match_tys_x (const BindMe) False subst [ty1] [ty2]
+  = tc_match_tys_x alwaysBindFun False subst [ty1] [ty2]
 
 -- | Like 'tcMatchTy' but over a list of types.
 -- See also Note [tcMatchTy vs tcMatchTyKi]
@@ -152,7 +162,7 @@ tcMatchTys :: [Type]         -- ^ Template
            -> Maybe TCvSubst -- ^ One-shot; in principle the template
                              -- variables could be free in the target
 tcMatchTys tys1 tys2
-  = tc_match_tys (const BindMe) False tys1 tys2
+  = tc_match_tys alwaysBindFun False tys1 tys2
 
 -- | Like 'tcMatchTyKi' but over a list of types.
 -- See also Note [tcMatchTy vs tcMatchTyKi]
@@ -160,7 +170,7 @@ tcMatchTyKis :: [Type]         -- ^ Template
              -> [Type]         -- ^ Target
              -> Maybe TCvSubst -- ^ One-shot substitution
 tcMatchTyKis tys1 tys2
-  = tc_match_tys (const BindMe) True tys1 tys2
+  = tc_match_tys alwaysBindFun True tys1 tys2
 
 -- | Like 'tcMatchTys', but extending a substitution
 -- See also Note [tcMatchTy vs tcMatchTyKi]
@@ -169,7 +179,7 @@ tcMatchTysX :: TCvSubst       -- ^ Substitution to extend
             -> [Type]         -- ^ Target
             -> Maybe TCvSubst -- ^ One-shot substitution
 tcMatchTysX subst tys1 tys2
-  = tc_match_tys_x (const BindMe) False subst tys1 tys2
+  = tc_match_tys_x alwaysBindFun False subst tys1 tys2
 
 -- | Like 'tcMatchTyKis', but extending a substitution
 -- See also Note [tcMatchTy vs tcMatchTyKi]
@@ -178,21 +188,21 @@ tcMatchTyKisX :: TCvSubst        -- ^ Substitution to extend
               -> [Type]          -- ^ Target
               -> Maybe TCvSubst  -- ^ One-shot substitution
 tcMatchTyKisX subst tys1 tys2
-  = tc_match_tys_x (const BindMe) True subst tys1 tys2
+  = tc_match_tys_x alwaysBindFun True subst tys1 tys2
 
 -- | Same as tc_match_tys_x, but starts with an empty substitution
-tc_match_tys :: (TyVar -> BindFlag)
-               -> Bool          -- ^ match kinds?
-               -> [Type]
-               -> [Type]
-               -> Maybe TCvSubst
+tc_match_tys :: BindFun
+             -> Bool          -- ^ match kinds?
+             -> [Type]
+             -> [Type]
+             -> Maybe TCvSubst
 tc_match_tys bind_me match_kis tys1 tys2
   = tc_match_tys_x bind_me match_kis (mkEmptyTCvSubst in_scope) tys1 tys2
   where
     in_scope = mkInScopeSet (tyCoVarsOfTypes tys1 `unionVarSet` tyCoVarsOfTypes tys2)
 
 -- | Worker for 'tcMatchTysX' and 'tcMatchTyKisX'
-tc_match_tys_x :: (TyVar -> BindFlag)
+tc_match_tys_x :: BindFun
                -> Bool          -- ^ match kinds?
                -> TCvSubst
                -> [Type]
@@ -225,9 +235,22 @@ ruleMatchTyKiX tmpl_tvs rn_env tenv tmpl target
       Unifiable (tenv', _) -> Just tenv'
       _                    -> Nothing
 
-matchBindFun :: TyCoVarSet -> TyVar -> BindFlag
-matchBindFun tvs tv = if tv `elemVarSet` tvs then BindMe else Skolem
-
+-- | Allow binding only for any variable in the set. Variables may
+-- be bound to any type.
+-- Used when doing simple matching; e.g. can we find a substitution
+--
+-- @
+-- S = [a :-> t1, b :-> t2] such that
+--     S( Maybe (a, b->Int )  =   Maybe (Bool, Char -> Int)
+-- @
+matchBindFun :: TyCoVarSet -> BindFun
+matchBindFun tvs tv _ty
+  | tv `elemVarSet` tvs = BindMe
+  | otherwise           = Apart
+
+-- | Allow the binding of any variable to any type
+alwaysBindFun :: BindFun
+alwaysBindFun _tv _ty = BindMe
 
 {- *********************************************************************
 *                                                                      *
@@ -301,7 +324,7 @@ typesCantMatch :: [(Type,Type)] -> Bool
 typesCantMatch prs = any (uncurry cant_match) prs
   where
     cant_match :: Type -> Type -> Bool
-    cant_match t1 t2 = case tcUnifyTysFG (const BindMe) [t1] [t2] of
+    cant_match t1 t2 = case tcUnifyTysFG alwaysBindFun [t1] [t2] of
       SurelyApart -> True
       _           -> False
 
@@ -409,11 +432,11 @@ indexed-types/should_compile/Overlap14.
 tcUnifyTy :: Type -> Type       -- All tyvars are bindable
           -> Maybe TCvSubst
                        -- A regular one-shot (idempotent) substitution
-tcUnifyTy t1 t2 = tcUnifyTys (const BindMe) [t1] [t2]
+tcUnifyTy t1 t2 = tcUnifyTys alwaysBindFun [t1] [t2]
 
 -- | Like 'tcUnifyTy', but also unifies the kinds
 tcUnifyTyKi :: Type -> Type -> Maybe TCvSubst
-tcUnifyTyKi t1 t2 = tcUnifyTyKis (const BindMe) [t1] [t2]
+tcUnifyTyKi t1 t2 = tcUnifyTyKis alwaysBindFun [t1] [t2]
 
 -- | Unify two types, treating type family applications as possibly unifying
 -- with anything and looking through injective type family applications.
@@ -427,7 +450,7 @@ tcUnifyTyWithTFs :: Bool  -- ^ True <=> do two-way unification;
 -- The code is incorporated with the standard unifier for convenience, but
 -- its operation should match the specification in the paper.
 tcUnifyTyWithTFs twoWay t1 t2
-  = case tc_unify_tys (const BindMe) twoWay True False
+  = case tc_unify_tys alwaysBindFun twoWay True False
                        rn_env emptyTvSubstEnv emptyCvSubstEnv
                        [t1] [t2] of
       Unifiable          (subst, _) -> Just $ maybe_fix subst
@@ -444,7 +467,7 @@ tcUnifyTyWithTFs twoWay t1 t2
                                                -- domain with range
 
 -----------------
-tcUnifyTys :: (TyCoVar -> BindFlag)
+tcUnifyTys :: BindFun
            -> [Type] -> [Type]
            -> Maybe TCvSubst
                                 -- ^ A regular one-shot (idempotent) substitution
@@ -459,7 +482,7 @@ tcUnifyTys bind_fn tys1 tys2
       _                -> Nothing
 
 -- | Like 'tcUnifyTys' but also unifies the kinds
-tcUnifyTyKis :: (TyCoVar -> BindFlag)
+tcUnifyTyKis :: BindFun
              -> [Type] -> [Type]
              -> Maybe TCvSubst
 tcUnifyTyKis bind_fn tys1 tys2
@@ -511,20 +534,20 @@ instance Monad UnifyResultM where
 -- @s(tys1)@ and that of @s(tys2)@ are equal, as witnessed by the returned
 -- Coercions. This version requires that the kinds of the types are the same,
 -- if you unify left-to-right.
-tcUnifyTysFG :: (TyVar -> BindFlag)
+tcUnifyTysFG :: BindFun
              -> [Type] -> [Type]
              -> UnifyResult
 tcUnifyTysFG bind_fn tys1 tys2
   = tc_unify_tys_fg False bind_fn tys1 tys2
 
-tcUnifyTyKisFG :: (TyVar -> BindFlag)
+tcUnifyTyKisFG :: BindFun
                -> [Type] -> [Type]
                -> UnifyResult
 tcUnifyTyKisFG bind_fn tys1 tys2
   = tc_unify_tys_fg True bind_fn tys1 tys2
 
 tc_unify_tys_fg :: Bool
-                -> (TyVar -> BindFlag)
+                -> BindFun
                 -> [Type] -> [Type]
                 -> UnifyResult
 tc_unify_tys_fg match_kis bind_fn tys1 tys2
@@ -538,7 +561,7 @@ tc_unify_tys_fg match_kis bind_fn tys1 tys2
 
 -- | This function is actually the one to call the unifier -- a little
 -- too general for outside clients, though.
-tc_unify_tys :: (TyVar -> BindFlag)
+tc_unify_tys :: BindFun
              -> AmIUnifying -- ^ True <=> unify; False <=> match
              -> Bool        -- ^ True <=> doing an injectivity check
              -> Bool        -- ^ True <=> treat the kinds as well
@@ -1102,18 +1125,17 @@ unify_ty env (CoercionTy co1) (CoercionTy co2) kco
            CoVarCo cv
              | not (um_unif env)
              , not (cv `elemVarEnv` c_subst)
-             , BindMe <- tvBindFlag env cv
-             -> do { checkRnEnv env (tyCoVarsOfCo co2)
-                   ; let (_, co_l, co_r) = decomposeFunCo Nominal kco
-                     -- Because the coercion is nominal, it should be safe to
+             , let (_, co_l, co_r) = decomposeFunCo Nominal kco
+                     -- Because the coercion is used in a type, it should be safe to
                      -- ignore the multiplicity coercion.
                       -- cv :: t1 ~ t2
                       -- co2 :: s1 ~ s2
                       -- co_l :: t1 ~ s1
                       -- co_r :: t2 ~ s2
-                   ; extendCvEnv cv (co_l `mkTransCo`
-                                     co2 `mkTransCo`
-                                     mkSymCo co_r) }
+                   rhs_co = co_l `mkTransCo` co2 `mkTransCo` mkSymCo co_r
+             , BindMe <- tvBindFlag env cv (CoercionTy rhs_co)
+             -> do { checkRnEnv env (tyCoVarsOfCo co2)
+                   ; extendCvEnv cv rhs_co }
            _ -> return () }
 
 unify_ty _ _ _ _ = surelyApart
@@ -1206,13 +1228,15 @@ uUnrefined env tv1' ty2 ty2' kco
 
     do {   -- So both are unrefined
            -- Bind one or the other, depending on which is bindable
-       ; let b1  = tvBindFlag env tv1'
-             b2  = tvBindFlag env tv2'
+       ; let rhs1 = ty2 `mkCastTy` mkSymCo kco
+             rhs2 = ty1 `mkCastTy` kco
+             b1  = tvBindFlag env tv1' rhs1
+             b2  = tvBindFlag env tv2' rhs2
              ty1 = mkTyVarTy tv1'
        ; case (b1, b2) of
-           (BindMe, _) -> bindTv env tv1' (ty2 `mkCastTy` mkSymCo kco)
+           (BindMe, _) -> bindTv env tv1' rhs1
            (_, BindMe) | um_unif env
-                       -> bindTv (umSwapRn env) tv2 (ty1 `mkCastTy` kco)
+                       -> bindTv (umSwapRn env) tv2 rhs2
 
            _ | tv1' == tv2' -> return ()
              -- How could this happen? If we're only matching and if
@@ -1222,9 +1246,11 @@ uUnrefined env tv1' ty2 ty2' kco
   }}}}
 
 uUnrefined env tv1' ty2 _ kco -- ty2 is not a type variable
-  = case tvBindFlag env tv1' of
-      Skolem -> surelyApart
-      BindMe -> bindTv env tv1' (ty2 `mkCastTy` mkSymCo kco)
+  = case tvBindFlag env tv1' rhs of
+      Apart  -> surelyApart
+      BindMe -> bindTv env tv1' rhs
+  where
+    rhs = ty2 `mkCastTy` mkSymCo kco
 
 bindTv :: UMEnv -> OutTyVar -> Type -> UM ()
 -- OK, so we want to extend the substitution with tv := ty
@@ -1262,14 +1288,16 @@ occursCheck env tv free_tvs
 -}
 
 data BindFlag
-  = BindMe      -- A regular type variable
+  = BindMe      -- ^ A regular type variable
 
-  | Skolem      -- This type variable is a skolem constant
-                -- Don't bind it; it only matches itself
-                -- These variables are SurelyApart from other types
-                -- See Note [Binding when looking up instances] in GHC.Core.InstEnv
-                -- for why it must be SurelyApart.
+  | Apart       -- ^ Declare that this type variable is /apart/ from the
+                -- type provided. That is, the type variable will never
+                -- be instantiated to that type.
+                -- See also Note [Binding when looking up instances]
+                -- in GHC.Core.InstEnv.
   deriving Eq
+-- NB: It would be conceivable to have an analogue to MaybeApart here,
+-- but there is not yet a need.
 
 {-
 ************************************************************************
@@ -1296,7 +1324,7 @@ data UMEnv
             -- Do not bind these in the substitution!
             -- See the function tvBindFlag
 
-          , um_bind_fun :: TyVar -> BindFlag
+          , um_bind_fun :: BindFun
             -- User-supplied BindFlag function,
             -- for variables not in um_skols
           }
@@ -1340,10 +1368,10 @@ initUM subst_env cv_subst_env um
     state = UMState { um_tv_env = subst_env
                     , um_cv_env = cv_subst_env }
 
-tvBindFlag :: UMEnv -> OutTyVar -> BindFlag
-tvBindFlag env tv
-  | tv `elemVarSet` um_skols env = Skolem
-  | otherwise                    = um_bind_fun env tv
+tvBindFlag :: UMEnv -> OutTyVar -> Type -> BindFlag
+tvBindFlag env tv rhs
+  | tv `elemVarSet` um_skols env = Apart
+  | otherwise                    = um_bind_fun env tv rhs
 
 getTvSubstEnv :: UM TvSubstEnv
 getTvSubstEnv = UM $ \state -> Unifiable (state, um_tv_env state)
@@ -1843,7 +1871,7 @@ flattenTysX :: InScopeSet -> [Type] -> ([Type], TyVarEnv (TyCon, [Type]))
 --     can't really sensibly refer to that b. So it may include a locally-
 --     bound tyvar in its range. Currently, the only usage of this env't
 --     checks whether there are any meta-variables in it
---     (in GHC.Tc.Solver.Monad.mightMatchLater), so this is all OK.
+--     (in GHC.Tc.Solver.Monad.mightEqualLater), so this is all OK.
 flattenTysX in_scope tys
   = let (env, result) = coreFlattenTys emptyTvSubstEnv (emptyFlattenEnv in_scope) tys in
     (result, build_env (fe_type_map env))
diff --git a/compiler/GHC/Tc/Gen/Sig.hs b/compiler/GHC/Tc/Gen/Sig.hs
index f3934e6f78..466191b3c7 100644
--- a/compiler/GHC/Tc/Gen/Sig.hs
+++ b/compiler/GHC/Tc/Gen/Sig.hs
@@ -512,7 +512,7 @@ So we instantiate f and g's signature with TyVarTv skolems
 unification takes place, we'll find out when we do the final
 impedance-matching check in GHC.Tc.Gen.Bind.mkExport
 
-See Note [Signature skolems] in GHC.Tc.Utils.TcType
+See Note [TyVarTv] in GHC.Tc.Utils.TcMType
 
 None of this applies to a function binding with a complete
 signature, which doesn't use tcInstSig.  See GHC.Tc.Gen.Bind.tcPolyCheck.
diff --git a/compiler/GHC/Tc/Instance/FunDeps.hs b/compiler/GHC/Tc/Instance/FunDeps.hs
index c89a13dae8..3abb0140b1 100644
--- a/compiler/GHC/Tc/Instance/FunDeps.hs
+++ b/compiler/GHC/Tc/Instance/FunDeps.hs
@@ -656,9 +656,7 @@ checkFunDeps inst_envs (ClsInst { is_tvs = qtvs1, is_cls = cls
         (ltys1, rtys1) = instFD fd cls_tvs tys1
         (ltys2, rtys2) = instFD fd cls_tvs tys2
         qtv_set2       = mkVarSet qtvs2
-        bind_fn tv | tv `elemVarSet` qtv_set1 = BindMe
-                   | tv `elemVarSet` qtv_set2 = BindMe
-                   | otherwise                = Skolem
+        bind_fn        = matchBindFun (qtv_set1 `unionVarSet` qtv_set2)
 
     eq_inst i1 i2 = instanceDFunId i1 == instanceDFunId i2
         -- A single instance may appear twice in the un-nubbed conflict list
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}
diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs
index 0e387c6247..680d3d33b7 100644
--- a/compiler/GHC/Tc/TyCl.hs
+++ b/compiler/GHC/Tc/TyCl.hs
@@ -1083,7 +1083,7 @@ We do kind inference as follows:
   These unification variables
     - Are TyVarTvs: that is, unification variables that can
       unify only with other type variables.
-      See Note [Signature skolems] in GHC.Tc.Utils.TcType
+      See Note [TyVarTv] in GHC.Tc.Utils.TcMType
 
     - Have complete fresh Names; see GHC.Tc.Utils.TcMType
       Note [Unification variables need fresh Names]
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index 24b7e4d93a..ed9ee9cc44 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -766,21 +766,27 @@ the thinking.
 {- Note [TyVarTv]
 ~~~~~~~~~~~~~~~~~
 A TyVarTv can unify with type *variables* only, including other TyVarTvs and
-skolems. Sometimes, they can unify with type variables that the user would
-rather keep distinct; see #11203 for an example.  So, any client of this
-function needs to either allow the TyVarTvs to unify with each other or check
-that they don't (say, with a call to findDubTyVarTvs).
-
-Before #15050 this (under the name SigTv) was used for ScopedTypeVariables in
-patterns, to make sure these type variables only refer to other type variables,
-but this restriction was dropped, and ScopedTypeVariables can now refer to full
-types (GHC Proposal 29).
-
-The remaining uses of newTyVarTyVars are
-* In kind signatures, see
-  GHC.Tc.TyCl Note [Inferring kinds for type declarations]
-          and Note [Kind checking for GADTs]
-* In partial type signatures, see Note [Quantified variables in partial type signatures]
+skolems.  They are used in two places:
+
+1. In kind signatures, see GHC.Tc.TyCl
+      Note [Inferring kinds for type declarations]
+   and Note [Kind checking for GADTs]
+
+2. In partial type signatures.  See GHC.Tc.Types
+   Note [Quantified variables in partial type signatures]
+
+Sometimes, they can unify with type variables that the user would
+rather keep distinct; see #11203 for an example.  So, any client of
+this function needs to either allow the TyVarTvs to unify with each
+other or check that they don't. In the case of (1) the check is done
+in GHC.Tc.TyCl.swizzleTcTyConBndrs.  In case of (2) it's done by
+findDupTyVarTvs in GHC.Tc.Gen.Bind.chooseInferredQuantifiers.
+
+Historical note: Before #15050 this (under the name SigTv) was also
+used for ScopedTypeVariables in patterns, to make sure these type
+variables only refer to other type variables, but this restriction was
+dropped, and ScopedTypeVariables can now refer to full types (GHC
+Proposal 29).
 -}
 
 newMetaTyVarName :: FastString -> TcM Name
@@ -1777,7 +1783,7 @@ defaultTyVar default_kind tv
 
   | isTyVarTyVar tv
     -- Do not default TyVarTvs. Doing so would violate the invariants
-    -- on TyVarTvs; see Note [Signature skolems] in GHC.Tc.Utils.TcType.
+    -- on TyVarTvs; see Note [TyVarTv] in GHC.Tc.Utils.TcMType.
     -- #13343 is an example; #14555 is another
     -- See Note [Inferring kinds for type declarations] in GHC.Tc.TyCl
   = return False
diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs
index 9ec129ef4a..0a0d341a47 100644
--- a/compiler/GHC/Tc/Utils/TcType.hs
+++ b/compiler/GHC/Tc/Utils/TcType.hs
@@ -457,26 +457,6 @@ checking.  It's attached to mutable type variables only.
 It's knot-tied back to "GHC.Types.Var".  There is no reason in principle
 why "GHC.Types.Var" shouldn't actually have the definition, but it "belongs" here.
 
-Note [Signature skolems]
-~~~~~~~~~~~~~~~~~~~~~~~~
-A TyVarTv is a specialised variant of TauTv, with the following invariants:
-
-    * A TyVarTv can be unified only with a TyVar,
-      not with any other type
-
-    * Its MetaDetails, if filled in, will always be another TyVarTv
-      or a SkolemTv
-
-TyVarTvs are only distinguished to improve error messages.
-Consider this
-
-  data T (a:k1) = MkT (S a)
-  data S (b:k2) = MkS (T b)
-
-When doing kind inference on {S,T} we don't want *skolems* for k1,k2,
-because they end up unifying; we want those TyVarTvs again.
-
-
 Note [TyVars and TcTyVars during type checking]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The Var type has constructors TyVar and TcTyVar.  They are used
@@ -547,7 +527,7 @@ data MetaInfo
 
    | TyVarTv       -- A variant of TauTv, except that it should not be
                    --   unified with a type, only with a type variable
-                   -- See Note [Signature skolems]
+                   -- See Note [TyVarTv] in GHC.Tc.Utils.TcMType
 
    | RuntimeUnkTv  -- A unification variable used in the GHCi debugger.
                    -- It /is/ allowed to unify with a polytype, unlike TauTv
diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs
index 735edc8ff0..f5cf306dc1 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs
+++ b/compiler/GHC/Tc/Utils/Unify.hs
@@ -1582,7 +1582,7 @@ Needless to say, all three have wrinkles:
   up a fresh gamma[n], and unify beta[k] := gamma[n].
 
 * (TYVAR-TV) Unification variables.  Suppose alpha[tyv,n] is a level-n
-  TyVarTv (see Note [Signature skolems] in GHC.Tc.Types.TcType)? Now
+  TyVarTv (see Note [TyVarTv] in GHC.Tc.Types.TcMType)? Now
   consider alpha[tyv,n] ~ Bool.  We don't want to unify because that
   would break the TyVarTv invariant.
 
diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index ff6a89d02f..7a83bfc573 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -2452,8 +2452,8 @@ checkConsistentFamInst (InClsInst { ai_class = clas
     -- The /scoped/ type variables from the class-instance header
     -- should not be alpha-renamed.  Inferred ones can be.
     no_bind_set = mkVarSet inst_tvs
-    bind_me tv | tv `elemVarSet` no_bind_set = Skolem
-               | otherwise                   = BindMe
+    bind_me tv _ty | tv `elemVarSet` no_bind_set = Apart
+                   | otherwise                   = BindMe
 
 
 {- Note [Check type-family instance binders]
diff --git a/testsuite/tests/partial-sigs/should_compile/T19106.hs b/testsuite/tests/partial-sigs/should_compile/T19106.hs
new file mode 100644
index 0000000000..02f36744a0
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T19106.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE TypeFamilies, GADTs, PartialTypeSignatures #-}
+{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
+
+module T19106 where
+
+f :: (a ~ [b]) => T a -> _ -> String
+f (MkT x) _ = show x
+
+data T a where
+  MkT :: G a => a -> T a
+
+type family G a where
+  G [b] = Show b
diff --git a/testsuite/tests/partial-sigs/should_compile/all.T b/testsuite/tests/partial-sigs/should_compile/all.T
index 00d051447f..99627a15c2 100644
--- a/testsuite/tests/partial-sigs/should_compile/all.T
+++ b/testsuite/tests/partial-sigs/should_compile/all.T
@@ -79,6 +79,7 @@ test('T11670', normal, compile, [''])
 test('T12156', normal, compile_fail, ['-fdefer-typed-holes'])
 test('T12531', normal, compile, ['-fdefer-typed-holes'])
 test('T12845', normal, compile, [''])
+test('T19106', normal, compile, [''])
 test('T12844', normal, compile, [''])
 test('T13324_compile', normal, compile, ['-Wno-partial-type-signatures'])
 test('T13482', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_compile/T19107.hs b/testsuite/tests/typecheck/should_compile/T19107.hs
new file mode 100644
index 0000000000..c90ccbf207
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T19107.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE GADTs #-}
+-- NB: NO FlexibleContexts
+
+module T19107 where
+
+data T a where
+  MkT :: Show a => [a] -> T a
+
+f (MkT x) = show x
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 396d7ce15a..44e60ea55c 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -729,6 +729,7 @@ test('T18585', normal, compile, [''])
 test('T18831', normal, compile, [''])
 test('T18920', normal, compile, [''])
 test('T18939_Compile', normal, compile, [''])
+test('T19107', normal, compile, [''])
 test('T15942', normal, compile, [''])
 test('T17562b', normal, compile, [''])
 test('T17567StupidThetaB', normal, compile, [''])