GitLab

Marge Bot pushed to branch wip/marge_bot_batch_merge_job at Glasgow Haskell Compiler / GHC

Commits:

ec079385

by Simon Peyton Jones at 2026-10-12T18:14:12-04:00

Refactor fundeps again

This MR fixes #27828; there was a bad scoping error in `trim_qtvs`.

The main changes are

* Refactor `trim_qtvs` completely to eliminate the bug.

* Remove a redundant `apartnessCheck` from `mkTopOpenFamEqFDs`.

* Lots of improvements to the Notes in FunDeps.hs

I also did a couple of pure refactors:

* I realised that we were carefully caching `cab_incomps` in each
  `CoAxBranch`, to make it more efficient to reduce a type family application,
  but we were not doing the same thing when computing relevance for functional
  dependencies; see Note [Relevance] in GHC.Tc.Solver.FunDeps.  So I added
  `cab_overlaps`, which is now used in `noEarlierMatch`.

* Use a proper data types, `AmIUnifying` and `OuterKindsFlag`, for two
  previously-Boolean arguments to `tc_unify_tys`.  This is a pure refactor.

15 changed files:

+ changelog.d/T27828
compiler/GHC/Builtin/WiredIn/Types/Box.hs
compiler/GHC/Core/Coercion/Axiom.hs
compiler/GHC/Core/FamInstEnv.hs
compiler/GHC/Core/Unify.hs
compiler/GHC/Iface/Decl.hs
compiler/GHC/Iface/Syntax.hs
compiler/GHC/IfaceToCore.hs
compiler/GHC/Tc/Instance/FunDeps.hs
compiler/GHC/Tc/Solver/FunDeps.hs
compiler/GHC/Tc/TyCl.hs
+ testsuite/tests/indexed-types/should_compile/T27828.hs
+ testsuite/tests/indexed-types/should_compile/T27828a.hs
+ testsuite/tests/indexed-types/should_compile/T27828b.hs
testsuite/tests/indexed-types/should_compile/all.T

Changes:

changelog.d/T27828

 +section: compiler
 +synopsis: Fix a "No skolem info" compiler crash
 +issues: #27828
 +mrs: !16714
++
 +description: {
 +    There was a bug in the implementation of functional dependencies for type families.
 +}

compiler/GHC/Builtin/WiredIn/Types/Box.hs

@@ -329,7 +329,8 @@ mkWiredInNewTyCon tc_name dc_name nt_co_uniq bndrs roles nt_fld_ty =
                          , cab_roles   = roles
                          , cab_lhs     = mkTyVarTys tvs
                          , cab_rhs     = nt_fld_ty
 -                        , cab_incomps = [] }
 +                        , cab_overlaps = []
 +                        , cab_incomps  = [] }
  -- | The wired-in @Box@ newtype:
  --

compiler/GHC/Core/Coercion/Axiom.hs

@@ -18,7 +18,7 @@ module GHC.Core.Coercion.Axiom (
         coAxiomSingleBranch, coAxBranchTyVars, coAxBranchCoVars,
         coAxBranchRoles,
         coAxBranchLHS, coAxBranchRHS, coAxBranchSpan, coAxBranchIncomps,
 -       placeHolderIncomps,
 +       placeHolderIncomps, placeHolderOverlaps,
         Role(..),
@@ -195,23 +195,44 @@ mapAccumBranches f (MkBranches arr)
  Note [Storing compatibility]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 -During axiom application, we need to be aware of which branches are compatible
 -with which others. The full explanation is in Note [Compatibility] in
 -GHc.Core.FamInstEnv. (The code is placed there to avoid a dependency from
 -GHC.Core.Coercion.Axiom on the unification algorithm.) Although we could
 -theoretically compute compatibility on the fly, this is silly, so we store it
 -in a CoAxiom.
 +A `CoAxBranch` caches some useful information in `cab_incomps` and `cab_overlaps`:
 -Specifically, each branch refers to all other branches with which it is
 -incompatible. This list might well be empty, and it will always be for the
 -first branch of any axiom.
 +* `cab_overlaps`: when computing "relevance", in the function
 +  `GHC.Tc.Solver.FunDeps.getRelevantBranches`, we need to know which ealier branches
 +  can match this one -- see `noEarlierMatch`.
 -CoAxBranches that do not (yet) belong to a CoAxiom should have a panic thunk
 -stored in cab_incomps. The incompatibilities are properly a property of the
 -axiom as a whole, and they are computed only when the final axiom is built.
 +  Again we could look at all earlier branches, but instead we cache in `cab_overlaps`
 +  a list of all earlier branches that could overlap with this one.
 -During serialization, the list is converted into a list of the indices
 -of the branches.
 +* `cab_incomps`: during axiom application, we need to be aware of which branches are
 +  /compatible/ with which others. The full explanation is in Note [Compatibility] in
 +  GHC.Core.FamInstEnv. (The code is placed there to avoid a dependency from
 +  GHC.Core.Coercion.Axiom on the unification algorithm.)
++
 +  Although we could readily compute compatibility on the fly, this is silly, so we
 +  cache in `cab_incomps` a list of earlier branches that are /incompatible/ with
 +  this one.  (See Note [Compatibility] for a definition.)
++
 +  Always a sub-list of `cab_overlaps`.
++
 +Both lists can be empty, and always are for the first branch of any axiom.
++
 +Some extra points:
++
 +(SC1) A `CoAxBranch` that does not (yet) belong to a CoAxiom is initialised with panic
 +  thunks, `placeHolderOverlaps` or `placeHolderIncomps`, for the two fields; see `mkCoAxBranch`.
++
 +  Then, when a bunch of branches is grouped together in an axiom, we analyse the
 +  branches as a whole and initialise the fields properly, using `computeAxiomIncomps`.
 +  (For open type families, whose axioms have only one branch, we null out both lists
 +  with `noAxiomIncomps`.)
++
 +(SC2) We don't need to serialise `cab_overlaps` and `cab_incomps` into an interface
 +  file, because we recompute them in `computeAxiomIncomps`.  However, annoyingly,
 +  the pretty printer converts to IfaceSyn before printing, and we do want to show
 +  `cab_incomps` (see Note [Displaying axiom incompatibilities]).  So, tiresomely,
 +  `IfaceAxBranch` has a `ifaxbIncomps` field, used only for printing.  For historical
 +  reasons this is actually serialised.  Yuk.
  Note [CoAxioms are homogeneous]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -230,7 +251,9 @@ This is checked in FamInstEnv.mkCoAxBranch.
  -- If you edit this type, you may need to update the GHC formalism
  -- See Note [GHC Formalism] in GHC.Core.Lint
  data CoAxiom br
 -  = CoAxiom                   -- Type equality axiom.
 +  = -- `br` is Unbranched for each of the many axioms of an open type family
 +    --         Branched   for the single multi-branch axiom of a closed type family
 +    CoAxiom                   -- Type equality axiom.
      { co_ax_unique   :: Unique        -- Unique identifier
      , co_ax_name     :: Name          -- Name for pretty-printing
      , co_ax_role     :: Role          -- Role of the axiom's equality
@@ -268,8 +291,15 @@ data CoAxBranch
      , cab_rhs      :: Type
         -- ^ Right-hand side of the equality
         -- See Note [CoAxioms are homogeneous]
++
 +    , cab_overlaps :: [CoAxBranch]
 +       -- ^ The preceding branches whose LHSs are /unify with/ this one
 +       -- Order is unimportant
 +       -- See Note [Storing compatibility]
++
      , cab_incomps  :: [CoAxBranch]
 -       -- ^ The previous incompatible branches
 +       -- ^ The preceding branches that are /incompatible/ with this one
 +       -- Order is unimportant
         -- See Note [Storing compatibility]
+     }
    deriving Data.Data
@@ -342,8 +372,9 @@ coAxBranchIncomps :: CoAxBranch -> [CoAxBranch]
  coAxBranchIncomps = cab_incomps
  -- See Note [Compatibility] in GHC.Core.FamInstEnv
 -placeHolderIncomps :: [CoAxBranch]
 -placeHolderIncomps = panic "placeHolderIncomps"
 +placeHolderIncomps, placeHolderOverlaps :: [CoAxBranch]
 +placeHolderIncomps  = panic "placeHolderIncomps"
 +placeHolderOverlaps = panic "placeHolderOverlaps"
  {-
  Note [CoAxBranch type variables]

compiler/GHC/Core/FamInstEnv.hs

@@ -19,7 +19,7 @@ module GHC.Core.FamInstEnv (
          FamInstMatch(..),
          lookupFamInstEnv, lookupFamInstEnvConflicts, lookupFamInstEnvByTyCon,
 -        isDominatedBy, apartnessCheck, compatibleBranches,
 +        isDominatedBy, apartnessCheck, noEarlierMatchCheck, compatibleBranches,
          -- Injectivity
          InjectivityCheckResult(..),
@@ -487,20 +487,45 @@ in GHC.Core.Unify.)
  Note [Compatibility]
  ~~~~~~~~~~~~~~~~~~~~
 -Two patterns are /compatible/ if either of the following conditions hold:
 -1) The patterns are apart.
 -2) The patterns unify with a substitution S, and their right hand sides
 -equal under that substitution.
 +Consider a closed type family with two equations (X1) and (X2)
 +   type family F a where
 +      F lhs1 = rhs1   -- (X1)
 +      ...
 +      F lhs2 = rhs2   -- (X2)
 +      ...
 +Then equations (X1) and (X2) are /compatible/ if any target (F ty) that
 +matches both equations yields the very same right hand side.  Example:
 +      And True True = True
 +      And a    True = a
 +The target (And True True) matches both equations but they then both
 +produce the same reduct True.
++
 +More precisely (X1) and (X2) are /compatible/ iff
 +   If LHSs unify with a substitution S, then S(rhs1) = S(rhs2)
++
 +Conversely, (X1) and (X2) are /incompatible/ if
 +   Their LHSs unify with S, and S(rhs1) /= S(rhs2)
  For open type families, only compatible instances are allowed. For closed
 -type families, the story is slightly more complicated. Consider the following:
 +families, we use the Closed Family Matching Rule (see function `findBranch`):
 -type family F a where
 -  F Int = Bool
 -  F a   = Int
 +    When looking up a target (F ty) in a closed type family F,
 +    find an equation (branch) such that:
 +      * the LHS matches the target
 +      * the target is apart from every previous /incompatible/ equation for F
 -g :: Show a => a -> F a
 -g x = length (show x)
 +We don't need to check the earlier equations that are compatible with the
 +matching equation, because they are either irrelevant (clause 1 of compatible)
 +or benign (clause 2 of compatible).
++
 +Some examples:
++
 +  type family F a where
 +    F Int = Bool
 +    F a   = Int
++
 +  g :: Show a => a -> F a
 +  g x = length (show x)
  Should that type-check? No. We need to allow for the possibility that 'a'
  might be Int and therefore 'F a' should be Bool. We can simplify 'F a' to Int
@@ -516,12 +541,12 @@ potentially-overlapping group is closed.
  As another example, consider this:
 -type family G x where
 -  G Int = Bool
 -  G a   = Double
 +  type family G x where
 +    G Int = Bool
 +    G a   = Double
 -type family H y
 --- no instances
 +  type family H y
 +  -- no instances
  Now, we want to simplify (G (H Char)). We can't, because (H Char) might later
  simplify to be Int. So, (G (H Char)) is stuck, for now.
@@ -529,18 +554,13 @@ simplify to be Int. So, (G (H Char)) is stuck, for now.
  While everything above is quite sound, it isn't as expressive as we'd like.
  Consider this:
 -type family J a where
 -  J Int = Int
 -  J a   = a
 +  type family J a where
 +    J Int = Int
 +    J a   = a
  Can we simplify (J b) to b? Sure we can. Yes, the first equation matches if
  b is instantiated with Int, but the RHSs coincide there, so it's all OK.
+-
 -So, the rule is this: when looking up a branch in a closed type family, we
 -find a branch that matches the target, but then we make sure that the target
 -is apart from every previous *incompatible* branch. We don't check the
 -branches that are compatible with the matching branch, because they are either
 -irrelevant (clause 1 of compatible) or benign (clause 2 of compatible).
 +Hence the Closed Family Matching Rule.
  Note [Compatibility of eta-reduced axioms]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -572,15 +592,32 @@ fails anyway.
  -- See Note [Compatibility]
  compatibleBranches :: CoAxBranch -> CoAxBranch -> Bool
 -compatibleBranches (CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 })
 -                   (CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 })
 +compatibleBranches b1 b2
 +  = case compareBranches b1 b2 of
 +       BC_Apart    -> True
 +       BC_Compat   -> True
 +       BC_Incompat -> False
++
 +data BranchCompatibility
 +  = BC_Apart     -- LHSs are apart
 +  | BC_Compat    -- LHSs unify with S, and S(rhs1)=S(rhs2)
 +  | BC_Incompat  -- LHSs unify with S, and S(rhs1)/=S(rhs2)
++
 +compareBranches :: CoAxBranch -> CoAxBranch -> BranchCompatibility
 +compareBranches (CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 })
 +                (CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 })
    = case tcUnifyTysFG alwaysBindFam alwaysBindTv commonlhs1 commonlhs2 of
        -- Here we need the cab_tvs of the two branches to be disinct.
        -- See Note [CoAxBranch type variables] in GHC.Core.Coercion.Axiom.
 -      SurelyApart     -> True
 -      MaybeApart {}   -> False
 -      Unifiable subst -> Type.substTyAddInScope subst rhs1 `eqType`
 +      SurelyApart     -> BC_Apart
 +      Unifiable subst |  Type.substTyAddInScope subst rhs1 `eqType`
                           Type.substTyAddInScope subst rhs2
 +                      -> BC_Compat
 +                      | otherwise
 +                      -> BC_Incompat
 +      MaybeApart {}   -> BC_Incompat
 +        -- An occurs check yields MaybeApart;
 +        -- see Note [Infinitary substitutions] in GHC.Core.Unify
    where
       (commonlhs1, commonlhs2) = zipAndUnzip lhs1 lhs2
       -- See Note [Compatibility of eta-reduced axioms]
@@ -603,8 +640,7 @@ injectiveBranches injectivity
                    ax1@(CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 })
                    ax2@(CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 })
    -- See Note [Verifying injectivity annotation], case 1.
 -  = case tcUnifyTysForInjectivity True [rhs1] [rhs2] of
 -             -- True = two-way pre-unification
 +  = case tcUnifyTysForInjectivity Unifying [rhs1] [rhs2] of
         Nothing -> InjectivityAccepted
           -- RHS are different, so equations are injective.
           -- This is case 1A from Note [Verifying injectivity annotation]
@@ -629,10 +665,11 @@ injectiveBranches injectivity
            lhs1Subst = Type.substTys subst (getInjArgs lhs1)
            lhs2Subst = Type.substTys subst (getInjArgs lhs2)
 --- takes a CoAxiom with unknown branch incompatibilities and computes
 --- the compatibilities
 --- See Note [Storing compatibility] in GHC.Core.Coercion.Axiom
  computeAxiomIncomps :: [CoAxBranch] -> [CoAxBranch]
 +-- Takes a CoAxiom for a closed type family that has place-holder
 +-- `cab_incomps` and `cab_overlaps` fields, and computes those fields
 +-- properly from the list of branches.
 +-- See Note [Storing compatibility] in GHC.Core.Coercion.Axiom
  computeAxiomIncomps branches
    = snd (mapAccumL go [] branches)
    where
@@ -640,11 +677,23 @@ computeAxiomIncomps branches
      go prev_brs cur_br
         = (new_br : prev_brs, new_br)
         where
 -         new_br = cur_br { cab_incomps = mk_incomps prev_brs cur_br }
+-
 -    mk_incomps :: [CoAxBranch] -> CoAxBranch -> [CoAxBranch]
 -    mk_incomps prev_brs cur_br
 -       = filter (not . compatibleBranches cur_br) prev_brs
 +         (overlaps,incomps) = get_cab [] [] prev_brs
 +         new_br = cur_br { cab_overlaps = overlaps, cab_incomps  = incomps }
++
 +         get_cab :: [CoAxBranch] -> [CoAxBranch]   -- Accumulators
 +                 -> [CoAxBranch]
 +                 -> ([CoAxBranch], [CoAxBranch])
 +         get_cab overlaps incomps [] = (overlaps,incomps)
 +         get_cab overlaps incomps (br:brs)
 +            = case compareBranches cur_br br of
 +                BC_Apart    -> get_cab overlaps      incomps      brs
 +                BC_Compat   -> get_cab (br:overlaps) incomps      brs
 +                BC_Incompat -> get_cab (br:overlaps) (br:incomps) brs
++
 +noAxiomIncomps :: CoAxBranch -> CoAxBranch
 +-- Overwrite the placeholders for `cab_incomps` and `cab_overlaps`
 +-- with [], because unbranched axioms have no "preceding" equations
 +noAxiomIncomps branch = branch { cab_incomps = [], cab_overlaps = [] }
  {-
  ************************************************************************
@@ -715,14 +764,17 @@ mkCoAxBranch :: [TyVar] -- original, possibly stale, tyvars
               -> SrcSpan
               -> CoAxBranch
  mkCoAxBranch tvs eta_tvs cvs lhs rhs roles loc
 -  = CoAxBranch { cab_tvs     = tvs'
 -               , cab_eta_tvs = eta_tvs'
 -               , cab_cvs     = cvs'
 -               , cab_lhs     = tidyTypes env lhs
 -               , cab_roles   = roles
 -               , cab_rhs     = tidyType env rhs
 -               , cab_loc     = loc
 -               , cab_incomps = placeHolderIncomps }
 +  = CoAxBranch { cab_tvs      = tvs'
 +               , cab_eta_tvs  = eta_tvs'
 +               , cab_cvs      = cvs'
 +               , cab_lhs      = tidyTypes env lhs
 +               , cab_roles    = roles
 +               , cab_rhs      = tidyType env rhs
 +               , cab_loc      = loc
++
 +               -- See (SC1) in Note [Storing compatibility]
 +               , cab_overlaps = placeHolderOverlaps
 +               , cab_incomps  = placeHolderIncomps }
    where
      (env1, tvs')     = tidyVarBndrs init_tidy_env tvs
      (env2, eta_tvs') = tidyVarBndrs env1          eta_tvs
@@ -736,14 +788,16 @@ mkCoAxBranch tvs eta_tvs cvs lhs rhs roles loc
  -- all of the following code is here to avoid mutual dependencies with
  -- Coercion
 -mkBranchedCoAxiom :: Name -> TyCon -> [CoAxBranch] -> CoAxiom Branched
 -mkBranchedCoAxiom ax_name fam_tc branches
 +mkBranchedCoAxiom :: Role -> Name -> TyCon -> [CoAxBranch] -> CoAxiom Branched
 +mkBranchedCoAxiom role ax_name fam_tc branches
    = CoAxiom { co_ax_unique   = nameUnique ax_name
              , co_ax_name     = ax_name
              , co_ax_tc       = fam_tc
 -            , co_ax_role     = Nominal
 +            , co_ax_role     = role
              , co_ax_implicit = False
              , co_ax_branches = manyBranches (computeAxiomIncomps branches) }
 +                               -- computeAxiomIncomps: see (SC1) in
 +                               --      Note [Storing compatibility]
  mkUnbranchedCoAxiom :: Name -> TyCon -> CoAxBranch -> CoAxiom Unbranched
  mkUnbranchedCoAxiom ax_name fam_tc branch
@@ -752,7 +806,9 @@ mkUnbranchedCoAxiom ax_name fam_tc branch
              , co_ax_tc       = fam_tc
              , co_ax_role     = Nominal
              , co_ax_implicit = False
 -            , co_ax_branches = unbranched (branch { cab_incomps = [] }) }
 +            , co_ax_branches = unbranched (noAxiomIncomps branch) }
 +                               -- noAxiomIncomps: see (SC1) in
 +                               --      Note [Storing compatibility]
  mkSingleCoAxiom :: Role -> Name
                  -> [TyVar] -> [TyVar] -> [CoVar]
@@ -767,7 +823,9 @@ mkSingleCoAxiom role ax_name tvs eta_tvs cvs fam_tc lhs_tys rhs_ty
              , co_ax_tc       = fam_tc
              , co_ax_role     = role
              , co_ax_implicit = False
 -            , co_ax_branches = unbranched (branch { cab_incomps = [] }) }
 +            , co_ax_branches = unbranched (noAxiomIncomps branch) }
 +                               -- noAxiomIncomps: see (SC1) in
 +                               --      Note [Storing compatibility]
    where
      branch = mkCoAxBranch tvs eta_tvs cvs lhs_tys rhs_ty
                            (map (const Nominal) tvs)
@@ -785,7 +843,9 @@ mkNewTypeCoAxiom name tycon tvs roles rhs_ty
              , co_ax_implicit = True  -- See Note [Implicit axioms] in GHC.Core.TyCon
              , co_ax_role     = Representational
              , co_ax_tc       = tycon
 -            , co_ax_branches = unbranched (branch { cab_incomps = [] }) }
 +            , co_ax_branches = unbranched (noAxiomIncomps branch) }
 +                               -- noAxiomIncomps: see (SC1) in
 +                               --      Note [Storing compatibility]
    where
      branch = mkCoAxBranch tvs [] [] (mkTyVarTys tvs) rhs_ty
                            roles (getSrcSpan name)
@@ -1223,7 +1283,9 @@ findBranch :: Array BranchIndex CoAxBranch
             -> Maybe (BranchIndex, [Type], [Coercion])
      -- coercions relate requested types to returned axiom LHS at role N
  findBranch branches target_tys
 -  = foldr go Nothing (assocs branches)
 +  = -- Implements the Closed Family Matching Rule
 +    -- in Note [Compatibility]
 +    foldr go Nothing (assocs branches)
    where
      go :: (BranchIndex, CoAxBranch)
         -> Maybe (BranchIndex, [Type], [Coercion])
@@ -1258,6 +1320,20 @@ apartnessCheck target (CoAxBranch { cab_incomps = incomps })
      isSurelyApart SurelyApart = True
      isSurelyApart _           = False
 +-- | Check whether an earlier branch matches these target types
 +noEarlierMatchCheck
 +  :: [Type]
 +  -> CoAxBranch -- ^ The candidate equation we wish to use
 +  -> Bool       -- ^ True <=> equation can fire
 +noEarlierMatchCheck target (CoAxBranch { cab_overlaps = overlaps })
 +    -- NB: this is the /only/ use of the `cab_overlaps` field
 +    -- See Note [Storing compatibility] and
 +    -- (RW4) in Note [Relevance]
 +  = not (any matches overlaps)
 +  where
 +    matches earlier_branch
 +      = isJust (tcMatchTys (coAxBranchLHS earlier_branch) target)
++
  {-
  ************************************************************************
  *                                                                      *

compiler/GHC/Core/Unify.hs

@@ -9,6 +9,7 @@ module GHC.Core.Unify (
          tcMatchTyX_BM, ruleMatchTyKiX,
          -- Side-effect free unification
 +        AmIUnifying(..),
          tcUnifyTy, tcUnifyTys, tcUnifyFunDeps, tcUnifyDebugger,
          tcUnifyTysFG, tcUnifyTysForInjectivity,
          BindTvFun, BindFamFun, BindFlag(..),
@@ -597,14 +598,14 @@ tcMatchTyX_BM :: HasDebugCallStack
                => BindTvFun -> Subst
                -> Type -> Type -> Maybe Subst
  tcMatchTyX_BM bind_tv subst ty1 ty2
 -  = tc_match_tys_x bind_tv False subst [ty1] [ty2]
 +  = tc_match_tys_x bind_tv IgnoreOuterKinds subst [ty1] [ty2]
  -- | Like 'tcMatchTy', but allows the kinds of the types to differ,
  -- and thus matches them as well.
  -- See also Note [tcMatchTy vs tcMatchTyKi]
  tcMatchTyKi :: HasDebugCallStack => Type -> Type -> Maybe Subst
  tcMatchTyKi ty1 ty2
 -  = tc_match_tys alwaysBindTv True [ty1] [ty2]
 +  = tc_match_tys alwaysBindTv CheckOuterKinds [ty1] [ty2]
  -- | This is similar to 'tcMatchTy', but extends a substitution
  -- See also Note [tcMatchTy vs tcMatchTyKi]
@@ -614,7 +615,7 @@ tcMatchTyX :: HasDebugCallStack
             -> Type                -- ^ Target
             -> Maybe Subst
  tcMatchTyX subst ty1 ty2
 -  = tc_match_tys_x alwaysBindTv False subst [ty1] [ty2]
 +  = tc_match_tys_x alwaysBindTv IgnoreOuterKinds subst [ty1] [ty2]
  -- | Like 'tcMatchTy' but over a list of types.
  -- See also Note [tcMatchTy vs tcMatchTyKi]
@@ -625,7 +626,7 @@ tcMatchTys :: HasDebugCallStack
                               -- variables could be free in the target
                               -- See (CU6) in Note [The Core unifier]
  tcMatchTys tys1 tys2
 -  = tc_match_tys alwaysBindTv False tys1 tys2
 +  = tc_match_tys alwaysBindTv IgnoreOuterKinds tys1 tys2
  -- | Like 'tcMatchTyKi' but over a list of types.
  -- See also Note [tcMatchTy vs tcMatchTyKi]
@@ -635,7 +636,7 @@ tcMatchTyKis :: HasDebugCallStack
               -> Maybe Subst    -- ^ One-shot substitution
                                 -- See (CU6) in Note [The Core unifier]
  tcMatchTyKis tys1 tys2
 -  = tc_match_tys alwaysBindTv True tys1 tys2
 +  = tc_match_tys alwaysBindTv CheckOuterKinds tys1 tys2
  -- | Like 'tcMatchTys', but extending a substitution
  -- See also Note [tcMatchTy vs tcMatchTyKi]
@@ -645,7 +646,7 @@ tcMatchTysX :: HasDebugCallStack
              -> [Type]         -- ^ Target
              -> Maybe Subst    -- ^ One-shot substitution
  tcMatchTysX subst tys1 tys2
 -  = tc_match_tys_x alwaysBindTv False subst tys1 tys2
 +  = tc_match_tys_x alwaysBindTv IgnoreOuterKinds subst tys1 tys2
  -- | Like 'tcMatchTyKis', but extending a substitution
  -- See also Note [tcMatchTy vs tcMatchTyKi]
@@ -655,12 +656,12 @@ tcMatchTyKisX :: HasDebugCallStack
                -> [Type]       -- ^ Target
                -> Maybe Subst  -- ^ One-shot substitution
  tcMatchTyKisX subst tys1 tys2
 -  = tc_match_tys_x alwaysBindTv True subst tys1 tys2
 +  = tc_match_tys_x alwaysBindTv CheckOuterKinds subst tys1 tys2
  -- | Same as tc_match_tys_x, but starts with an empty substitution
  tc_match_tys :: HasDebugCallStack
               => BindTvFun
 -             -> Bool          -- ^ match kinds?
 +             -> OuterKindsFlag   -- ^ Match kinds?
               -> [Type]
               -> [Type]
               -> Maybe Subst
@@ -672,7 +673,7 @@ tc_match_tys bind_me match_kis tys1 tys2
  -- | Worker for 'tcMatchTysX' and 'tcMatchTyKisX'
  tc_match_tys_x :: HasDebugCallStack
                 => BindTvFun
 -               -> Bool          -- ^ match kinds?
 +               -> OuterKindsFlag   -- ^ Match kinds?
                 -> Subst
                 -> [Type]
                 -> [Type]
@@ -680,8 +681,8 @@ tc_match_tys_x :: HasDebugCallStack
  tc_match_tys_x bind_tv match_kis (Subst in_scope id_env tv_env cv_env) tys1 tys2
    = case tc_unify_tys neverBindFam  -- (ATF7) in Note [Apartness and type families]
                        bind_tv
 -                      False  -- Matching, not unifying
 -                      False  -- Not an injectivity check
 +                      Matching  -- Matching, not unifying
 +                      False     -- Not an injectivity check
                        match_kis
                        RespectMultiplicities
                        (mkRnEnv2 in_scope) tv_env cv_env tys1 tys2 of
@@ -706,9 +707,9 @@ ruleMatchTyKiX tmpl_tvs rn_env tenv tmpl target
        -- But even if it did, (ATF8) in Note [Apartness and type families]
        -- says it doesn't matter becuase here we only care about Unifiable.
        -- So neverBindFam is efficient, and sufficient.
 -                      False    -- Matching, not unifying
 +                      Matching -- Matching, not unifying
                        False    -- No doing an injectivity check
 -                      True     -- Match the kinds
 +                      CheckOuterKinds  -- Match the kinds
                        IgnoreMultiplicities
                          -- See Note [Rewrite rules ignore multiplicities in FunTy]
                        rn_env tenv emptyCvSubstEnv [tmpl] [target] of
@@ -784,7 +785,7 @@ tcUnifyTy t1 t2 = tcUnifyTys alwaysBindTv [t1] [t2]
  tcUnifyDebugger :: Type -> Type -> Maybe Subst
  tcUnifyDebugger t1 t2
    = case tc_unify_tys_fg
 -             True            -- Unify kinds
 +             CheckOuterKinds -- Unify kinds
               neverBindFam    -- Does not affect Unifiable, so pick max efficient
                               -- See (ATF8) in Note [Apartness and type families]
               alwaysBindTv
@@ -798,7 +799,7 @@ tcUnifyFunDeps :: TyCoVarSet
                 -> Maybe Subst
  tcUnifyFunDeps qtvs tys1 tys2
    = case tc_unify_tys_fg
 -             True               -- Unify kinds
 +             CheckOuterKinds    -- Unify kinds
               dontCareBindFam    -- Class-instance heads never mention type families
               (matchBindTv qtvs)
               tys1 tys2 of
@@ -821,7 +822,7 @@ tcUnifyTysForInjectivity unif tys1 tys2
    = case tc_unify_tys alwaysBindFam alwaysBindTv
                         unif   -- Am I unifying?
                         True   -- Do injectivity checks
 -                       False  -- Don't check outermost kinds
 +                       IgnoreOuterKinds  -- Don't check outermost kinds
                         RespectMultiplicities
                         rn_env emptyTvSubstEnv emptyCvSubstEnv
                         tys1 tys2 of
@@ -838,8 +839,9 @@ tcUnifyTysForInjectivity unif tys1 tys2
                 -- should never actually be done
      maybe_fix tv_subst
 -      | unif      = niFixSubst in_scope tv_subst
 -      | otherwise = mkTvSubst  in_scope tv_subst
 +      = case unif of
 +          Unifying -> niFixSubst in_scope tv_subst
 +          Matching -> mkTvSubst  in_scope tv_subst
        -- When matching, don't confuse domain with range; no fixpoint!
  -----------------
@@ -866,15 +868,15 @@ tcUnifyTysFG :: BindFamFun -> BindTvFun
               -> [Type] -> [Type]
               -> UnifyResult
  tcUnifyTysFG bind_fam bind_tv tys1 tys2
 -  = tc_unify_tys_fg False bind_fam bind_tv tys1 tys2
 +  = tc_unify_tys_fg IgnoreOuterKinds bind_fam bind_tv tys1 tys2
 -tc_unify_tys_fg :: Bool
 +tc_unify_tys_fg :: OuterKindsFlag
                  -> BindFamFun -> BindTvFun
                  -> [Type] -> [Type]
                  -> UnifyResult
  tc_unify_tys_fg match_kis bind_fam bind_tv tys1 tys2
    = do { (tv_env, _) <- tc_unify_tys bind_fam bind_tv
 -                                  True       -- Unifying
 +                                  Unifying
                                    False      -- Not doing an injectivity check
                                    match_kis  -- Match outer kinds
                                    RespectMultiplicities rn_env
@@ -888,10 +890,10 @@ tc_unify_tys_fg match_kis bind_fam bind_tv tys1 tys2
  -- | This function is actually the one to call the unifier -- a little
  -- too general for outside clients, though.
  tc_unify_tys :: BindFamFun -> BindTvFun
 -             -> AmIUnifying -- ^ True <=> unify; False <=> match
 -             -> Bool        -- ^ True <=> doing an injectivity check
 -             -> Bool        -- ^ True <=> treat the kinds as well
 -             -> MultiplicityFlag -- ^ see Note [Rewrite rules ignore multiplicities in FunTy] in GHC.Core.Unify
 +             -> AmIUnifying    -- ^ Unifying or matching
 +             -> Bool           -- ^ True <=> doing an injectivity check
 +             -> OuterKindsFlag -- ^ Check outer kinds or not
 +             -> MultiplicityFlag  -- ^ see Note [Rewrite rules ignore multiplicities in FunTy] in GHC.Core.Unify
               -> RnEnv2
               -> TvSubstEnv  -- ^ substitution to extend
               -> CvSubstEnv
@@ -910,8 +912,9 @@ tc_unify_tys :: BindFamFun -> BindTvFun
  -- See also Note [tcMatchTy vs tcMatchTyKi].
  tc_unify_tys bind_fam bind_tv unif inj_check match_kis match_mults rn_env tv_env cv_env tys1 tys2
    = initUM tv_env cv_env $
 -    do { when match_kis $
 -         unify_tys env kis1 kis2
 +    do { case match_kis of
 +            CheckOuterKinds  -> unify_tys env kis1 kis2
 +            IgnoreOuterKinds -> return ()
         ; unify_tys env tys1 tys2 }
    where
      env = UMEnv { um_bind_tv_fun  = bind_tv
@@ -926,6 +929,11 @@ tc_unify_tys bind_fam bind_tv unif inj_check match_kis match_mults rn_env tv_env
      kis2 = map typeKind tys2
 +data OuterKindsFlag
 +  = CheckOuterKinds    -- Unify or match the /kind/ of the two types
 +  | IgnoreOuterKinds   -- Just unify or match the types, ignoring kinds
 +                       --  (typically, we already know they are equal)
++
  {- *********************************************************************
  *                                                                      *
                  UnifyResult, MaybeApart etc
@@ -1583,8 +1591,7 @@ c.f. Note [Comparing type synonyms] in GHC.Core.TyCo.Compare
  -------------- unify_ty: the main workhorse -----------
 -type AmIUnifying = Bool   -- True  <=> Unifying
 -                          -- False <=> Matching
 +data AmIUnifying = Matching | Unifying
  type InType      = Type       -- Before applying the RnEnv2
  type OutCoercion = Coercion   -- After applying the RnEnv2
@@ -1618,7 +1625,7 @@ unify_ty env (CastTy ty1 co1) ty2 kco
      -- See (KCU1) in Note [Kind coercions in Unify]
    = maybeApart MARCast  -- See (KCU2)
 -  | um_unif env
 +  | Unifying <- um_unif env
    = unify_ty env ty1 ty2 (co1 `mkTransCo` kco)
    | otherwise -- We are matching, not unifying
@@ -1661,7 +1668,7 @@ unify_ty env (CoercionTy co1) (CoercionTy co2) kco
    = do { c_subst <- getCvSubstEnv
         ; case co1 of
             CoVarCo cv
 -             | not (um_unif env)
 +             | Matching <- um_unif env
               , not (cv `elemVarEnv` c_subst)   -- Not forall-bound
               , let (_mult_co, co_l, co_r) = decomposeFunCo kco
                       -- Because the coercion is used in a type, it should be safe to
@@ -1682,7 +1689,7 @@ unify_ty env (TyVarTy tv1) ty2 kco
    = uVarOrFam env (TyVarLHS tv1) ty2 kco
  unify_ty env ty1 (TyVarTy tv2) kco
 -  | um_unif env  -- If unifying, can swap args; but not when matching
 +  | Unifying <- um_unif env  -- If unifying, can swap args; but not when matching
    = uVarOrFam (umSwapRn env) (TyVarLHS tv2) ty1 (mkSymCo kco)
  -- Deal with TyConApps
@@ -1692,7 +1699,7 @@ unify_ty env ty1 ty2 kco
    | Just (tc,tys) <- mb_sat_fam_app1
    = uVarOrFam env (TyFamLHS tc tys) ty2 kco
 -  | um_unif env
 +  | Unifying <- um_unif env
    , Just (tc,tys) <- mb_sat_fam_app2
    = uVarOrFam (umSwapRn env) (TyFamLHS tc tys) ty1 (mkSymCo kco)
@@ -1820,7 +1827,7 @@ uVarOrFam env ty1 ty2 kco
      go swapped substs lhs@(TyVarLHS tv1) ty2 kco
        | Just ty1' <- lookupVarEnv (um_tv_env substs) tv1'
        = -- We already have a substitution for tv1
 -        if | um_unif env                          -> unify_ty env ty1' ty2 kco
 +        if | Unifying <- um_unif env              -> unify_ty env ty1' ty2 kco
             | (ty1' `mkCastTy` kco) `tcEqType` ty2 -> return ()
             | otherwise                            -> surelyApart
             -- Unifying: recurse into unify_ty
@@ -1842,9 +1849,9 @@ uVarOrFam env ty1 ty2 kco
        | TyVarTy tv2 <- ty2
        , let tv2' = umRnOccR env tv2
        , tv1' == tv2'
 -      = if | um_unif env     -> return ()
 -           | tv1_is_bindable -> extendTvEnv tv1' ty2
 -           | otherwise       -> return ()
 +      = if | Unifying <- um_unif env -> return ()
 +           | tv1_is_bindable         -> extendTvEnv tv1' ty2
 +           | otherwise               -> return ()
        | tv1_is_bindable
        , not (mentionsForAllBoundTyVarsR env ty2_fvs)
@@ -1858,9 +1865,9 @@ uVarOrFam env ty1 ty2 kco
        -- e.g.   a    ~ F p q       with `a` not bindable: we might succeed with go_fam
        -- e.g.   a    ~ beta        with `a` not bindable: we might be able to bind `beta`
        -- e.g.   beta ~ F beta Int  occurs check; but MaybeApart after swapping
 -      | um_unif env
 +      | Unifying   <- um_unif env
        , NotSwapped <- swapped  -- If we have swapped already, don't do so again
 -      , Just lhs2 <- canEqLHS_maybe ty2
 +      , Just lhs2  <- canEqLHS_maybe ty2
        = go IsSwapped substs lhs2 (mkTyVarTy tv1) (mkSymCo kco)
        | occurs_check = maybeApart MARInfinite   -- Occurs check
@@ -1879,7 +1886,9 @@ uVarOrFam env ty1 ty2 kco
                          | otherwise
                          = False
 -        occurs_check = um_unif env && uOccursCheck substs foralld_tvs lhs rhs
 +        occurs_check = case um_unif env of
 +                         Unifying -> uOccursCheck substs foralld_tvs lhs rhs
 +                         Matching -> False
            -- Occurs check, only when unifying
            -- see Note [Infinitary substitutions]
            -- Make sure you include `kco` in rhs #14846
@@ -1893,7 +1902,7 @@ uVarOrFam env ty1 ty2 kco
        -- Hence the RnEnv2 is empty
        | not under_forall
        , Just ty1' <- lookupFamEnv (um_fam_env substs) tc1 tys1
 -      = if | um_unif env                          -> unify_ty env ty1' ty2 kco
 +      = if | Unifying <- um_unif env              -> unify_ty env ty1' ty2 kco
             -- Below here we are matching
             -- The return () case deals with:
             --    Template:   (F a)..(F a)
@@ -1930,9 +1939,9 @@ uVarOrFam env ty1 ty2 kco
        -- NB: a type family can appear on the template when matching
        --     see (ATF6) in Note [Apartness and type families]
        -- (Only worth doing this if we are not under a forall.)
 -      | um_unif env
 +      | Unifying   <- um_unif env
        , NotSwapped <- swapped
 -      , Just lhs2 <- canEqLHS_maybe ty2
 +      , Just lhs2  <- canEqLHS_maybe ty2
        = go IsSwapped substs lhs2 (mkTyConApp tc1 tys1) (mkSymCo kco)
        | otherwise   -- See (ATF5) in Note [Apartness and type families]
@@ -1962,9 +1971,9 @@ uVarOrFam env ty1 ty2 kco
         (inj_tys2, noninj_tys2) = partitionByList inj tys2
         bind_fam_if_poss
 -         | not (um_unif env)  -- Not when matching (ATF11-1)
 +         | Matching <- um_unif env  -- Not when matching (ATF11-1)
           = return ()
 -         | under_forall       -- Not under a forall (ATF3)
 +         | under_forall             -- Not under a forall (ATF3)
           = return ()
           | BindMe <- um_bind_fam_fun env tc tys1 rhs1
           = unless (uOccursCheck substs emptyVarSet (TyFamLHS tc tys1) rhs1) $

compiler/GHC/Iface/Decl.hs

@@ -112,7 +112,7 @@ coAxBranchToIfaceBranch tc lhs_s
                    , ifaxbRoles   = roles
                    , ifaxbRHS     = toIfaceType rhs
                    , ifaxbIncomps = iface_incomps }
 -  where
 + where
      iface_incomps = map (expectJust
                          . flip findIndex lhs_s
                          . eqTypes

compiler/GHC/Iface/Syntax.hs

@@ -338,7 +338,12 @@ data IfaceAxBranch = IfaceAxBranch { ifaxbTyVars    :: [IfaceTvBndr]
                                     , ifaxbRoles     :: [Role]
                                     , ifaxbRHS       :: IfaceType
                                     , ifaxbIncomps   :: [BranchIndex] }
 -                                     -- See Note [Storing compatibility] in GHC.Core.Coercion.Axiom
 +    -- We store the incompatibilities in IfaceAxBranch
 +    --   just for (perhaps unnecessary) display purposes:
 +    --   see Note [Displaying axiom incompatibilities]
 +    -- When we construct a real CoAxBranch we compute cab_incomps directly
 +    --   from the equations, ignoring the ifaxbIncomps.
 +    -- We could consider getting rid of ifaxbIncomps altogether.
  data IfaceConDecls
    = IfAbstractTyCon -- c.f TyCon.AbstractTyCon
@@ -779,14 +784,13 @@ that is what is seen by importing module with --make
  Note [Displaying axiom incompatibilities]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 -With -fprint-axiom-incomps we display which closed type family equations
 -are incompatible with which. This information is sometimes necessary
 -because GHC doesn't try equations in order: any equation can be used when
 -all preceding equations that are incompatible with it do not apply.
+-
 -For example, the last "a && a = a" equation in Data.Type.Bool.&& is
 -actually compatible with all previous equations, and can reduce at any
 -time.
 +With -fprint-axiom-incomps we display which closed type family equations are
 +incompatible with which (see #15546). This information is sometimes necessary
 +because GHC doesn't try equations in order: any equation can be used when all
 +preceding equations that are incompatible with it do not apply.
++
 +For example, the last "a && a = a" equation in Data.Type.Bool.&& is actually
 +compatible with all previous equations, and can reduce at any time.
  This is displayed as:
  Prelude> :i Data.Type.Equality.==

compiler/GHC/IfaceToCore.hs

@@ -91,7 +91,6 @@ import GHC.Utils.Logger
  import GHC.Data.Bag
  import GHC.Data.Maybe
  import GHC.Data.FastString
 -import GHC.Data.List.SetOps
  import GHC.Types.Annotations
  import GHC.Types.SourceFile
@@ -903,12 +902,7 @@ tc_iface_decl _ _ (IfaceAxiom { ifName = tc_name, ifTyCon = tc
         -- See #13803
         ; tc_branches <- forkM (text "Axiom branches" <+> ppr tc_name)
                        $ tc_ax_branches branches
 -       ; let axiom = CoAxiom { co_ax_unique   = nameUnique tc_name
 -                             , co_ax_name     = tc_name
 -                             , co_ax_tc       = tc_tycon
 -                             , co_ax_role     = role
 -                             , co_ax_branches = manyBranches tc_branches
 -                             , co_ax_implicit = False }
 +       ; let axiom = mkBranchedCoAxiom role tc_name tc_tycon tc_branches
         ; return (ACoAxiom axiom) }
  tc_iface_decl _ _ (IfacePatSyn{ ifName = name
@@ -1116,15 +1110,14 @@ tc_fd (tvs1, tvs2) = do { tvs1' <- mapM tcIfaceTyVar tvs1
                          ; return (tvs1', tvs2') }
  tc_ax_branches :: [IfaceAxBranch] -> IfL [CoAxBranch]
 -tc_ax_branches if_branches = foldlM tc_ax_branch [] if_branches
 +tc_ax_branches if_branches = mapM tc_ax_branch if_branches
 -tc_ax_branch :: [CoAxBranch] -> IfaceAxBranch -> IfL [CoAxBranch]
 -tc_ax_branch prev_branches
 -             (IfaceAxBranch { ifaxbTyVars = tv_bndrs
 +tc_ax_branch :: IfaceAxBranch -> IfL CoAxBranch
 +tc_ax_branch (IfaceAxBranch { ifaxbTyVars = tv_bndrs
                              , ifaxbEtaTyVars = eta_tv_bndrs
                              , ifaxbCoVars = cv_bndrs
                              , ifaxbLHS = lhs, ifaxbRHS = rhs
 -                            , ifaxbRoles = roles, ifaxbIncomps = incomps })
 +                            , ifaxbRoles = roles })
    = bindIfaceTyConBinders_AT
        (map (\b -> Bndr (IfaceTvBndr b) (NamedTCB Inferred)) tv_bndrs) $ \ tvs ->
           -- The _AT variant is needed here; see Note [CoAxBranch type variables] in GHC.Core.Coercion.Axiom
@@ -1135,15 +1128,15 @@ tc_ax_branch prev_branches
      ; this_mod <- getIfModule
      ; let loc = mkGeneralSrcSpan (fsLit "module " `appendFS`
                                    moduleNameFS (moduleName this_mod))
 -          br = CoAxBranch { cab_loc     = loc
 -                          , cab_tvs     = binderVars tvs
 -                          , cab_eta_tvs = eta_tvs
 -                          , cab_cvs     = cvs
 -                          , cab_lhs     = tc_lhs
 -                          , cab_roles   = roles
 -                          , cab_rhs     = tc_rhs
 -                          , cab_incomps = map (prev_branches `getNth`) incomps }
 -    ; return (prev_branches ++ [br]) }
 +    ; return (CoAxBranch { cab_loc      = loc
 +                         , cab_tvs      = binderVars tvs
 +                         , cab_eta_tvs  = eta_tvs
 +                         , cab_cvs      = cvs
 +                         , cab_lhs      = tc_lhs
 +                         , cab_roles    = roles
 +                         , cab_rhs      = tc_rhs
 +                         , cab_overlaps = placeHolderOverlaps
 +                         , cab_incomps  = placeHolderIncomps }) }
  tcIfaceDataCons :: Name -> TyCon -> IfaceConDecls -> IfL AlgTyConRhs
  tcIfaceDataCons tycon_name tycon if_cons

compiler/GHC/Tc/Instance/FunDeps.hs

@@ -136,10 +136,10 @@ data FunDepEqns  -- Plural becuase fd_eqs has multiple equations
                                   --   to fresh unification vars,
                                   -- See (IMP2) in Note [Improving against instances]
 -           , fd_eqs   :: [TypeEqn]  -- Make these pairs of types equal
 -                                   -- Invariant: In each (Pair ty1 ty2), the fd_qtvs may be
 -                                   -- free in ty1 but not in ty2.  See Wrinkle (1) of
 -                                   -- Note [Improving against instances]
 +           , fd_eqs  :: [TypeEqn]  -- Make these pairs of types equal
 +                        -- Invariant: In each (Pair ty1 ty2), the fd_qtvs may be
 +                        -- free in ty1 but not in ty2.  See Wrinkle (1) of
 +                        -- Note [Improving against instances]
+            }
  instance Outputable FunDepEqns where

compiler/GHC/Tc/Solver/FunDeps.hs

@@ -26,20 +26,23 @@ import GHC.Core.Coercion
  import GHC.Core.TyCo.Rep( Type(..) )
  import GHC.Core.Predicate( EqRel(..) )
  import GHC.Core.TyCon
 -import GHC.Core.Unify( tcUnifyTysForInjectivity, typeListsAreApart )
 +import GHC.Core.Unify( AmIUnifying(..)
 +                     , tcUnifyTysForInjectivity, typeListsAreApart )
  import GHC.Core.Coercion.Axiom
 -import GHC.Core.TyCo.Subst( elemSubst )
 +import GHC.Core.TyCo.Subst( elemSubst, extendTvSubstWithClone )
  import GHC.Builtin.WiredIn.TypeLits( tryInteractTopFam, tryInteractInertFam )
 +import GHC.Types.Var( TyVar, tyVarKind, setTyVarKind )
  import GHC.Types.Var.Set
 +import GHC.Types.Var.Env( mkInScopeSet )
  import GHC.Utils.Outputable
  import GHC.Utils.Panic
  import Control.Monad( unless )
  import GHC.Data.Pair
 -import Data.Maybe( isNothing, isJust, mapMaybe )
 +import Data.Maybe( isJust, mapMaybe )
  {- Note [Overview of functional dependencies in type inference]
@@ -109,7 +112,6 @@ Wrinkles
    from fundeps, but that would require new evidence forms, and an extension to
    FC, so we don't do that right now (Dec 14).
+-
  Note [FunDep and implicit parameter reactions]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  Currently, our story of interacting two dictionaries (or a dictionary
@@ -573,6 +575,7 @@ tryEqFunDeps work_item@(EqCt { eq_lhs = work_lhs
  tryFamEqFunDeps :: TcSMode -> [EqCt] -> TyCon -> [TcType] -> EqCt -> SolverStage ()
 +-- See Note [Type inference for type families with injectivity]
  tryFamEqFunDeps mode eqs_for_me fam_tc work_args
                  work_item@(EqCt { eq_ev = ev, eq_rhs = work_rhs })
    | Just ops <- builtInClosedTyFamTyCon_maybe fam_tc
@@ -583,6 +586,7 @@ tryFamEqFunDeps mode eqs_for_me fam_tc work_args
              ; tryFDEqns False fam_tc work_args work_item eqns
              ; unless (hasRelevantGiven eqs_for_me work_args work_item) $
 +              -- hasRelevantGiven: See (CF1) in Note [Exploiting closed type families]
                do { eqns <- mkTopBuiltinFamEqFDs fam_tc ops work_args work_rhs
                   ; tryFDEqns True fam_tc work_args work_item eqns } }
@@ -599,8 +603,11 @@ tryFamEqFunDeps mode eqs_for_me fam_tc work_args
             NotInjective  -> nopStage ()
             Injective inj -> do { eqns <- mkLocalFamEqFDs eqs_for_me fam_tc inj work_args work_rhs
                                 ; tryFDEqns False fam_tc work_args work_item eqns }
 +         -- NB: tryFDEqns bales out on an insoluble fundep
 +         -- See (CF4) in Note [Exploiting closed type families]
         ; unless (hasRelevantGiven eqs_for_me work_args work_item) $
 +         -- hasRelevantGiven: See (CF1) in Note [Exploiting closed type families]
           do { eqns <- mkTopFamEqFDs fam_tc work_args work_item
              ; tryFDEqns True fam_tc work_args work_item eqns } }
@@ -638,10 +645,11 @@ tryFDEqns is_top fam_tc work_args work_item@(EqCt { eq_ev = ev, eq_rhs= rhs }) f
  --  User-defined type families
  -----------------------------------------
  mkTopClosedFamEqFDs :: CoAxiom Branched -> [TcType] -> EqCt -> SolverStage [FunDepEqns]
 +-- Implements (INJFAM:Wanted/top-closed)
 +-- See Note [Exploiting closed type families]
  -- Look at the top-level axioms; we effectively infer injectivity,
 --- so we don't need tyConInjectivtyInfo.  This works fine for closed
 +-- so we don't need tyConInjectivityInfo.  This works fine for closed
  -- type families without injectivity info
 --- See Note [Exploiting closed type families]
  mkTopClosedFamEqFDs ax work_args (EqCt { eq_ev = ev, eq_rhs = work_rhs })
    | isGenerativeType work_rhs -- See (CF5) in Note [Exploiting closed type families]
    = Stage $
@@ -679,39 +687,46 @@ hasRelevantGiven eqs_for_me work_args (EqCt { eq_rhs = work_rhs })
      relevant (EqCt { eq_ev = ev, eq_lhs = lhs, eq_rhs = rhs_ty })
         | isGiven ev
         , TyFamLHS _ lhs_tys <- lhs
 -       = isJust (tcUnifyTysForInjectivity True work_tys (rhs_ty:lhs_tys))
 +       = isJust (tcUnifyTysForInjectivity Unifying work_tys (rhs_ty:lhs_tys))
         | otherwise
         = False
  getRelevantBranches :: CoAxiom Branched -> [TcType] -> Xi -> [FunDepEqns]
  -- Return the FunDepEqns that arise from each relevant branch
 +-- Implements Note [Relevance]
  getRelevantBranches ax work_args work_rhs
 -  = go [] (fromBranches (coAxiomBranches ax))
 +  = go (fromBranches (coAxiomBranches ax))
    where
      work_tys = work_rhs : work_args
 -    go _ [] = []
 -    go preceding (branch:branches)
 +    go [] = []
 +    go (branch:branches)
        = case is_relevant branch of
 -          Just eqn -> eqn : go (branch:preceding) branches
 -          Nothing  ->       go (branch:preceding) branches
 +          Just eqn -> eqn : go branches
 +          Nothing  ->       go branches
        where
 -         is_relevant (CoAxBranch { cab_tvs = qtvs, cab_lhs = lhs_tys, cab_rhs = rhs_ty })
 -            | Just subst <- tcUnifyTysForInjectivity True (rhs_ty:lhs_tys) work_tys
 -            , let (subst', qtvs') = trim_qtvs subst qtvs
 -                  lhs_tys' = substTys subst' lhs_tys
 -                  rhs_ty'  = substTy  subst' rhs_ty
 -            , all (no_match lhs_tys') preceding
 +         is_relevant branch@(CoAxBranch { cab_tvs = qtvs
 +                                        , cab_lhs = lhs_tys
 +                                        , cab_rhs = rhs_ty })
 +            | Just subst <- tcUnifyTysForInjectivity Unifying (rhs_ty:lhs_tys) work_tys
 +              -- See (RW1)-(RW3) in Note [Relevance]
 +              -- This is a pre-/unification/ check (not matching)
 +              -- so `subst` can bind both `qtvs` and fvs(work_tys)
 +            , let (subst',qtvs') = trim_qtvs subst qtvs
 +                  lhs_tys'       = substTys subst' lhs_tys
 +                  rhs_ty'        = substTy  subst' rhs_ty
 +                  branch_tys'    = rhs_ty' : lhs_tys'
 +            , noEarlierMatchCheck lhs_tys' branch  -- See (RW4) in Note [Relevance]
              = Just (FDEqns { fd_qtvs = qtvs'
 -                           , fd_eqs = zipWith Pair (rhs_ty':lhs_tys') work_tys })
 +                           , fd_eqs  = zipWith Pair branch_tys' work_tys })
 +                              -- Do not apply the substition to `work_tys`;
 +                              -- See (CF7) in Note [Exploiting closed type families]
              | otherwise
              = Nothing
 -         no_match lhs_tys (CoAxBranch { cab_lhs = lhs_tys1 })
 -            = isNothing (tcUnifyTysForInjectivity False lhs_tys1 lhs_tys)
+-
  mkTopOpenFamEqFDs :: TyCon -> [Bool] -> [TcType] -> EqCt -> TcS [FunDepEqns]
 --- Implements (INJFAM:Wanted/top)
 +-- Implements (INJFAM:Wanted/top-open)
 +-- See Note [Exploiting open type families]
  mkTopOpenFamEqFDs fam_tc inj_flags work_args (EqCt { eq_rhs = work_rhs })
    = do { fam_envs <- getFamInstEnvs
         ; let branches :: [CoAxBranch]
@@ -720,15 +735,15 @@ mkTopOpenFamEqFDs fam_tc inj_flags work_args (EqCt { eq_rhs = work_rhs })
         ; return (mapMaybe do_one branches) }
    where
      do_one :: CoAxBranch -> Maybe FunDepEqns
 -    do_one branch@(CoAxBranch { cab_tvs = branch_tvs
 -                              , cab_lhs = branch_lhs_tys
 -                              , cab_rhs = branch_rhs })
 -      | Just subst <- tcUnifyTysForInjectivity False [branch_rhs] [work_rhs]
 -                      -- False: matching, not unifying
 -      , let (subst', qtvs) = trim_qtvs subst branch_tvs
 +    do_one (CoAxBranch { cab_tvs = branch_qtvs
 +                       , cab_lhs = branch_lhs_tys
 +                       , cab_rhs = branch_rhs })
 +      | Just subst <- tcUnifyTysForInjectivity Matching [branch_rhs] [work_rhs]
 +      , let (subst', qtvs') = trim_qtvs subst branch_qtvs
              branch_lhs_tys' = substTys subst' branch_lhs_tys
 -      , apartnessCheck branch_lhs_tys' branch  -- See (TIF3)
 -      = Just (mkInjectivityFDEqn inj_flags qtvs branch_lhs_tys' work_args)
 +        -- No need for an apartness check here; for open type families
 +        -- there are no "preceding" equations
 +      = Just (mkInjectivityFDEqn inj_flags qtvs' branch_lhs_tys' work_args)
        | otherwise
        = Nothing
@@ -736,7 +751,7 @@ mkTopOpenFamEqFDs fam_tc inj_flags work_args (EqCt { eq_rhs = work_rhs })
  mkLocalFamEqFDs :: [EqCt] -> TyCon -> [Bool] -> [TcType] -> Xi -> SolverStage [FunDepEqns]
  -- Wanted constraints only
  -- Both open and closed type families, but only ones with declared injectivity
 --- See Note [Type inference for type families with injectivity] esp (TIF2)
 +-- See Note [Exploiting local type-family injectivity]
  mkLocalFamEqFDs eqs_for_me fam_tc inj_flags work_args work_rhs
    = do { let -- eqns_from_inerts: see (INJFAM:Wanted/other)
               eqns_from_inerts = mapMaybe do_one eqs_for_me
@@ -755,15 +770,27 @@ mkLocalFamEqFDs eqs_for_me fam_tc inj_flags work_args work_rhs
      mk_eqn iargs = mkInjectivityFDEqn inj_flags [] work_args iargs
 -trim_qtvs :: Subst -> [TcTyVar] -> (Subst,[TcTyVar])
 --- Tricky stuff: see (TIF1) in
 --- Note [Type inference for type families with injectivity]
 -trim_qtvs subst []       = (subst, [])
 -trim_qtvs subst (tv:tvs)
 -  | tv `elemSubst` subst = trim_qtvs subst tvs
 -  | otherwise            = let !(subst1, tv')  = substTyVarBndr subst tv
 -                               !(subst', tvs') = trim_qtvs subst1 tvs
 -                           in (subst', tv':tvs')
 +trim_qtvs :: Subst -> [TyVar] -> (Subst, [TyVar])
 +-- Tricky stuff: see (OF1) in Note [Exploiting open type families]
 +trim_qtvs unif_subst qtvs
 +  = go unif_subst qtvs
 +  where
 +    go :: Subst -> [TyVar] -> (Subst, [TyVar])
 +    go subst [] = (subst, [])
 +    go subst (tv:tvs)
 +       | tv `elemSubst` unif_subst = go subst tvs
 +       | otherwise                 = go_fresh subst tv tvs
++
 +    -- Using an auxiliary function here to avoid prematurely forcing
 +    -- the (banged) recursive call to `go` in the non-fresh case
 +    go_fresh subst tv tvs = (subst'', tv':tvs')
 +      where
 +        !(subst'', tvs') = go subst' tvs
 +        tv'    = tv `setTyVarKind` substTy subst (tyVarKind tv)
 +        subst' = extendTvSubstWithClone subst tv tv'
 +                 -- extendTvSubstWithClone: see (OF1b) in
 +                 -- Note [Exploiting open type families]
++
  -----------------------------------------
  --  Built-in type families
@@ -924,15 +951,20 @@ we attempt to exploit injectivity, via `mkLocalFamEqFDs`:
  * (INJFAM:Wanted/other) see `mkLocalFamEqFDs`
      work item: [W]   F s1 s2 ~ rhs   -- Wanted
      inert:     [G/W] F t2 t2 ~ rhs   -- Same `rhs`, Given or Wanted
 -  We can generate FunDepEqns: (s2 ~ t2)
 +  See Note [Exploiting local type-family injectivity]
++
 +* (INJFAM:Wanted/top-open) for open type families: `mkTopOpenFamEqFDs`
 +    type family F a b = r | r -> b
 +    type instance F Int (Maybe a) = [G Int]   -- G is a type family
 +    [W] F alpha beta = [ty]
 +  We can generate (Maybe gamma ~ beta)
 +  See Note [Exploiting open type families]
 -* (INJFAM:Wanted/top) see `mkTopUserFamEqFDs`
 -    work item: [W] F s1 s2 ~ rhs
 -    type instance forall a b c. F t1 t2 ~ top_rhs
 -  and we can /match/ the LHS, so that
 -     S(top_rhs) = rhs
 -  then we can generate the FunDepEqns:  forall a c. s2 ~ S(t2)
 -  But see wrinkle (TIF1), (TIF3)
 +* (INJFAM:Wanted/top-closed) for closed type families: `mkTopClosedFamEqFDs`
 +    type family F a b where { ...eqns... }
 +    [W] F alpha ~ Int
 +  We may be able to generate some extra equalities to constraint `alpha`
 +  See very clever Note [Exploiting closed type families]
  For /built-in/ type families, it's pretty similar, except that
@@ -945,45 +977,36 @@ For /built-in/ type families, it's pretty similar, except that
     * mkLocalBuiltinFamEqFDs
     * mkTopBuiltinFamEqFDs
 -(TIF1) Generating fundeps from a top-level type instance is covered in
 -  Section 5.2 in the Injective Type Families paper. It's a bit tricky.
 -  Consider
 -     type family F @k (a::k) (b::k) = r | r -> k b
 -     type instance forall k (a::k) (b::k). F @k (Proxy @k a) (Proxy @k b) = Proxy @k a
 -     [W] F @kappa alpha beta ~ Maybe (Proxy @kappa (delta::kappa))
+-
 -  we match (Proxy @kappa delta) against the template (Proxy k a), succeeding
 -  with substitution [k:->kappa, a:->delta].  We want to generate this FunDepEqns
 -    FDEqn { fd_qtvs = [b:kappa], fd_eqs = [ beta ~ Proxy @kappa b ] }
 -  Notice that
 -    * we must quantify the FunDepEqns over `b`, which is not matched; for this
 -      we will generate a fresh unification variable in `instantiateFunDepEqn`.
 -    * we must substitute `k:->kappa` in the kind of `b`.
 -  This fancy footwork for `fd_qtvs` is done by `trim_qtvs` in
 -  `mkInjWantedFamEqTopEqns`.
+-
 -(TIF2) All this applies equally to /closed/ type families; it is /not/
 -  subsumed by Note [Exploiting closed type families].  Consider:
 +Note [Exploiting local type-family injectivity] see `mkLocalFamEqFDs`
 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 +Suppose we have a type family with declared injectivity:
 +    type family F a b = r | r -> b
 +and we have
 +    work item: [W] F s1 s2 ~ F t1 t2
 +or
 +    work item: [W]   F s1 s2 ~ rhs   -- Wanted
 +    inert:     [G/W] F t2 t2 ~ rhs   -- Same `rhs`, Given or Wanted
++
 +Then we can generate FunDepEqns: (s2 ~ t2)
++
 +This applies equally to /closed/ type families; it is /not/ subsumed
 +by Note [Exploiting closed type families].  Consider:
++
        type family F a | r -> a where { .... }
        [W] F t1 ~ a
        [W] F t2 ~ a
 -  Then since F is declared injective, we can generate t1~t2.
 +Then since F is declared injective, we can generate t1~t2.
 -  As for open type families, we insist on /user-declared/ injectivity only; we
 -  don't try to /infer/ injectivity even for a closed family.  See Section 3.4
 -  of the "Injective type families" paper.  (Arguably, we could /infer/
 -  injectivity for closed type families, and that would be more in the spirit of
 -  Note [Exploiting closed type families].)
 +As for open type families, we insist on /user-declared/ injectivity only; we
 +don't try to /infer/ injectivity even for a closed family.  See Section 3.4
 +of the "Injective type families" paper.  (Arguably, we could /infer/
 +injectivity for closed type families, and that would be more in the spirit of
 +Note [Exploiting closed type families].)
 -(TIF3) Further to (TIF1), if we are considering a /closed/ type family, we
 -  must ensure (see Section 5.2 of the paper) that after matching that
 -  equation would indeed be the one to fire.  So we call `apartnessCheck`
 -  on the branch to ensure this, in `mkTopUserFamEqFDs`.
+-
 -Definition [Relevance]
 -~~~~~~~~~~~~~~~~~~~~~~
 +Note [Relevance]
 +~~~~~~~~~~~~~~~~
  We say that a closed-type-family equation `F lhs = rhs` is
     /relevant/ for a Wanted [W] F wlhs ~ wrhs
  iff
@@ -992,6 +1015,10 @@ iff
    (R2) There is no earlier equation that matches S(lhs).  See (RW4) below.
 +The relevance check is implemented by `getRelevantBranches`, which actually
 +returns the [FunDepEqns] described in the Closed Family Fundep Algorithm in
 +Note [Exploiting closed type families].
++
  (RW1) Pre-unification treats type-family applications as binding to anything,
      rather like type variables.  If two types don't even pre-unify, we say that they
      are /apart/.  It is done by `tcUnifyTysForInjectivity`.
@@ -1014,24 +1041,130 @@ iff
      Clearly the RHS is apart from the first equation and we want to fire injectivity
      on the second equation.
 -(RW4) Why "no earlier equation matches" in conditoin (R2)?  Consider the family
 +(RW4) Why "no earlier equation matches" in condition (R2)?  Consider the family
            type family Bak a = r where
               Bak Int  = Char   -- B1
               Bak Char = Int    -- B2
               Bak a    = a      -- B3
 -    and [W] Bak alpha ~ Char. In fact, only (B2) is relevant for this Wanted.
 +    and [W] Bak alpha ~ Char. In fact, only (B1) is relevant for this Wanted.
      You might think that (B3) could be instantiated to Bak Char ~ Char; but
      actually that instantiation will never fire because (B2) Bak Char ~ Int would
 -    fire first.  So the only way to return a Char is if the argment is Int; so we
 -    can emit [W] alpha ~ Int.  Hence (B3) is not relevant; only (B2) is relevant.
 +    fire first.  So the only way to return a Char is via (B1); so we
 +    can emit [W] alpha ~ Int.  Hence (B3) is not relevant; only (B1) is relevant.
      That is the reason for condition (R2) in the definition of Relevance above.
      A watertight proof that this is the Right Thing is not very easy.  See more
 -    discussion in #23162.
+-
 -Note [Exploiting closed type families]
 +    discussion in #23162, and Section 5.2 of the paper.
++
 +    How, precisely, do we implement (R2)? We check that there is no earlier equation
 +    that fires on S(lhs), in this case (on Bak Char).  Notice that this is different
 +    from the `apartnessCheck`, which checks that all preceding equations are apart
 +    from S(lhs).  Apartness checking uses /unification/; here we want /matching/.
 +    Hence using `noEarlierMatchCheck`, not `apartnessCheck`.
++
 +    Here's a good example from T27171_aux. T
 +       type family TMessage m where
 +         {- T1 -} TMessage @f @t   (CustomMethod s :: Method f t) = ()
 +         {- T2 -} TMessage @f @Req (m :: Method f Req)            = TRequestMessage m
 +         {- T3 -} TMessage @f @Not (m :: Method f Not)            = TNotificationMessage m
++
 +       [W] TMessage @SC @Req alpha  ~# TRequestMessage alpha
++
 +    There is only one relevant equation, namely (T2).  If we apply its
 +    pre-unification substitution [f :-> SC, m :-> alpha] to its LHS we get
 +         TMessage @SC @Req alpha
 +    and equation (T1) does not match that. (It does unify, but we don't care.)
++
 +(RW5) `noEarlierMatchCheck`: in (RW4) We really do need to check that /no/
 +    earlier equation matches, not just no earlier /incompatible/ equation
 +    matches.  Consider T27828a:
 +        type family F a where
 +          F Int  = Int  -- B1
 +          F Char = Bool -- B2
 +          F a    = a    -- B3
++
 +        [W] F alpha ~ Int
++
 +    (B1) is relevant, and (B2) is not. What about (B3)?  It pre-unifies with
 +    the Wanted via [alpha :-> Int, a :-> Int].  But under that substitution
 +    (B1) would fire, so (B3) is not relevant.
++
 +    And yet, (B1) is /compatible/ with (B3), so it's no good just looking at
 +    the `cab_incomps` of (B3).  Instead we look at `cab_overlaps`.
++
 +Note [Exploiting open type families] see `mkTopOpenFamEqFDs`
 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 +Generating fundeps from a top-level type instance is covered in Section 5.2 in
 +the Injective Type Families paper. For open type families, suppose we have
++
 +   type family F a = r | r -> a
 +   type instance F [a] = a->a
++
 +   [W] F alpha ~ Int->Int
++
 +Then, since F has been checked as injective, and the RHS `a->a` (pre-)unifies
 +with the `Int->Int` in the Wanted with substitution [a :-> Int], we can
 +add a derived FunDepEqns
 +   FDEqns{ fd_qtvs = [], fd_eqs = [ [Int] ~ alpha ] }
 +and thereby emit (via `instantiateFunDepEqns`)
 +   [W] [Int] ~ alpha
++
 +Things are a bit trickier when not all the quantified variables of the
 +instance are bound by the pre-unification step.  Suppose we have
++
 +   type family F a = r | r -> a
 +   type instance F (Maybe a) = [G a]   -- G is a type family
++
 +   [W] F alpha ~ [ty]
++
 +Then, the RHS [G a] pre-unifies with the RHS of the Wanted, but with an
 +empty substitution, which does not fix `a`.  So we get this FunDepEqns:
 +   FDEqns{ fd_qtvs = a, fd_eqs = [ Maybe a ~ alpha ] }
 +(note the fd_qtvs=a) and thereby emit (via `instantiateFunDepEqns`)
 +   [W] Maybe gamma ~ alpha    -- Fresh gamma
 +We have learned that `alpha` must be a list, but that is all; we don't
 +know what is inside it, hence the fresh `gamma`.
++
 +In general we have:
++
 +  type family F x1 ... xn = r | r -> x1 x3     (say)
 +  type instance forall qs. F t1 ... tn = rhs
 +  [W] F a1 ... an ~ b
++
 +Suppose `b` pre-unifies with `rhs`, with substitution `S` that binds
 +some (but perhaps not all) of the `qs`.  Lets say
 +   unbound_qs = qs \ dom(S)
++
 +Then we generate the FunDepEqs
 +   FDEqns{ fd_qtvs = unbound_qs
 +         , fd_eqs = [ S(t1) ~ S(a1), S(t3) ~ S(a3) ]
++
 +These 'fd_qtvs' are subsequently instantiated to fresh metavariables by
 +'instantiateFunDepEqns'.
++
 +(OF1) The computation of `unbound_qs` is done by `trim_qtvs`, but we
 +   have to be careful.   Suppose (OF1a)
 +       qs = [ k::*, a::k ]
 +       S  = [ k :-> UnliftedType ]
 +   Then we want
 +       unbound_qs = [ a::UnliftedType ]    -- Must apply S to q's kind!!
++
 +   And (OF1b), although I'm not sure if this can acutally happen:
 +        qs = [ k::*, a::(k::*), b::(a::k) ]
 +        S  = [ k :-> UnliftedType ]
 +   We want
 +        unbound_qs = [ a::UnliftedType, b::(a::UnliftedType) ]
 +   Note that the occurrence of `a` in b's kind should be replaced by the
 +   newly-kinded `a` not the original `a::k`.
++
 +   This fancy footwork for `fd_qtvs` is done by `trim_qtvs`.  It
 +    * Drops a quantified tyvar that /is/ matched
 +    * Substitutes in the kind of a quantified tyvar `a` that is /not/ matched
 +    * Adds the substitution [a::k :-> a::S(k)] to the substitution
++
 +Note [Exploiting closed type families] see `mkTopClosedFamEqFDs`
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  Suppose we have
      type family F a b where
@@ -1042,17 +1175,18 @@ Suppose we have
      [W]  F Int alpha ~ Char
  The /only/ way to solve this Wanted is using (F2), so we can safely unify
 -alpha:=Char without risking losing any solutions.  That is what
 -`mkTopClosedFamEqFDs` does.  Ticket #23162 has lots of background detail
 +alpha:=Char without risking losing any solutions.  We don't even need any
 +injectivity annotations. Ticket #23162 has lots of background detail.
 -More precisely, here is the Closed Family Fundep Algorithm (CFFA)
 +More precisely, here is the very clever Closed Family Fundep Algorithm (CFFA)
      IF * F a is a closed type family.
         * We are trying to solve [W] F wlhs ~ wrhs.
 -       * There are no "relevant" Givens [G] F lhs ~ rhs.  See (CF1) below.
 -       * F  has exactly one equation, F lhs = rhs that is "relevant" for that Wanted
 +       * There are no "relevant Givens" [G] F lhs ~ rhs.  See (CF1) below.
 +       * F  has exactly one equation, F lhs = rhs that is "relevant" for
 +         that Wanted (see Note [Relevance])
      THEN
 -      we can emit and solve the fundep equalities:
 +      we can emit and solve the fundeps :: [FunDepEqns]:
            [W] wlhs1 ~ lhs1
            ...
            [W] wlhsn ~ lhsn
@@ -1060,7 +1194,10 @@ More precisely, here is the Closed Family Fundep Algorithm (CFFA)
      with fresh unification vars in lhs and rhs for the quantified variables of the
      equation.
 -See Definition [Relevance] for what "relevant" means.
 +    Actually we take advantage of the substitution generated by the relevance
 +    check, see (CF7) below.
++
 +See Note [Relevance] for what "relevant" means.
  We need to take care about non-termination; see (CF3).
  Key point: equations that are not relevant do not need to be considered for fundeps at all.
@@ -1166,6 +1303,8 @@ Key point: equations that are not relevant do not need to be considered for fund
    I was looking at non-termination for closed type families, but it's a small
    improvement in general.
 +  This bale-out is implementedn in `tryFDEqns`.
++
  (CF5) Consider (see "Yikes5" in #23162):
        type family F a where
           F (Just x) = Int
@@ -1196,7 +1335,7 @@ Key point: equations that are not relevant do not need to be considered for fund
        type family I t = res | res -> t where
          I TInt = Int |> g    -- where g :: Type ~# IK k
    and [W] I alpha ~ Int |> g2
 -  Here we definiteily want to take advantage of injectivity.
 +  Here we definitely want to take advantage of injectivity.
  (CF6) This machinery can also have a significant positive effect on the size of
    proof terms. For example (simplification of T26426):
@@ -1204,7 +1343,8 @@ Key point: equations that are not relevant do not need to be considered for fund
        type family (++) a b where { '[] ++ ys = ys; (x:xs) ++ ys = x : (xs ++ ys) }
        type family MapId a where { MapId '[] = '[]; MapId (x:xs) = x : MapId xs }
 -      app :: (MapId xs ++ MapId ys ~ MapId (xs ++ ys)) => Proxy xs -> Proxy ys -> Proxy (xs ++ ys)
 +      app :: (MapId xs ++ MapId ys ~ MapId (xs ++ ys))
 +          => Proxy xs -> Proxy ys -> Proxy (xs ++ ys)
        test :: Proxy [ty_1, ..., ty_n]
        test =   Proxy @'[ty_1]
@@ -1248,6 +1388,30 @@ Key point: equations that are not relevant do not need to be considered for fund
    instead of relying on recursively built sub-proof terms, which brings down
    coercion sizes (in certain situations) from O(n^3) to O(n^2).
 +(CF7) Relevance.  When computing relevance in the Closed Family Fundep Algorithm,
 +  for [W] F wlhs1 wlhs2 ~ wrhs, against an equation   F lhs1 lhs2 ~ rhs
 +  we get back a pre-unifying substitution S that makes the two as equal as poss.
 +  Then we use `trim_qtvs` in exactly the same way as in
 +       (OF1) of Note [Exploiting open type families], to generate qtvs' and S'
 +  Then we generate
 +      FDEqns { fd_qtvs = qtvs', fd_eqs [ S'(lhs1) ~ wlhs1
 +                                       , S'(lhs2) ~ wlhs2
 +                                       , S'(rhs)  ~ wrhs ] }
 +  Notice that we do /not/ apply S' to wlhs/wrhs.  These type contain unification
 +  variables that we must actually unify! Example
 +     type family F a b where
 +       F [a] (Maybe b) = (a,  G b)
 +     [W] F alpha beta ~ (Int, [gamma])
 +  Pre-unification gives [alpha :-> [a], beta :-> Maybe b, a :-> Int]
 +  This substitution eliminates the quantified variable `a` but not `b`, so we
 +  want this:
 +     FDEqns { fd_qtvs = [b], fd_eqs [ [Int] ~ alpha
 +                                    , Maybe b ~ beta
 +                                    , (Int,G b) ~ (Int, [gamma]) ] }
++
 +  Notice also that by applying the substitution to the template but not to the
 +  Wanted, we uphold the `fd_eqs` invariant in `FDEqns` (see its data type decl)
++
  Note [Cache-caused loops]
  ~~~~~~~~~~~~~~~~~~~~~~~~~
  It is very dangerous to cache a rewritten wanted family equation as 'solved' in
@@ -1340,28 +1504,34 @@ solveFunDeps work_ev fd_eqns
                           ; uPairsTcM uenv eqs }
  instantiateFunDepEqns :: FunDepEqns -> TcM [TypeEqn]
 -instantiateFunDepEqns (FDEqns { fd_qtvs = tvs, fd_eqs = eqs })
 -  | null tvs
 +-- See GHC.Tc.Instance.Fundeps Note [Improving against instances]
 +--     Wrinkle (IMP1)
 +instantiateFunDepEqns (FDEqns { fd_qtvs = qtvs, fd_eqs = eqs })
 +  | null qtvs
    = return rev_eqs
    | otherwise
 -  = do { TcM.traceTc "instantiateFunDepEqns" (ppr tvs $$ ppr eqs)
 -       ; (_, subst) <- instFlexiXTcM emptySubst tvs  -- Takes account of kind substitution
 +  = do { TcM.traceTc "instantiateFunDepEqns" (ppr qtvs $$ ppr eqs)
 +       ; (_, subst) <- instFlexiXTcM empty_subst qtvs  -- Takes account of kind substitution
         ; return (map (subst_pair subst) rev_eqs) }
    where
      rev_eqs = reverse eqs
         -- (reverse eqs): See Note [Reverse order of fundep equations]
 +    -- The kinds of `qtvs` can have free variables, because of `trim_qtvs`
 +    -- Example: T27828b
 +    empty_subst = mkEmptySubst $ mkInScopeSet $
 +                  tyCoVarsOfTypes (map tyVarKind qtvs)
++
      subst_pair subst (Pair ty1 ty2)
 -       = Pair (substTyUnchecked subst' ty1) ty2
 -              -- ty2 does not mention fd_qtvs, so no need to subst it.
 -              -- See GHC.Tc.Instance.Fundeps Note [Improving against instances]
 -              --     Wrinkle (1)
 +       = Pair (substTy subst' ty1) ty2
 +         -- NB: ty2 does not mention fd_qtvs, so no need to subst it.
 +         --     See invariant on `fv_eqs` in `data FunDepEqns`.
         where
           subst' = extendSubstInScopeSet subst (tyCoVarsOfType ty1)
                    -- The free vars of ty1 aren't just fd_qtvs: ty1 is the result
                    -- of matching with the [W] constraint. So we add its free
                    -- vars to InScopeSet, to satisfy substTy's invariants, even
 -                  -- though ty1 will never (currently) be a poytype, so this
 +                  -- though ty1 will never (currently) be a polytype, so this
                    -- InScopeSet will never be looked at.

compiler/GHC/Tc/TyCl.hs

@@ -3462,7 +3462,7 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info
         ; let mb_co_ax
                | null eqns = Nothing   -- mkBranchedCoAxiom fails on empty list
 -              | otherwise = Just (mkBranchedCoAxiom co_ax_name fam_tc branches)
 +              | otherwise = Just (mkBranchedCoAxiom Nominal co_ax_name fam_tc branches)
               fam_tc = mkFamilyTyCon tc_name kind tc_bndrs 0 res_kind (resultVariableName sig)
                        (ClosedTypeFamilyTyCon $ CTF mb_co_ax) parent inj'

testsuite/tests/indexed-types/should_compile/T27828.hs

 +{-# LANGUAGE DataKinds #-}
 +{-# LANGUAGE TypeAbstractions #-}
 +{-# LANGUAGE TypeFamilies #-}
 +{-# LANGUAGE UndecidableInstances #-}
 +module Bug where
++
 +import Data.Functor.Identity (Identity(..))
 +import Data.Kind (Type)
 +import Data.Proxy (Proxy(..))
 +import Data.Type.Equality ((:~:)(..))
++
 +type TyFun :: Type -> Type -> Type
 +data TyFun a b
++
 +type (~>) :: Type -> Type -> Type
 +type a ~> b = TyFun a b -> Type
 +infixr 0 ~>
++
 +type Apply :: (k1 ~> k2) -> k1 -> k2
 +type family Apply f x
++
 +type Rep1 :: (k -> Type) -> k -> Type
 +type family Rep1 f
++
 +type To1 :: Rep1 f a -> f a
 +type family To1 z
++
 +type Par1 :: Type -> Type
 +newtype Par1 p = Par1 p
++
 +type To1Sym0 :: forall k (f :: k -> Type) (a :: k). Rep1 f a ~> f a
 +data To1Sym0 z
++
 +applyTo1Sym0 :: forall k (f :: k -> Type) (a :: k) (x :: Rep1 f a). Proxy x -> Apply @(Rep1 f a) @(f a) To1Sym0 x :~: To1 x
 +applyTo1Sym0 _ = undefined
++
 +type IdentitySym0 :: a ~> Identity a
 +data IdentitySym0 z
 +type instance Apply IdentitySym0 x = 'Identity x
++
 +type Aux :: Rep1 Identity a -> Rep1 Identity a -> Identity a
 +type family Aux x y where
 +  Aux x ('Par1 wombat) = Apply IdentitySym0 wombat
++
 +type instance Rep1 Identity = Par1
 +type instance To1 @Identity y = Aux y y
++
 +lemma :: forall a (z :: a). Apply @(Rep1 Identity a) @(Identity a) To1Sym0 ('Par1 z) :~: 'Identity z
 +lemma = applyTo1Sym0 @Type @Identity @a (Proxy @('Par1 z))
 +-- lemma = applyTo1Sym0 @Type @Identity @a @('Par1 z) (Proxy @('Par1 z))

testsuite/tests/indexed-types/should_compile/T27828a.hs

 +{-# LANGUAGE TypeFamilies #-}
++
 +module T27828a where
++
 +import Data.Proxy
++
 +type family F a where
 +  F Int = Int   -- B1
 +  F Char = Bool -- B2
 +  F a   = a     -- B3
++
 +h :: (F a ~ Int) => Proxy a -> ()
 +h = error "urk"
++
 +k :: ()
 +k = h Proxy      -- [W] F alpha ~ Int

testsuite/tests/indexed-types/should_compile/T27828b.hs

 +{-# LANGUAGE TypeFamilies, KindSignatures, AllowAmbiguousTypes #-}
++
 +module T27828b where
++
 +type family IsJust (m :: Maybe k) :: Bool where
 +  IsJust ('Just x) = 'True
 +  IsJust 'Nothing  = 'False
++
 +f :: forall k (m :: Maybe k). (IsJust m ~ 'True) => Int -> Int
 +f = error "urk"
++
 +g _ = f 3   -- Triggered checkValidSubst error in `instantiateFunDepEqns`o

testsuite/tests/indexed-types/should_compile/all.T

@@ -316,3 +316,6 @@ test('T25611b', normal, compile, [''])
  test('T25611c', normal, compile, [''])
  test('T25611d', normal, compile, [''])
  test('T25657', normal, compile, [''])
 +test('T27828', normal, compile, [''])
 +test('T27828a', normal, compile, [''])
 +test('T27828b', normal, compile, [''])