Remove flattening variables

This patch redesigns the flattener to simplify type family applications
directly instead of using flattening meta-variables and skolems. The key new
innovation is the CanEqLHS type and the new CEqCan constraint (Ct). A CanEqLHS
is either a type variable or exactly-saturated type family application; either
can now be rewritten using a CEqCan constraint in the inert set.

Because the flattener no longer reduces all type family applications to
variables, there was some performance degradation if a lengthy type family
application is now flattened over and over (not making progress). To
compensate, this patch contains some extra optimizations in the flattener,
leading to a number of performance improvements.

Close #18875.
Close #18910.

There are many extra parts of the compiler that had to be affected in writing
this patch:

* The family-application cache (formerly the flat-cache) sometimes stores
  coercions built from Given inerts. When these inerts get kicked out, we must
  kick out from the cache as well. (This was, I believe, true previously, but
  somehow never caused trouble.) Kicking out from the cache requires adding a
  filterTM function to TrieMap.

* This patch obviates the need to distinguish "blocking" coercion holes from
  non-blocking ones (which, previously, arose from CFunEqCans). There is thus
  some simplification around coercion holes.

* Extra commentary throughout parts of the code I read through, to preserve
  the knowledge I gained while working.

* A change in the pure unifier around unifying skolems with other types.
  Unifying a skolem now leads to SurelyApart, not MaybeApart, as documented
  in Note [Binding when looking up instances] in GHC.Core.InstEnv.

* Some more use of MCoercion where appropriate.

* Previously, class-instance lookup automatically noticed that e.g. C Int was
  a "unifier" to a target [W] C (F Bool), because the F Bool was flattened to
  a variable. Now, a little more care must be taken around checking for
  unifying instances.

* Previously, tcSplitTyConApp_maybe would split (Eq a => a). This is silly,
  because (=>) is not a tycon in Haskell. Fixed now, but there are some
  knock-on changes in e.g. TrieMap code and in the canonicaliser.

* New function anyFreeVarsOf{Type,Co} to check whether a free variable
  satisfies a certain predicate.

* Type synonyms now remember whether or not they are "forgetful"; a forgetful
  synonym drops at least one argument. This is useful when flattening; see
  flattenView.

* The pattern-match completeness checker invokes the solver. This invocation
  might need to look through newtypes when checking representational equality.
  Thus, the desugarer needs to keep track of the in-scope variables to know
  what newtype constructors are in scope. I bet this bug was around before but
  never noticed.

* Extra-constraints wildcards are no longer simplified before printing.
  See Note [Do not simplify ConstraintHoles] in GHC.Tc.Solver.

* Whether or not there are Given equalities has become slightly subtler.
  See the new HasGivenEqs datatype.

* Note [Type variable cycles in Givens] in GHC.Tc.Solver.Canonical
  explains a significant new wrinkle in the new approach.

* See Note [What might match later?] in GHC.Tc.Solver.Interact, which
  explains the fix to #18910.

* The inert_count field of InertCans wasn't actually used, so I removed
  it.

Though I (Richard) did the implementation, Simon PJ was very involved
in design and review.

This updates the Haddock submodule to avoid #18932 by adding
a type signature.

-------------------------
Metric Decrease:
    T12227
    T5030
    T9872a
    T9872b
    T9872c
Metric Increase:
    T9872d
-------------------------

14 files changed, 387 insertions, 153 deletions

diff --git a/compiler/GHC/Core/Coercion.hs b/compiler/GHC/Core/Coercion.hs
index 4413c7355b..051f415572 100644
--- a/compiler/GHC/Core/Coercion.hs
+++ b/compiler/GHC/Core/Coercion.hs
@@ -13,8 +13,8 @@
 --
 module GHC.Core.Coercion (
         -- * Main data type
-        Coercion, CoercionN, CoercionR, CoercionP, MCoercion(..), MCoercionR,
-        UnivCoProvenance, CoercionHole(..), BlockSubstFlag(..),
+        Coercion, CoercionN, CoercionR, CoercionP, MCoercion(..), MCoercionN, MCoercionR,
+        UnivCoProvenance, CoercionHole(..),
         coHoleCoVar, setCoHoleCoVar,
         LeftOrRight(..),
         Var, CoVar, TyCoVar,
@@ -69,8 +69,10 @@ module GHC.Core.Coercion (
         pickLR,
 
         isGReflCo, isReflCo, isReflCo_maybe, isGReflCo_maybe, isReflexiveCo, isReflexiveCo_maybe,
-        isReflCoVar_maybe, isGReflMCo,
-        coToMCo, mkTransMCo, mkTransMCoL,
+        isReflCoVar_maybe, isGReflMCo, mkGReflLeftMCo, mkGReflRightMCo,
+        mkCoherenceRightMCo,
+
+        coToMCo, mkTransMCo, mkTransMCoL, mkCastTyMCo, mkSymMCo, isReflMCo,
 
         -- ** Coercion variables
         mkCoVar, isCoVar, coVarName, setCoVarName, setCoVarUnique,
@@ -79,7 +81,7 @@ module GHC.Core.Coercion (
         -- ** Free variables
         tyCoVarsOfCo, tyCoVarsOfCos, coVarsOfCo,
         tyCoFVsOfCo, tyCoFVsOfCos, tyCoVarsOfCoDSet,
-        coercionSize,
+        coercionSize, anyFreeVarsOfCo,
 
         -- ** Substitution
         CvSubstEnv, emptyCvSubstEnv,
@@ -121,7 +123,8 @@ module GHC.Core.Coercion (
 
         simplifyArgsWorker,
 
-        badCoercionHole, badCoercionHoleCo
+        hasCoercionHoleTy, hasCoercionHoleCo,
+        HoleSet, coercionHolesOfType, coercionHolesOfCo
        ) where
 
 #include "HsVersions.h"
@@ -154,6 +157,7 @@ import GHC.Builtin.Types.Prim
 import GHC.Data.List.SetOps
 import GHC.Data.Maybe
 import GHC.Types.Unique.FM
+import GHC.Types.Unique.Set
 
 import GHC.Utils.Misc
 import GHC.Utils.Outputable
@@ -331,6 +335,32 @@ mkTransMCoL :: MCoercion -> Coercion -> MCoercion
 mkTransMCoL MRefl     co2 = MCo co2
 mkTransMCoL (MCo co1) co2 = MCo (mkTransCo co1 co2)
 
+-- | Get the reverse of an 'MCoercion'
+mkSymMCo :: MCoercion -> MCoercion
+mkSymMCo MRefl    = MRefl
+mkSymMCo (MCo co) = MCo (mkSymCo co)
+
+-- | Cast a type by an 'MCoercion'
+mkCastTyMCo :: Type -> MCoercion -> Type
+mkCastTyMCo ty MRefl    = ty
+mkCastTyMCo ty (MCo co) = ty `mkCastTy` co
+
+mkGReflLeftMCo :: Role -> Type -> MCoercionN -> Coercion
+mkGReflLeftMCo r ty MRefl    = mkReflCo r ty
+mkGReflLeftMCo r ty (MCo co) = mkGReflLeftCo r ty co
+
+mkGReflRightMCo :: Role -> Type -> MCoercionN -> Coercion
+mkGReflRightMCo r ty MRefl    = mkReflCo r ty
+mkGReflRightMCo r ty (MCo co) = mkGReflRightCo r ty co
+
+-- | Like 'mkCoherenceRightCo', but with an 'MCoercion'
+mkCoherenceRightMCo :: Role -> Type -> MCoercionN -> Coercion -> Coercion
+mkCoherenceRightMCo _ _  MRefl    co2 = co2
+mkCoherenceRightMCo r ty (MCo co) co2 = mkCoherenceRightCo r ty co co2
+
+isReflMCo :: MCoercion -> Bool
+isReflMCo MRefl = True
+isReflMCo _     = False
 
 {-
 %************************************************************************
@@ -1219,7 +1249,7 @@ mkKindCo co
   | otherwise
   = KindCo co
 
-mkSubCo :: Coercion -> Coercion
+mkSubCo :: HasDebugCallStack => Coercion -> Coercion
 -- Input coercion is Nominal, result is Representational
 -- see also Note [Role twiddling functions]
 mkSubCo (Refl ty) = GRefl Representational ty MRefl
@@ -1675,6 +1705,11 @@ data NormaliseStepResult ev
                                     -- ^ ev is evidence;
                                     -- Usually a co :: old type ~ new type
 
+instance Outputable ev => Outputable (NormaliseStepResult ev) where
+  ppr NS_Done           = text "NS_Done"
+  ppr NS_Abort          = text "NS_Abort"
+  ppr (NS_Step _ ty ev) = sep [text "NS_Step", ppr ty, ppr ev]
+
 mapStepResult :: (ev1 -> ev2)
               -> NormaliseStepResult ev1 -> NormaliseStepResult ev2
 mapStepResult f (NS_Step rec_nts ty ev) = NS_Step rec_nts ty (f ev)
@@ -2634,7 +2669,8 @@ FamInstEnv, and so lives here.
 
 Note [simplifyArgsWorker]
 ~~~~~~~~~~~~~~~~~~~~~~~~~
-Invariant (F2) of Note [Flattening] says that flattening is homogeneous.
+Invariant (F2) of Note [Flattening] in GHC.Tc.Solver.Flatten says that
+flattening is homogeneous.
 This causes some trouble when flattening a function applied to a telescope
 of arguments, perhaps with dependency. For example, suppose
 
@@ -2913,7 +2949,7 @@ simplifyArgsWorker :: [TyCoBinder] -> Kind
                    -> [(Type, Coercion)] -- flattened type arguments, arg
                                          -- each comes with the coercion used to flatten it,
                                          -- with co :: flattened_type ~ original_type
-                   -> ([Type], [Coercion], CoercionN)
+                   -> ([Type], [Coercion], MCoercionN)
 -- Returns (xis, cos, res_co), where each co :: xi ~ arg,
 -- and res_co :: kind (f xis) ~ kind (f tys), where f is the function applied to the args
 -- Precondition: if f :: forall bndrs. inner_ki (where bndrs and inner_ki are passed in),
@@ -2935,14 +2971,15 @@ simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs
        -> Kind        -- Unsubsted result kind of function (not a Pi-type)
        -> [Role]      -- Roles at which to flatten these ...
        -> [(Type, Coercion)]  -- flattened arguments, with their flattening coercions
-       -> ([Type], [Coercion], CoercionN)
+       -> ([Type], [Coercion], MCoercionN)
     go acc_xis acc_cos !lc binders inner_ki _ []
         -- The !lc makes the function strict in the lifting context
         -- which means GHC can unbox that pair.  A modest win.
       = (reverse acc_xis, reverse acc_cos, kind_co)
       where
         final_kind = mkPiTys binders inner_ki
-        kind_co = liftCoSubst Nominal lc final_kind
+        kind_co | noFreeVarsOfType final_kind = MRefl
+                | otherwise                   = MCo $ liftCoSubst Nominal lc final_kind
 
     go acc_xis acc_cos lc (binder:binders) inner_ki (role:roles) ((xi,co):args)
       = -- By Note [Flattening] in GHC.Tc.Solver.Flatten invariant (F2),
@@ -2998,7 +3035,7 @@ simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs
             (xis_out, cos_out, res_co_out)
               = go acc_xis acc_cos zapped_lc bndrs new_inner roles casted_args
         in
-        (xis_out, cos_out, res_co_out `mkTransCo` res_co)
+        (xis_out, cos_out, res_co_out `mkTransMCoL` res_co)
 
     go _ _ _ _ _ _ _ = panic
         "simplifyArgsWorker wandered into deeper water than usual"
@@ -3024,31 +3061,40 @@ simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs
 %************************************************************************
 -}
 
-bad_co_hole_ty :: Type -> Monoid.Any
-bad_co_hole_co :: Coercion -> Monoid.Any
-(bad_co_hole_ty, _, bad_co_hole_co, _)
+has_co_hole_ty :: Type -> Monoid.Any
+has_co_hole_co :: Coercion -> Monoid.Any
+(has_co_hole_ty, _, has_co_hole_co, _)
   = foldTyCo folder ()
   where
     folder = TyCoFolder { tcf_view  = const Nothing
                         , tcf_tyvar = const2 (Monoid.Any False)
                         , tcf_covar = const2 (Monoid.Any False)
-                        , tcf_hole  = const hole
+                        , tcf_hole  = const2 (Monoid.Any True)
                         , tcf_tycobinder = const2
                         }
 
     const2 :: a -> b -> c -> a
     const2 x _ _ = x
 
-    hole :: CoercionHole -> Monoid.Any
-    hole (CoercionHole { ch_blocker = YesBlockSubst }) = Monoid.Any True
-    hole _                                             = Monoid.Any False
+-- | Is there a coercion hole in this type?
+hasCoercionHoleTy :: Type -> Bool
+hasCoercionHoleTy = Monoid.getAny . has_co_hole_ty
+
+-- | Is there a coercion hole in this coercion?
+hasCoercionHoleCo :: Coercion -> Bool
+hasCoercionHoleCo = Monoid.getAny . has_co_hole_co
 
--- | Is there a blocking coercion hole in this type? See
--- "GHC.Tc.Solver.Canonical" Note [Equalities with incompatible kinds]
-badCoercionHole :: Type -> Bool
-badCoercionHole = Monoid.getAny . bad_co_hole_ty
+-- | A set of 'CoercionHole's
+type HoleSet = UniqSet CoercionHole
 
--- | Is there a blocking coercion hole in this coercion? See
--- GHC.Tc.Solver.Canonical Note [Equalities with incompatible kinds]
-badCoercionHoleCo :: Coercion -> Bool
-badCoercionHoleCo = Monoid.getAny . bad_co_hole_co
+-- | Extract out all the coercion holes from a given type
+coercionHolesOfType :: Type -> UniqSet CoercionHole
+coercionHolesOfCo   :: Coercion -> UniqSet CoercionHole
+(coercionHolesOfType, _, coercionHolesOfCo, _) = foldTyCo folder ()
+  where
+    folder = TyCoFolder { tcf_view  = const Nothing  -- don't look through synonyms
+                        , tcf_tyvar = \ _ _ -> mempty
+                        , tcf_covar = \ _ _ -> mempty
+                        , tcf_hole  = const unitUniqSet
+                        , tcf_tycobinder = \ _ _ _ -> ()
+                        }
diff --git a/compiler/GHC/Core/Coercion.hs-boot b/compiler/GHC/Core/Coercion.hs-boot
index 7a92a84eb6..0c18e5e68f 100644
--- a/compiler/GHC/Core/Coercion.hs-boot
+++ b/compiler/GHC/Core/Coercion.hs-boot
@@ -30,7 +30,7 @@ mkInstCo :: Coercion -> Coercion -> Coercion
 mkGReflCo :: Role -> Type -> MCoercionN -> Coercion
 mkNomReflCo :: Type -> Coercion
 mkKindCo :: Coercion -> Coercion
-mkSubCo :: Coercion -> Coercion
+mkSubCo :: HasDebugCallStack => Coercion -> Coercion
 mkProofIrrelCo :: Role -> Coercion -> Coercion -> Coercion -> Coercion
 mkAxiomRuleCo :: CoAxiomRule -> [Coercion] -> Coercion
 
diff --git a/compiler/GHC/Core/Coercion/Axiom.hs b/compiler/GHC/Core/Coercion/Axiom.hs
index ae7ae8971f..46b238e678 100644
--- a/compiler/GHC/Core/Coercion/Axiom.hs
+++ b/compiler/GHC/Core/Coercion/Axiom.hs
@@ -584,9 +584,21 @@ instance Outputable CoAxiomRule where
 -- Type checking of built-in families
 data BuiltInSynFamily = BuiltInSynFamily
   { sfMatchFam      :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
+    -- Does this reduce on the given arguments?
+    -- If it does, returns (CoAxiomRule, types to instantiate the rule at, rhs type)
+    -- That is: mkAxiomRuleCo coax (zipWith mkReflCo (coaxrAsmpRoles coax) ts)
+    --              :: F tys ~r rhs,
+    -- where the r in the output is coaxrRole of the rule. It is up to the
+    -- caller to ensure that this role is appropriate.
+
   , sfInteractTop   :: [Type] -> Type -> [TypeEqn]
+    -- If given these type arguments and RHS, returns the equalities that
+    -- are guaranteed to hold.
+
   , sfInteractInert :: [Type] -> Type ->
                        [Type] -> Type -> [TypeEqn]
+    -- If given one set of arguments and result, and another set of arguments
+    -- and result, returns the equalities that are guaranteed to hold.
   }
 
 -- Provides default implementations that do nothing.
diff --git a/compiler/GHC/Core/Coercion/Opt.hs b/compiler/GHC/Core/Coercion/Opt.hs
index 3769fb23be..108154e1c6 100644
--- a/compiler/GHC/Core/Coercion/Opt.hs
+++ b/compiler/GHC/Core/Coercion/Opt.hs
@@ -27,7 +27,6 @@ import GHC.Types.Var.Env
 import GHC.Data.Pair
 import GHC.Data.List.SetOps ( getNth )
 import GHC.Core.Unify
-import GHC.Core.InstEnv
 import Control.Monad   ( zipWithM )
 
 import GHC.Utils.Outputable
@@ -1006,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 instanceBindFun flat lhs_incomp
+      | SurelyApart <- tcUnifyTysFG (const BindMe) 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 c5445fceae..a6c7604008 100644
--- a/compiler/GHC/Core/FamInstEnv.hs
+++ b/compiler/GHC/Core/FamInstEnv.hs
@@ -428,7 +428,8 @@ Here is how we do it:
 apart(target, pattern) = not (unify(flatten(target), pattern))
 
 where flatten (implemented in flattenTys, below) converts all type-family
-applications into fresh variables. (See Note [Flattening] in GHC.Core.Unify.)
+applications into fresh variables. (See
+Note [Flattening type-family applications when matching instances] in GHC.Core.Unify.)
 
 Note [Compatibility]
 ~~~~~~~~~~~~~~~~~~~~
@@ -1141,6 +1142,7 @@ reduceTyFamApp_maybe envs role tc tys
 
   | Just ax           <- isBuiltInSynFamTyCon_maybe tc
   , Just (coax,ts,ty) <- sfMatchFam ax tys
+  , role == coaxrRole coax
   = let co = mkAxiomRuleCo coax (zipWith mkReflCo (coaxrAsmpRoles coax) ts)
     in Just (co, ty)
 
@@ -1175,7 +1177,8 @@ findBranch branches target_tys
                         , cab_incomps = incomps }) = branch
             in_scope = mkInScopeSet (unionVarSets $
                             map (tyCoVarsOfTypes . coAxBranchLHS) incomps)
-            -- See Note [Flattening] in GHC.Core.Unify
+            -- See Note [Flattening type-family applications when matching instances]
+            -- in GHC.Core.Unify
             flattened_target = flattenTys in_scope target_tys
         in case tcMatchTys tpl_lhs target_tys of
         Just subst -- matching worked. now, check for apartness.
@@ -1192,11 +1195,11 @@ findBranch branches target_tys
 -- (POPL '14). This should be used when determining if an equation
 -- ('CoAxBranch') of a closed type family can be used to reduce a certain target
 -- type family application.
-apartnessCheck :: [Type]     -- ^ /flattened/ target arguments. Make sure
-                             -- they're flattened! See Note [Flattening]
-                             -- in GHC.Core.Unify
-                             -- (NB: This "flat" is a different
-                             -- "flat" than is used in GHC.Tc.Solver.Flatten.)
+apartnessCheck :: [Type]
+  -- ^ /flattened/ target arguments. Make sure they're flattened! See
+  -- Note [Flattening type-family applications when matching instances]
+  -- in GHC.Core.Unify. (NB: This "flat" is a different
+ -- "flat" than is used in GHC.Tc.Solver.Flatten.)
                -> CoAxBranch -- ^ the candidate equation we wish to use
                              -- Precondition: this matches the target
                -> Bool       -- ^ True <=> equation can fire
@@ -1316,7 +1319,7 @@ topNormaliseType_maybe env ty
     tyFamStepper :: NormaliseStepper (Coercion, MCoercionN)
     tyFamStepper rec_nts tc tys  -- Try to step a type/data family
       = case topReduceTyFamApp_maybe env tc tys of
-          Just (co, rhs, res_co) -> NS_Step rec_nts rhs (co, MCo res_co)
+          Just (co, rhs, res_co) -> NS_Step rec_nts rhs (co, res_co)
           _                      -> NS_Done
 
 ---------------
@@ -1362,14 +1365,14 @@ normalise_tc_app tc tys
     assemble_result :: Role       -- r, ambient role in NormM monad
                     -> Type       -- nty, result type, possibly of changed kind
                     -> Coercion   -- orig_ty ~r nty, possibly heterogeneous
-                    -> CoercionN  -- typeKind(orig_ty) ~N typeKind(nty)
+                    -> MCoercionN -- typeKind(orig_ty) ~N typeKind(nty)
                     -> (Coercion, Type)   -- (co :: orig_ty ~r nty_casted, nty_casted)
                                           -- where nty_casted has same kind as orig_ty
     assemble_result r nty orig_to_nty kind_co
       = ( final_co, nty_old_kind )
       where
-        nty_old_kind = nty `mkCastTy` mkSymCo kind_co
-        final_co     = mkCoherenceRightCo r nty (mkSymCo kind_co) orig_to_nty
+        nty_old_kind = nty `mkCastTyMCo` mkSymMCo kind_co
+        final_co     = mkCoherenceRightMCo r nty (mkSymMCo kind_co) orig_to_nty
 
 ---------------
 -- | Try to simplify a type-family application, by *one* step
@@ -1378,7 +1381,7 @@ normalise_tc_app tc tys
 --         res_co :: typeKind(F tys) ~ typeKind(rhs)
 -- Type families and data families; always Representational role
 topReduceTyFamApp_maybe :: FamInstEnvs -> TyCon -> [Type]
-                        -> Maybe (Coercion, Type, Coercion)
+                        -> Maybe (Coercion, Type, MCoercion)
 topReduceTyFamApp_maybe envs fam_tc arg_tys
   | isFamilyTyCon fam_tc   -- type families and data families
   , Just (co, rhs) <- reduceTyFamApp_maybe envs role fam_tc ntys
@@ -1391,7 +1394,7 @@ topReduceTyFamApp_maybe envs fam_tc arg_tys
                               normalise_tc_args fam_tc arg_tys
 
 normalise_tc_args :: TyCon -> [Type]             -- tc tys
-                  -> NormM (Coercion, [Type], CoercionN)
+                  -> NormM (Coercion, [Type], MCoercionN)
                   -- (co, new_tys), where
                   -- co :: tc tys ~ tc new_tys; might not be homogeneous
                   -- res_co :: typeKind(tc tys) ~N typeKind(tc new_tys)
@@ -1474,14 +1477,14 @@ normalise_type ty
                     ; role <- getRole
                     ; let nty = mkAppTys nfun nargs
                           nco = mkAppCos fun_co args_cos
-                          nty_casted = nty `mkCastTy` mkSymCo res_co
-                          final_co = mkCoherenceRightCo role nty (mkSymCo res_co) nco
+                          nty_casted = nty `mkCastTyMCo` mkSymMCo res_co
+                          final_co = mkCoherenceRightMCo role nty (mkSymMCo res_co) nco
                     ; return (final_co, nty_casted) } }
 
 normalise_args :: Kind    -- of the function
                -> [Role]  -- roles at which to normalise args
                -> [Type]  -- args
-               -> NormM ([Coercion], [Type], Coercion)
+               -> NormM ([Coercion], [Type], MCoercion)
 -- returns (cos, xis, res_co), where each xi is the normalised
 -- version of the corresponding type, each co is orig_arg ~ xi,
 -- and the res_co :: kind(f orig_args) ~ kind(f xis)
@@ -1491,7 +1494,7 @@ normalise_args :: Kind    -- of the function
 normalise_args fun_ki roles args
   = do { normed_args <- zipWithM normalise1 roles args
        ; let (xis, cos, res_co) = simplifyArgsWorker ki_binders inner_ki fvs roles normed_args
-       ; return (map mkSymCo cos, xis, mkSymCo res_co) }
+       ; return (map mkSymCo cos, xis, mkSymMCo res_co) }
   where
     (ki_binders, inner_ki) = splitPiTys fun_ki
     fvs = tyCoVarsOfTypes args
diff --git a/compiler/GHC/Core/InstEnv.hs b/compiler/GHC/Core/InstEnv.hs
index e8603a4cae..6eae14090f 100644
--- a/compiler/GHC/Core/InstEnv.hs
+++ b/compiler/GHC/Core/InstEnv.hs
@@ -828,18 +828,22 @@ lookupInstEnv' ie vis_mods cls tys
       = find ms us rest
 
       | otherwise
-      = ASSERT2( tyCoVarsOfTypes tys `disjointVarSet` tpl_tv_set,
+      = ASSERT2( tys_tv_set `disjointVarSet` tpl_tv_set,
                  (ppr cls <+> ppr tys <+> ppr all_tvs) $$
                  (ppr tpl_tvs <+> ppr tpl_tys)
                 )
                 -- Unification will break badly if the variables overlap
                 -- They shouldn't because we allocate separate uniques for them
                 -- See Note [Template tyvars are fresh]
-        case tcUnifyTys instanceBindFun tpl_tys tys of
-            Just _   -> find ms (item:us) rest
-            Nothing  -> find ms us        rest
+        case tcUnifyTysFG instanceBindFun tpl_tys tys of
+          -- We consider MaybeApart to be a case where the instance might
+          -- apply in the future. This covers an instance like C Int and
+          -- a target like [W] C (F a), where F is a type family.
+            SurelyApart -> find ms us        rest
+            _           -> find ms (item:us) rest
       where
         tpl_tv_set = mkVarSet tpl_tvs
+        tys_tv_set = tyCoVarsOfTypes tys
 
 ---------------
 -- This is the common way to call this function.
@@ -1023,20 +1027,28 @@ When looking up in the instance environment, or family-instance environment,
 we are careful about multiple matches, as described above in
 Note [Overlapping instances]
 
-The key_tys can contain skolem constants, and we can guarantee that those
+The target tys can contain skolem constants. For existentials and instance variables,
+we can guarantee that those
 are never going to be instantiated to anything, so we should not involve
-them in the unification test.  Example:
+them in the unification test. These are called "super skolems". Example:
         class Foo a where { op :: a -> Int }
         instance Foo a => Foo [a]       -- NB overlap
         instance Foo [Int]              -- NB overlap
         data T = forall a. Foo a => MkT a
         f :: T -> Int
         f (MkT x) = op [x,x]
-The op [x,x] means we need (Foo [a]).  Without the filterVarSet we'd
-complain, saying that the choice of instance depended on the instantiation
-of 'a'; but of course it isn't *going* to be instantiated.
-
-We do this only for isOverlappableTyVar skolems.  For example we reject
+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
+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
+course it isn't *going* to be instantiated. Note that it is necessary that
+the unification algorithm returns SurelyApart for these super-skolems
+for GHC to be able to commit to another instance.
+
+We do this only for super skolems.  For example we reject
         g :: forall a => [a] -> Int
         g x = op x
 on the grounds that the correct instance depends on the instantiation of 'a'
diff --git a/compiler/GHC/Core/Map/Expr.hs b/compiler/GHC/Core/Map/Expr.hs
index b3273a1a2e..2181abb304 100644
--- a/compiler/GHC/Core/Map/Expr.hs
+++ b/compiler/GHC/Core/Map/Expr.hs
@@ -116,6 +116,7 @@ instance TrieMap CoreMap where
     alterTM k f (CoreMap m) = CoreMap (alterTM (deBruijnize k) f m)
     foldTM k (CoreMap m) = foldTM k m
     mapTM f (CoreMap m) = CoreMap (mapTM f m)
+    filterTM f (CoreMap m) = CoreMap (filterTM f m)
 
 -- | @CoreMapG a@ is a map from @DeBruijn CoreExpr@ to @a@.  The extended
 -- key makes it suitable for recursive traversal, since it can track binders,
@@ -197,6 +198,7 @@ instance TrieMap CoreMapX where
    alterTM  = xtE
    foldTM   = fdE
    mapTM    = mapE
+   filterTM = ftE
 
 --------------------------
 mapE :: (a->b) -> CoreMapX a -> CoreMapX b
@@ -213,6 +215,20 @@ mapE f (CM { cm_var = cvar, cm_lit = clit
        , cm_letr = mapTM (mapTM (mapTM f)) cletr, cm_case = mapTM (mapTM f) ccase
        , cm_ecase = mapTM (mapTM f) cecase, cm_tick = mapTM (mapTM f) ctick }
 
+ftE :: (a->Bool) -> CoreMapX a -> CoreMapX a
+ftE f (CM { cm_var = cvar, cm_lit = clit
+          , cm_co = cco, cm_type = ctype
+          , cm_cast = ccast , cm_app = capp
+          , cm_lam = clam, cm_letn = cletn
+          , cm_letr = cletr, cm_case = ccase
+          , cm_ecase = cecase, cm_tick = ctick })
+  = CM { cm_var = filterTM f cvar, cm_lit = filterTM f clit
+       , cm_co = filterTM f cco, cm_type = filterTM f ctype
+       , cm_cast = mapTM (filterTM f) ccast, cm_app = mapTM (filterTM f) capp
+       , cm_lam = mapTM (filterTM f) clam, cm_letn = mapTM (mapTM (filterTM f)) cletn
+       , cm_letr = mapTM (mapTM (filterTM f)) cletr, cm_case = mapTM (filterTM f) ccase
+       , cm_ecase = mapTM (filterTM f) cecase, cm_tick = mapTM (filterTM f) ctick }
+
 --------------------------
 lookupCoreMap :: CoreMap a -> CoreExpr -> Maybe a
 lookupCoreMap cm e = lookupTM e cm
@@ -330,6 +346,7 @@ instance TrieMap AltMap where
    alterTM  = xtA emptyCME
    foldTM   = fdA
    mapTM    = mapA
+   filterTM = ftA
 
 instance Eq (DeBruijn CoreAlt) where
   D env1 a1 == D env2 a2 = go a1 a2 where
@@ -348,6 +365,12 @@ mapA f (AM { am_deflt = adeflt, am_data = adata, am_lit = alit })
        , am_data = mapTM (mapTM f) adata
        , am_lit = mapTM (mapTM f) alit }
 
+ftA :: (a->Bool) -> AltMap a -> AltMap a
+ftA f (AM { am_deflt = adeflt, am_data = adata, am_lit = alit })
+  = AM { am_deflt = filterTM f adeflt
+       , am_data = mapTM (filterTM f) adata
+       , am_lit = mapTM (filterTM f) alit }
+
 lkA :: CmEnv -> CoreAlt -> AltMap a -> Maybe a
 lkA env (DEFAULT,    _, rhs)  = am_deflt >.> lkG (D env rhs)
 lkA env (LitAlt lit, _, rhs)  = am_lit >.> lookupTM lit >=> lkG (D env rhs)
diff --git a/compiler/GHC/Core/Map/Type.hs b/compiler/GHC/Core/Map/Type.hs
index 36583dc670..8056211314 100644
--- a/compiler/GHC/Core/Map/Type.hs
+++ b/compiler/GHC/Core/Map/Type.hs
@@ -8,6 +8,9 @@
 {-# LANGUAGE TypeFamilies #-}
 
 module GHC.Core.Map.Type (
+     -- * Re-export generic interface
+   TrieMap(..),
+
      -- * Maps over 'Type's
    TypeMap, emptyTypeMap, extendTypeMap, lookupTypeMap, foldTypeMap,
    LooseTypeMap,
@@ -45,6 +48,7 @@ import GHC.Types.Var.Env
 import GHC.Types.Unique.FM
 import GHC.Utils.Outputable
 
+import GHC.Data.Maybe
 import GHC.Utils.Panic
 
 import qualified Data.Map    as Map
@@ -86,6 +90,7 @@ instance TrieMap CoercionMap where
    alterTM k f (CoercionMap m) = CoercionMap (alterTM (deBruijnize k) f m)
    foldTM k    (CoercionMap m) = foldTM k m
    mapTM f     (CoercionMap m) = CoercionMap (mapTM f m)
+   filterTM f  (CoercionMap m) = CoercionMap (filterTM f m)
 
 type CoercionMapG = GenMap CoercionMapX
 newtype CoercionMapX a = CoercionMapX (TypeMapX a)
@@ -97,6 +102,7 @@ instance TrieMap CoercionMapX where
   alterTM  = xtC
   foldTM f (CoercionMapX core_tm) = foldTM f core_tm
   mapTM f (CoercionMapX core_tm)  = CoercionMapX (mapTM f core_tm)
+  filterTM f (CoercionMapX core_tm) = CoercionMapX (filterTM f core_tm)
 
 instance Eq (DeBruijn Coercion) where
   D env1 co1 == D env2 co2
@@ -135,6 +141,12 @@ data TypeMapX a
   = TM { tm_var    :: VarMap a
        , tm_app    :: TypeMapG (TypeMapG a)
        , tm_tycon  :: DNameEnv a
+
+         -- only InvisArg arrows here
+       , tm_funty  :: TypeMapG (TypeMapG (TypeMapG a))
+                       -- keyed on the argument, result rep, and result
+                       -- constraints are never linear-restricted and are always lifted
+
        , tm_forall :: TypeMapG (BndrMap a) -- See Note [Binders] in GHC.Core.Map.Expr
        , tm_tylit  :: TyLitMap a
        , tm_coerce :: Maybe a
@@ -142,10 +154,12 @@ data TypeMapX a
     -- Note that there is no tyconapp case; see Note [Equality on AppTys] in GHC.Core.Type
 
 -- | Squeeze out any synonyms, and change TyConApps to nested AppTys. Why the
--- last one? See Note [Equality on AppTys] in "GHC.Core.Type"
+-- last one? See Note [Equality on AppTys] in GHC.Core.Type
 --
 -- Note, however, that we keep Constraint and Type apart here, despite the fact
 -- that they are both synonyms of TYPE 'LiftedRep (see #11715).
+--
+-- We also keep (Eq a => a) as a FunTy, distinct from ((->) (Eq a) a).
 trieMapView :: Type -> Maybe Type
 trieMapView ty
   -- First check for TyConApps that need to be expanded to
@@ -164,6 +178,7 @@ instance TrieMap TypeMapX where
    alterTM  = xtT
    foldTM   = fdT
    mapTM    = mapT
+   filterTM = filterT
 
 instance Eq (DeBruijn Type) where
   env_t@(D env t) == env_t'@(D env' t')
@@ -184,8 +199,11 @@ instance Eq (DeBruijn Type) where
             -> D env t1 == D env' t1' && D env t2 == D env' t2'
         (s, AppTy t1' t2') | Just (t1, t2) <- repSplitAppTy_maybe s
             -> D env t1 == D env' t1' && D env t2 == D env' t2'
-        (FunTy _ w1 t1 t2, FunTy _ w1' t1' t2')
-            -> D env w1 == D env w1' && D env t1 == D env' t1' && D env t2 == D env' t2'
+        (FunTy v1 w1 t1 t2, FunTy v1' w1' t1' t2')
+            -> v1 == v1' &&
+               D env w1 == D env w1' &&
+               D env t1 == D env' t1' &&
+               D env t2 == D env' t2'
         (TyConApp tc tys, TyConApp tc' tys')
             -> tc == tc' && D env tys == D env' tys'
         (LitTy l, LitTy l')
@@ -205,17 +223,19 @@ emptyT :: TypeMapX a
 emptyT = TM { tm_var  = emptyTM
             , tm_app  = emptyTM
             , tm_tycon  = emptyDNameEnv
+            , tm_funty  = emptyTM
             , tm_forall = emptyTM
             , tm_tylit  = emptyTyLitMap
             , tm_coerce = Nothing }
 
 mapT :: (a->b) -> TypeMapX a -> TypeMapX b
 mapT f (TM { tm_var  = tvar, tm_app = tapp, tm_tycon = ttycon
-           , tm_forall = tforall, tm_tylit = tlit
+           , tm_funty = tfunty, tm_forall = tforall, tm_tylit = tlit
            , tm_coerce = tcoerce })
   = TM { tm_var    = mapTM f tvar
        , tm_app    = mapTM (mapTM f) tapp
        , tm_tycon  = mapTM f ttycon
+       , tm_funty  = mapTM (mapTM (mapTM f)) tfunty
        , tm_forall = mapTM (mapTM f) tforall
        , tm_tylit  = mapTM f tlit
        , tm_coerce = fmap f tcoerce }
@@ -233,6 +253,11 @@ lkT (D env ty) m = go ty m
     go (LitTy l)                   = tm_tylit  >.> lkTyLit l
     go (ForAllTy (Bndr tv _) ty)   = tm_forall >.> lkG (D (extendCME env tv) ty)
                                                >=> lkBndr env tv
+    go (FunTy InvisArg _ arg res)
+      | Just res_rep <- getRuntimeRep_maybe res
+                                   = tm_funty >.> lkG (D env arg)
+                                              >=> lkG (D env res_rep)
+                                              >=> lkG (D env res)
     go ty@(FunTy {})               = pprPanic "lkT FunTy" (ppr ty)
     go (CastTy t _)                = go t
     go (CoercionTy {})             = tm_coerce
@@ -245,6 +270,10 @@ xtT (D env (TyVarTy v))       f m = m { tm_var    = tm_var m |> xtVar env v f }
 xtT (D env (AppTy t1 t2))     f m = m { tm_app    = tm_app m |> xtG (D env t1)
                                                             |>> xtG (D env t2) f }
 xtT (D _   (TyConApp tc []))  f m = m { tm_tycon  = tm_tycon m |> xtDNamed tc f }
+xtT (D env (FunTy InvisArg _ t1 t2)) f m = m { tm_funty = tm_funty m |> xtG (D env t1)
+                                                                    |>> xtG (D env t2_rep)
+                                                                    |>> xtG (D env t2) f }
+  where t2_rep = expectJust "xtT FunTy InvisArg" (getRuntimeRep_maybe t2)
 xtT (D _   (LitTy l))         f m = m { tm_tylit  = tm_tylit m |> xtTyLit l f }
 xtT (D env (CastTy t _))      f m = xtT (D env t) f m
 xtT (D _   (CoercionTy {}))   f m = m { tm_coerce = tm_coerce m |> f }
@@ -258,10 +287,23 @@ fdT :: (a -> b -> b) -> TypeMapX a -> b -> b
 fdT k m = foldTM k (tm_var m)
         . foldTM (foldTM k) (tm_app m)
         . foldTM k (tm_tycon m)
+        . foldTM (foldTM (foldTM k)) (tm_funty m)
         . foldTM (foldTM k) (tm_forall m)
         . foldTyLit k (tm_tylit m)
         . foldMaybe k (tm_coerce m)
 
+filterT :: (a -> Bool) -> TypeMapX a -> TypeMapX a
+filterT f (TM { tm_var  = tvar, tm_app = tapp, tm_tycon = ttycon
+              , tm_funty = tfunty, tm_forall = tforall, tm_tylit = tlit
+              , tm_coerce = tcoerce })
+  = TM { tm_var    = filterTM f tvar
+       , tm_app    = mapTM (filterTM f) tapp
+       , tm_tycon  = filterTM f ttycon
+       , tm_funty  = mapTM (mapTM (filterTM f)) tfunty
+       , tm_forall = mapTM (filterTM f) tforall
+       , tm_tylit  = filterTM f tlit
+       , tm_coerce = filterMaybe f tcoerce }
+
 ------------------------
 data TyLitMap a = TLM { tlm_number :: Map.Map Integer a
                       , tlm_string :: UniqFM  FastString a
@@ -274,6 +316,7 @@ instance TrieMap TyLitMap where
    alterTM  = xtTyLit
    foldTM   = foldTyLit
    mapTM    = mapTyLit
+   filterTM = filterTyLit
 
 emptyTyLitMap :: TyLitMap a
 emptyTyLitMap = TLM { tlm_number = Map.empty, tlm_string = emptyUFM }
@@ -298,6 +341,10 @@ foldTyLit :: (a -> b -> b) -> TyLitMap a -> b -> b
 foldTyLit l m = flip (foldUFM l) (tlm_string m)
               . flip (Map.foldr l)   (tlm_number m)
 
+filterTyLit :: (a -> Bool) -> TyLitMap a -> TyLitMap a
+filterTyLit f (TLM { tlm_number = tn, tlm_string = ts })
+  = TLM { tlm_number = Map.filter f tn, tlm_string = filterUFM f ts }
+
 -------------------------------------------------
 -- | @TypeMap a@ is a map from 'Type' to @a@.  If you are a client, this
 -- is the type you want. The keys in this map may have different kinds.
@@ -321,6 +368,7 @@ instance TrieMap TypeMap where
     alterTM k f m = xtTT (deBruijnize k) f m
     foldTM k (TypeMap m) = foldTM (foldTM k) m
     mapTM f (TypeMap m) = TypeMap (mapTM (mapTM f) m)
+    filterTM f (TypeMap m) = TypeMap (mapTM (filterTM f) m)
 
 foldTypeMap :: (a -> b -> b) -> b -> TypeMap a -> b
 foldTypeMap k z m = foldTM k m z
@@ -361,6 +409,7 @@ instance TrieMap LooseTypeMap where
   alterTM k f (LooseTypeMap m) = LooseTypeMap (alterTM (deBruijnize k) f m)
   foldTM f (LooseTypeMap m) = foldTM f m
   mapTM f (LooseTypeMap m) = LooseTypeMap (mapTM f m)
+  filterTM f (LooseTypeMap m) = LooseTypeMap (filterTM f m)
 
 {-
 ************************************************************************
@@ -435,6 +484,7 @@ instance TrieMap BndrMap where
    alterTM  = xtBndr emptyCME
    foldTM   = fdBndrMap
    mapTM    = mapBndrMap
+   filterTM = ftBndrMap
 
 mapBndrMap :: (a -> b) -> BndrMap a -> BndrMap b
 mapBndrMap f (BndrMap tm) = BndrMap (mapTM (mapTM f) tm)
@@ -456,6 +506,8 @@ xtBndr :: forall a . CmEnv -> Var -> XT a -> BndrMap a -> BndrMap a
 xtBndr env v xt (BndrMap tymap)  =
   BndrMap (tymap |> xtG (D env (varType v)) |>> (alterTM (D env <$> varMultMaybe v) xt))
 
+ftBndrMap :: (a -> Bool) -> BndrMap a -> BndrMap a
+ftBndrMap f (BndrMap tm) = BndrMap (mapTM (filterTM f) tm)
 
 --------- Variable occurrence -------------
 data VarMap a = VM { vm_bvar   :: BoundVarMap a  -- Bound variable
@@ -468,6 +520,7 @@ instance TrieMap VarMap where
    alterTM  = xtVar emptyCME
    foldTM   = fdVar
    mapTM    = mapVar
+   filterTM = ftVar
 
 mapVar :: (a->b) -> VarMap a -> VarMap b
 mapVar f (VM { vm_bvar = bv, vm_fvar = fv })
@@ -493,6 +546,10 @@ lkDFreeVar var env = lookupDVarEnv env var
 xtDFreeVar :: Var -> XT a -> DVarEnv a -> DVarEnv a
 xtDFreeVar v f m = alterDVarEnv f m v
 
+ftVar :: (a -> Bool) -> VarMap a -> VarMap a
+ftVar f (VM { vm_bvar = bv, vm_fvar = fv })
+  = VM { vm_bvar = filterTM f bv, vm_fvar = filterTM f fv }
+
 -------------------------------------------------
 lkDNamed :: NamedThing n => n -> DNameEnv a -> Maybe a
 lkDNamed n env = lookupDNameEnv env (getName n)
diff --git a/compiler/GHC/Core/TyCo/FVs.hs b/compiler/GHC/Core/TyCo/FVs.hs
index dadb82c5f5..8277b06378 100644
--- a/compiler/GHC/Core/TyCo/FVs.hs
+++ b/compiler/GHC/Core/TyCo/FVs.hs
@@ -26,7 +26,8 @@ module GHC.Core.TyCo.FVs
         injectiveVarsOfType, injectiveVarsOfTypes,
         invisibleVarsOfType, invisibleVarsOfTypes,
 
-        -- No Free vars
+        -- Any and No Free vars
+        anyFreeVarsOfType, anyFreeVarsOfTypes, anyFreeVarsOfCo,
         noFreeVarsOfType, noFreeVarsOfTypes, noFreeVarsOfCo,
 
         -- * Well-scoped free variables
@@ -47,7 +48,7 @@ import GHC.Prelude
 
 import {-# SOURCE #-} GHC.Core.Type (coreView, partitionInvisibleTypes)
 
-import Data.Monoid as DM ( Endo(..), All(..) )
+import Data.Monoid as DM ( Endo(..), Any(..) )
 import GHC.Core.TyCo.Rep
 import GHC.Core.TyCon
 import GHC.Types.Var
@@ -855,32 +856,43 @@ invisibleVarsOfTypes = mapUnionFV invisibleVarsOfType
 
 {- *********************************************************************
 *                                                                      *
-                 No free vars
+                 Any free vars
 *                                                                      *
 ********************************************************************* -}
 
-nfvFolder :: TyCoFolder TyCoVarSet DM.All
-nfvFolder = TyCoFolder { tcf_view = noView
-                       , tcf_tyvar = do_tcv, tcf_covar = do_tcv
-                       , tcf_hole = do_hole, tcf_tycobinder = do_bndr }
+{-# INLINE afvFolder #-}   -- so that specialization to (const True) works
+afvFolder :: (TyCoVar -> Bool) -> TyCoFolder TyCoVarSet DM.Any
+afvFolder check_fv = TyCoFolder { tcf_view = noView
+                                , tcf_tyvar = do_tcv, tcf_covar = do_tcv
+                                , tcf_hole = do_hole, tcf_tycobinder = do_bndr }
   where
-    do_tcv is tv = All (tv `elemVarSet` is)
-    do_hole _ _  = All True    -- I'm unsure; probably never happens
+    do_tcv is tv = Any (not (tv `elemVarSet` is) && check_fv tv)
+    do_hole _ _  = Any False    -- I'm unsure; probably never happens
     do_bndr is tv _ = is `extendVarSet` tv
 
-nfv_ty  :: Type       -> DM.All
-nfv_tys :: [Type]     -> DM.All
-nfv_co  :: Coercion   -> DM.All
-(nfv_ty, nfv_tys, nfv_co, _) = foldTyCo nfvFolder emptyVarSet
+anyFreeVarsOfType :: (TyCoVar -> Bool) -> Type -> Bool
+anyFreeVarsOfType check_fv ty = DM.getAny (f ty)
+  where (f, _, _, _) = foldTyCo (afvFolder check_fv) emptyVarSet
+
+anyFreeVarsOfTypes :: (TyCoVar -> Bool) -> [Type] -> Bool
+anyFreeVarsOfTypes check_fv tys = DM.getAny (f tys)
+  where (_, f, _, _) = foldTyCo (afvFolder check_fv) emptyVarSet
+
+anyFreeVarsOfCo :: (TyCoVar -> Bool) -> Coercion -> Bool
+anyFreeVarsOfCo check_fv co = DM.getAny (f co)
+  where (_, _, f, _) = foldTyCo (afvFolder check_fv) emptyVarSet
 
 noFreeVarsOfType :: Type -> Bool
-noFreeVarsOfType ty = DM.getAll (nfv_ty ty)
+noFreeVarsOfType ty = not $ DM.getAny (f ty)
+  where (f, _, _, _) = foldTyCo (afvFolder (const True)) emptyVarSet
 
 noFreeVarsOfTypes :: [Type] -> Bool
-noFreeVarsOfTypes tys = DM.getAll (nfv_tys tys)
+noFreeVarsOfTypes tys = not $ DM.getAny (f tys)
+  where (_, f, _, _) = foldTyCo (afvFolder (const True)) emptyVarSet
 
 noFreeVarsOfCo :: Coercion -> Bool
-noFreeVarsOfCo co = getAll (nfv_co co)
+noFreeVarsOfCo co = not $ DM.getAny (f co)
+  where (_, _, f, _) = foldTyCo (afvFolder (const True)) emptyVarSet
 
 
 {- *********************************************************************
@@ -983,4 +995,3 @@ tyCoVarsOfTypeWellScoped = scopedSort . tyCoVarsOfTypeList
 -- | Get the free vars of types in scoped order
 tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar]
 tyCoVarsOfTypesWellScoped = scopedSort . tyCoVarsOfTypesList
-
diff --git a/compiler/GHC/Core/TyCo/Rep.hs b/compiler/GHC/Core/TyCo/Rep.hs
index 1e8fcda0ca..0be6824b9d 100644
--- a/compiler/GHC/Core/TyCo/Rep.hs
+++ b/compiler/GHC/Core/TyCo/Rep.hs
@@ -37,7 +37,7 @@ module GHC.Core.TyCo.Rep (
         -- * Coercions
         Coercion(..),
         UnivCoProvenance(..),
-        CoercionHole(..), BlockSubstFlag(..), coHoleCoVar, setCoHoleCoVar,
+        CoercionHole(..), coHoleCoVar, setCoHoleCoVar,
         CoercionN, CoercionR, CoercionP, KindCoercion,
         MCoercion(..), MCoercionR, MCoercionN,
 
@@ -93,7 +93,7 @@ import GHC.Core.Coercion.Axiom
 import GHC.Builtin.Names ( liftedTypeKindTyConKey, manyDataConKey )
 import {-# SOURCE #-} GHC.Builtin.Types ( liftedTypeKindTyCon, manyDataConTy )
 import GHC.Types.Basic ( LeftOrRight(..), pickLR )
-import GHC.Types.Unique ( hasKey )
+import GHC.Types.Unique ( hasKey, Uniquable(..) )
 import GHC.Utils.Outputable
 import GHC.Data.FastString
 import GHC.Utils.Misc
@@ -1588,15 +1588,9 @@ data CoercionHole
   = CoercionHole { ch_co_var  :: CoVar
                        -- See Note [CoercionHoles and coercion free variables]
 
-                 , ch_blocker :: BlockSubstFlag  -- should this hole block substitution?
-                                                 -- See (2a) in TcCanonical
-                                                 -- Note [Equalities with incompatible kinds]
                  , ch_ref     :: IORef (Maybe Coercion)
                  }
 
-data BlockSubstFlag = YesBlockSubst
-                    | NoBlockSubst
-
 coHoleCoVar :: CoercionHole -> CoVar
 coHoleCoVar = ch_co_var
 
@@ -1612,9 +1606,8 @@ instance Data.Data CoercionHole where
 instance Outputable CoercionHole where
   ppr (CoercionHole { ch_co_var = cv }) = braces (ppr cv)
 
-instance Outputable BlockSubstFlag where
-  ppr YesBlockSubst = text "YesBlockSubst"
-  ppr NoBlockSubst  = text "NoBlockSubst"
+instance Uniquable CoercionHole where
+  getUnique (CoercionHole { ch_co_var = cv }) = getUnique cv
 
 {- Note [Phantom coercions]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/GHC/Core/TyCon.hs b/compiler/GHC/Core/TyCon.hs
index b82dd5cb26..198b66959b 100644
--- a/compiler/GHC/Core/TyCon.hs
+++ b/compiler/GHC/Core/TyCon.hs
@@ -56,7 +56,7 @@ module GHC.Core.TyCon(
         mustBeSaturated,
         isPromotedDataCon, isPromotedDataCon_maybe,
         isKindTyCon, isLiftedTypeKindTyConName,
-        isTauTyCon, isFamFreeTyCon,
+        isTauTyCon, isFamFreeTyCon, isForgetfulSynTyCon,
 
         isDataTyCon, isProductTyCon, isDataProductTyCon_maybe,
         isDataSumTyCon_maybe,
@@ -817,10 +817,15 @@ data TyCon
         synIsTau     :: Bool,   -- True <=> the RHS of this synonym does not
                                  --          have any foralls, after expanding any
                                  --          nested synonyms
-        synIsFamFree  :: Bool    -- True <=> the RHS of this synonym does not mention
+        synIsFamFree  :: Bool,   -- True <=> the RHS of this synonym does not mention
                                  --          any type synonym families (data families
                                  --          are fine), again after expanding any
                                  --          nested synonyms
+        synIsForgetful :: Bool   -- True <=  at least one argument is not mentioned
+                                 --          in the RHS (or is mentioned only under
+                                 --          forgetful synonyms)
+                                 -- Test is conservative, so True does not guarantee
+                                 -- forgetfulness.
     }
 
   -- | Represents families (both type and data)
@@ -1779,20 +1784,21 @@ mkPrimTyCon' name binders res_kind roles is_unlifted rep_nm
 
 -- | Create a type synonym 'TyCon'
 mkSynonymTyCon :: Name -> [TyConBinder] -> Kind   -- ^ /result/ kind
-               -> [Role] -> Type -> Bool -> Bool -> TyCon
-mkSynonymTyCon name binders res_kind roles rhs is_tau is_fam_free
+               -> [Role] -> Type -> Bool -> Bool -> Bool -> TyCon
+mkSynonymTyCon name binders res_kind roles rhs is_tau is_fam_free is_forgetful
   = SynonymTyCon {
-        tyConName    = name,
-        tyConUnique  = nameUnique name,
-        tyConBinders = binders,
-        tyConResKind = res_kind,
-        tyConKind    = mkTyConKind binders res_kind,
-        tyConArity   = length binders,
-        tyConTyVars  = binderVars binders,
-        tcRoles      = roles,
-        synTcRhs     = rhs,
-        synIsTau     = is_tau,
-        synIsFamFree = is_fam_free
+        tyConName      = name,
+        tyConUnique    = nameUnique name,
+        tyConBinders   = binders,
+        tyConResKind   = res_kind,
+        tyConKind      = mkTyConKind binders res_kind,
+        tyConArity     = length binders,
+        tyConTyVars    = binderVars binders,
+        tcRoles        = roles,
+        synTcRhs       = rhs,
+        synIsTau       = is_tau,
+        synIsFamFree   = is_fam_free,
+        synIsForgetful = is_forgetful
     }
 
 -- | Create a type family 'TyCon'
@@ -2046,11 +2052,22 @@ isTauTyCon :: TyCon -> Bool
 isTauTyCon (SynonymTyCon { synIsTau = is_tau }) = is_tau
 isTauTyCon _                                    = True
 
+-- | Is this tycon neither a type family nor a synonym that expands
+-- to a type family?
 isFamFreeTyCon :: TyCon -> Bool
 isFamFreeTyCon (SynonymTyCon { synIsFamFree = fam_free }) = fam_free
 isFamFreeTyCon (FamilyTyCon { famTcFlav = flav })         = isDataFamFlav flav
 isFamFreeTyCon _                                          = True
 
+-- | Is this a forgetful type synonym? If this is a type synonym whose
+-- RHS does not mention one (or more) of its bound variables, returns
+-- True. Thus, False means that all bound variables appear on the RHS;
+-- True may not mean anything, as the test to set this flag is
+-- conservative.
+isForgetfulSynTyCon :: TyCon -> Bool
+isForgetfulSynTyCon (SynonymTyCon { synIsForgetful = forget }) = forget
+isForgetfulSynTyCon _                                          = False
+
 -- As for newtypes, it is in some contexts important to distinguish between
 -- closed synonyms and synonym families, as synonym families have no unique
 -- right hand side to which a synonym family application can expand.
@@ -2118,7 +2135,7 @@ isClosedSynFamilyTyConWithAxiom_maybe
   (FamilyTyCon {famTcFlav = ClosedSynFamilyTyCon mb}) = mb
 isClosedSynFamilyTyConWithAxiom_maybe _               = Nothing
 
--- | @'tyConInjectivityInfo' tc@ returns @'Injective' is@ is @tc@ is an
+-- | @'tyConInjectivityInfo' tc@ returns @'Injective' is@ if @tc@ is an
 -- injective tycon (where @is@ states for which 'tyConBinders' @tc@ is
 -- injective), or 'NotInjective' otherwise.
 tyConInjectivityInfo :: TyCon -> Injectivity
diff --git a/compiler/GHC/Core/TyCon/Env.hs b/compiler/GHC/Core/TyCon/Env.hs
index 76edb829fd..d5947a2fda 100644
--- a/compiler/GHC/Core/TyCon/Env.hs
+++ b/compiler/GHC/Core/TyCon/Env.hs
@@ -26,11 +26,11 @@ module GHC.Core.TyCon.Env (
 
         DTyConEnv,
 
-        emptyDTyConEnv,
+        emptyDTyConEnv, isEmptyDTyConEnv,
         lookupDTyConEnv,
         delFromDTyConEnv, filterDTyConEnv,
-        mapDTyConEnv,
-        adjustDTyConEnv, alterDTyConEnv, extendDTyConEnv,
+        mapDTyConEnv, mapMaybeDTyConEnv,
+        adjustDTyConEnv, alterDTyConEnv, extendDTyConEnv, foldDTyConEnv
     ) where
 
 #include "HsVersions.h"
@@ -116,6 +116,9 @@ type DTyConEnv a = UniqDFM TyCon a
 emptyDTyConEnv :: DTyConEnv a
 emptyDTyConEnv = emptyUDFM
 
+isEmptyDTyConEnv :: DTyConEnv a -> Bool
+isEmptyDTyConEnv = isNullUDFM
+
 lookupDTyConEnv :: DTyConEnv a -> TyCon -> Maybe a
 lookupDTyConEnv = lookupUDFM
 
@@ -128,6 +131,9 @@ filterDTyConEnv = filterUDFM
 mapDTyConEnv :: (a -> b) -> DTyConEnv a -> DTyConEnv b
 mapDTyConEnv = mapUDFM
 
+mapMaybeDTyConEnv :: (a -> Maybe b) -> DTyConEnv a -> DTyConEnv b
+mapMaybeDTyConEnv = mapMaybeUDFM
+
 adjustDTyConEnv :: (a -> a) -> DTyConEnv a -> TyCon -> DTyConEnv a
 adjustDTyConEnv = adjustUDFM
 
@@ -136,3 +142,6 @@ alterDTyConEnv = alterUDFM
 
 extendDTyConEnv :: DTyConEnv a -> TyCon -> a -> DTyConEnv a
 extendDTyConEnv = addToUDFM
+
+foldDTyConEnv :: (elt -> a -> a) -> a -> DTyConEnv elt -> a
+foldDTyConEnv = foldUDFM
diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index b983671d11..3164e2626b 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -29,7 +29,7 @@ module GHC.Core.Type (
         mkAppTy, mkAppTys, splitAppTy, splitAppTys, repSplitAppTys,
         splitAppTy_maybe, repSplitAppTy_maybe, tcRepSplitAppTy_maybe,
 
-        mkVisFunTy, mkInvisFunTy,
+        mkFunTy, mkVisFunTy, mkInvisFunTy,
         mkVisFunTys,
         mkVisFunTyMany, mkInvisFunTyMany,
         mkVisFunTysMany, mkInvisFunTysMany,
@@ -155,6 +155,7 @@ module GHC.Core.Type (
         coVarsOfType,
         coVarsOfTypes,
 
+        anyFreeVarsOfType, anyFreeVarsOfTypes,
         noFreeVarsOfType,
         splitVisVarsOfType, splitVisVarsOfTypes,
         expandTypeSynonyms,
@@ -1343,11 +1344,19 @@ splitTyConApp_maybe = repSplitTyConApp_maybe . coreFullView
 -- of @a@ isn't of the form @TYPE rep@). Consequently, you may need to zonk your
 -- type before using this function.
 --
+-- This does *not* split types headed with (=>), as that's not a TyCon in the
+-- type-checker.
+--
 -- If you only need the 'TyCon', consider using 'tcTyConAppTyCon_maybe'.
 tcSplitTyConApp_maybe :: HasCallStack => Type -> Maybe (TyCon, [Type])
 -- Defined here to avoid module loops between Unify and TcType.
 tcSplitTyConApp_maybe ty | Just ty' <- tcView ty = tcSplitTyConApp_maybe ty'
-tcSplitTyConApp_maybe ty                         = repSplitTyConApp_maybe ty
+tcSplitTyConApp_maybe (TyConApp tc tys)          = Just (tc, tys)
+tcSplitTyConApp_maybe (FunTy VisArg w arg res)
+  | Just arg_rep <- getRuntimeRep_maybe arg
+  , Just res_rep <- getRuntimeRep_maybe res
+  = Just (funTyCon, [w, arg_rep, res_rep, arg, res])
+tcSplitTyConApp_maybe _ = Nothing
 
 -------------------
 repSplitTyConApp_maybe :: HasDebugCallStack => Type -> Maybe (TyCon, [Type])
@@ -1358,7 +1367,7 @@ repSplitTyConApp_maybe :: HasDebugCallStack => Type -> Maybe (TyCon, [Type])
 -- have enough info to extract the runtime-rep arguments that
 -- the funTyCon requires.  This will usually be true;
 -- but may be temporarily false during canonicalization:
---     see Note [FunTy and decomposing tycon applications] in "GHC.Tc.Solver.Canonical"
+--     see Note [Decomposing FunTy] in GHC.Tc.Solver.Canonical
 --
 repSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
 repSplitTyConApp_maybe (FunTy _ w arg res)
@@ -1966,13 +1975,17 @@ isCoVarType ty
 
 buildSynTyCon :: Name -> [KnotTied TyConBinder] -> Kind   -- ^ /result/ kind
               -> [Role] -> KnotTied Type -> TyCon
--- This function is here beucase here is where we have
+-- This function is here because here is where we have
 --   isFamFree and isTauTy
 buildSynTyCon name binders res_kind roles rhs
-  = mkSynonymTyCon name binders res_kind roles rhs is_tau is_fam_free
+  = mkSynonymTyCon name binders res_kind roles rhs is_tau is_fam_free is_forgetful
   where
-    is_tau      = isTauTy rhs
-    is_fam_free = isFamFreeTy rhs
+    is_tau       = isTauTy rhs
+    is_fam_free  = isFamFreeTy rhs
+    is_forgetful = any (not . (`elemVarSet` tyCoVarsOfType rhs) . binderVar) binders ||
+                   uniqSetAny isForgetfulSynTyCon (tyConsOfType rhs)
+         -- NB: This is allowed to be conservative, returning True more often
+         -- than it should. See comments on GHC.Core.TyCon.isForgetfulSynTyCon
 
 {-
 ************************************************************************
diff --git a/compiler/GHC/Core/Unify.hs b/compiler/GHC/Core/Unify.hs
index c99913d3be..a8f75535ab 100644
--- a/compiler/GHC/Core/Unify.hs
+++ b/compiler/GHC/Core/Unify.hs
@@ -24,7 +24,7 @@ module GHC.Core.Unify (
         liftCoMatch,
 
         -- The core flattening algorithm
-        flattenTys
+        flattenTys, flattenTysX
    ) where
 
 #include "HsVersions.h"
@@ -363,12 +363,6 @@ types are apart. This has practical consequences for the ability for closed
 type family applications to reduce. See test case
 indexed-types/should_compile/Overlap14.
 
-Note [Unification with skolems]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-If we discover that two types unify if and only if a skolem variable is
-substituted, we can't properly unify the types. But, that skolem variable
-may later be instantiated with a unifyable type. So, we return maybeApart
-in these cases.
 -}
 
 -- | Simple unification of two types; all type variables are bindable
@@ -699,8 +693,9 @@ unifier It does /not/ work up to ~.
 The algorithm implemented here is rather delicate, and we depend on it
 to uphold certain properties. This is a summary of these required
 properties. Any reference to "flattening" refers to the flattening
-algorithm in GHC.Core.FamInstEnv (See Note [Flattening] in GHC.Core.Unify), not
-the flattening algorithm in the solver.
+algorithm in GHC.Core.Unify (See
+Note [Flattening type-family applications when matching instances] in GHC.Core.Unify),
+not the flattening algorithm in the solver.
 
 Notation:
  θ,φ    substitutions
@@ -983,9 +978,11 @@ unify_ty env ty1 (TyVarTy tv2) kco
   = uVar (umSwapRn env) tv2 ty1 (mkSymCo kco)
 
 unify_ty env ty1 ty2 _kco
+ -- NB: This keeps Constraint and Type distinct, as it should for use in the
+ -- type-checker.
   | Just (tc1, tys1) <- mb_tc_app1
   , Just (tc2, tys2) <- mb_tc_app2
-  , tc1 == tc2 || (tcIsLiftedTypeKind ty1 && tcIsLiftedTypeKind ty2)
+  , tc1 == tc2
   = if isInjectiveTyCon tc1 Nominal
     then unify_tys env tys1 tys2
     else do { let inj | isTypeFamilyTyCon tc1
@@ -1034,6 +1031,16 @@ unify_ty env ty1 (AppTy ty2a ty2b) _kco
   | Just (ty1a, ty1b) <- tcRepSplitAppTy_maybe ty1
   = unify_ty_app env ty1a [ty1b] ty2a [ty2b]
 
+  -- tcSplitTyConApp won't split a (=>), so we handle this separately.
+unify_ty env (FunTy InvisArg _w1 arg1 res1) (FunTy InvisArg _w2 arg2 res2) _kco
+   -- Look at result representations, but arg representations would be redundant
+   -- as anything that can appear to the left of => is lifted.
+   -- And anything that can appear to the left of => is unrestricted, so skip the
+   -- multiplicities.
+  | Just res_rep1 <- getRuntimeRep_maybe res1
+  , Just res_rep2 <- getRuntimeRep_maybe res2
+  = unify_tys env [res_rep1, arg1, res1] [res_rep2, arg2, res2]
+
 unify_ty _ (LitTy x) (LitTy y) _kco | x == y = return ()
 
 unify_ty env (ForAllTy (Bndr tv1 _) ty1) (ForAllTy (Bndr tv2 _) ty2) kco
@@ -1163,12 +1170,12 @@ uUnrefined env tv1' ty2 ty2' kco
              -- How could this happen? If we're only matching and if
              -- we're comparing forall-bound variables.
 
-           _ -> maybeApart -- See Note [Unification with skolems]
+           _ -> surelyApart
   }}}}
 
 uUnrefined env tv1' ty2 _ kco -- ty2 is not a type variable
   = case tvBindFlag env tv1' of
-      Skolem -> maybeApart  -- See Note [Unification with skolems]
+      Skolem -> surelyApart
       BindMe -> bindTv env tv1' (ty2 `mkCastTy` mkSymCo kco)
 
 bindTv :: UMEnv -> OutTyVar -> Type -> UM ()
@@ -1211,6 +1218,9 @@ data BindFlag
 
   | 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.
   deriving Eq
 
 {-
@@ -1616,8 +1626,8 @@ pushRefl co =
 *                                                                      *
 ************************************************************************
 
-Note [Flattening]
-~~~~~~~~~~~~~~~~~
+Note [Flattening type-family applications when matching instances]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 As described in "Closed type families with overlapping equations"
 http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-extended.pdf
 we need to flatten core types before unifying them, when checking for "surely-apart"
@@ -1646,6 +1656,15 @@ can see that (F x x) can reduce to Double. So, it had better be the
 case that (F blah blah) can reduce to Double, no matter what (blah)
 is!  Flattening as done below ensures this.
 
+We also use this flattening operation to check for class instances.
+If we have
+  instance C (Maybe b)
+  instance {-# OVERLAPPING #-} C (Maybe Bool)
+  [W] C (Maybe (F a))
+we want to know that the second instance might match later. So we
+flatten the (F a) in the target before trying to unify with instances.
+(This is done in GHC.Core.InstEnv.lookupInstEnv'.)
+
 The algorithm works by building up a TypeMap TyVar, mapping
 type family applications to fresh variables. This mapping must
 be threaded through all the function calls, as any entry in
@@ -1758,11 +1777,11 @@ flattenTys is defined here because of module dependencies.
 -}
 
 data FlattenEnv
-  = FlattenEnv { fe_type_map :: TypeMap TyVar
+  = FlattenEnv { fe_type_map :: TypeMap (TyVar, TyCon, [Type])
                  -- domain: exactly-saturated type family applications
-                 -- range: fresh variables
+                 -- range: (fresh variable, type family tycon, args)
                , fe_in_scope :: InScopeSet }
-                 -- See Note [Flattening]
+                 -- See Note [Flattening type-family applications when matching instances]
 
 emptyFlattenEnv :: InScopeSet -> FlattenEnv
 emptyFlattenEnv in_scope
@@ -1773,13 +1792,29 @@ updateInScopeSet :: FlattenEnv -> (InScopeSet -> InScopeSet) -> FlattenEnv
 updateInScopeSet env upd = env { fe_in_scope = upd (fe_in_scope env) }
 
 flattenTys :: InScopeSet -> [Type] -> [Type]
--- See Note [Flattening]
--- NB: the returned types may mention fresh type variables,
---     arising from the flattening.  We don't return the
---     mapping from those fresh vars to the ty-fam
---     applications they stand for (we could, but no need)
-flattenTys in_scope tys
-  = snd $ coreFlattenTys emptyTvSubstEnv (emptyFlattenEnv in_scope) tys
+-- See Note [Flattening type-family applications when matching instances]
+flattenTys in_scope tys = fst (flattenTysX in_scope tys)
+
+flattenTysX :: InScopeSet -> [Type] -> ([Type], TyVarEnv (TyCon, [Type]))
+-- See Note [Flattening type-family applications when matching instances]
+-- NB: the returned types mention the fresh type variables
+--     in the domain of the returned env, whose range includes
+--     the original type family applications. Building a substitution
+--     from this information and applying it would yield the original
+--     types -- almost. The problem is that the original type might
+--     have something like (forall b. F a b); the returned environment
+--     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.
+flattenTysX in_scope tys
+  = let (env, result) = coreFlattenTys emptyTvSubstEnv (emptyFlattenEnv in_scope) tys in
+    (result, build_env (fe_type_map env))
+  where
+    build_env :: TypeMap (TyVar, TyCon, [Type]) -> TyVarEnv (TyCon, [Type])
+    build_env env_in
+      = foldTM (\(tv, tc, tys) env_out -> extendVarEnv env_out tv (tc, tys))
+               env_in emptyVarEnv
 
 coreFlattenTys :: TvSubstEnv -> FlattenEnv
                -> [Type] -> (FlattenEnv, [Type])
@@ -1841,7 +1876,7 @@ coreFlattenCo subst env co
     (env1, kind') = coreFlattenTy subst env (coercionType co)
     covar         = mkFlattenFreshCoVar (fe_in_scope env1) kind'
     -- Add the covar to the FlattenEnv's in-scope set.
-    -- See Note [Flattening], wrinkle 2A.
+    -- See Note [Flattening type-family applications when matching instances], wrinkle 2A.
     env2          = updateInScopeSet env1 (flip extendInScopeSet covar)
 
 coreFlattenVarBndr :: TvSubstEnv -> FlattenEnv
@@ -1849,7 +1884,7 @@ coreFlattenVarBndr :: TvSubstEnv -> FlattenEnv
 coreFlattenVarBndr subst env tv
   = (env2, subst', tv')
   where
-    -- See Note [Flattening], wrinkle 2B.
+    -- See Note [Flattening type-family applications when matching instances], wrinkle 2B.
     kind          = varType tv
     (env1, kind') = coreFlattenTy subst env kind
     tv'           = uniqAway (fe_in_scope env1) (setVarType tv kind')
@@ -1862,26 +1897,30 @@ coreFlattenTyFamApp :: TvSubstEnv -> FlattenEnv
                     -> (FlattenEnv, Type)
 coreFlattenTyFamApp tv_subst env fam_tc fam_args
   = case lookupTypeMap type_map fam_ty of
-      Just tv -> (env', mkAppTys (mkTyVarTy tv) leftover_args')
-      Nothing -> let tyvar_name = mkFlattenFreshTyName fam_tc
-                     tv         = uniqAway in_scope $
-                                  mkTyVar tyvar_name (typeKind fam_ty)
-
-                     ty'   = mkAppTys (mkTyVarTy tv) leftover_args'
-                     env'' = env' { fe_type_map = extendTypeMap type_map fam_ty tv
-                                  , fe_in_scope = extendInScopeSet in_scope tv }
-                 in (env'', ty')
+      Just (tv, _, _) -> (env', mkAppTys (mkTyVarTy tv) leftover_args')
+      Nothing ->
+        let tyvar_name = mkFlattenFreshTyName fam_tc
+            tv         = uniqAway in_scope $
+                         mkTyVar tyvar_name (typeKind fam_ty)
+
+            ty'   = mkAppTys (mkTyVarTy tv) leftover_args'
+            env'' = env' { fe_type_map = extendTypeMap type_map fam_ty
+                                                       (tv, fam_tc, sat_fam_args)
+                         , fe_in_scope = extendInScopeSet in_scope tv }
+        in (env'', ty')
   where
     arity = tyConArity fam_tc
     tcv_subst = TCvSubst (fe_in_scope env) tv_subst emptyVarEnv
     (sat_fam_args, leftover_args) = ASSERT( arity <= length fam_args )
                                     splitAt arity fam_args
     -- Apply the substitution before looking up an application in the
-    -- environment. See Note [Flattening], wrinkle 1.
+    -- environment. See Note [Flattening type-family applications when matching instances],
+    -- wrinkle 1.
     -- NB: substTys short-cuts the common case when the substitution is empty.
     sat_fam_args' = substTys tcv_subst sat_fam_args
     (env', leftover_args') = coreFlattenTys tv_subst env leftover_args
-    -- `fam_tc` may be over-applied to `fam_args` (see Note [Flattening],
+    -- `fam_tc` may be over-applied to `fam_args` (see
+    -- Note [Flattening type-family applications when matching instances]
     -- wrinkle 3), so we split it into the arguments needed to saturate it
     -- (sat_fam_args') and the rest (leftover_args')
     fam_ty = mkTyConApp fam_tc sat_fam_args'