Fix decomposition of TyConAppswip/T22331

Ticket #22331 showed that we were being too eager to decompose
a Wanted TyConApp, leading to incompleteness in the solver.

To understand all this I ended up doing a substantial rewrite
of the old Note [Decomposing equalities], now reborn as
Note [Decomposing TyConApp equalities]. Plus rewrites of other
related Notes.

The actual fix is very minor and actually simplifies the code: in
`can_decompose` in `GHC.Tc.Solver.Canonical.canTyConApp`, we now call
`noMatchableIrreds`.  A closely related refactor: we stop trying to
use the same "no matchable givens" function here as in
`matchClassInst`.  Instead split into two much simpler functions.

6 files changed, 345 insertions, 227 deletions

diff --git a/compiler/GHC/Core/TyCon.hs b/compiler/GHC/Core/TyCon.hs
index 2a26363c7b..0cbb9ece43 100644
--- a/compiler/GHC/Core/TyCon.hs
+++ b/compiler/GHC/Core/TyCon.hs
@@ -2118,12 +2118,13 @@ isTypeDataTyCon (AlgTyCon {algTcRhs = DataTyCon {is_type_data = type_data }})
 isTypeDataTyCon _              = False
 
 -- | 'isInjectiveTyCon' is true of 'TyCon's for which this property holds
--- (where X is the role passed in):
---   If (T a1 b1 c1) ~X (T a2 b2 c2), then (a1 ~X1 a2), (b1 ~X2 b2), and (c1 ~X3 c2)
--- (where X1, X2, and X3, are the roles given by tyConRolesX tc X)
--- See also Note [Decomposing equality] in "GHC.Tc.Solver.Canonical"
+-- (where r is the role passed in):
+--   If (T a1 b1 c1) ~r (T a2 b2 c2), then (a1 ~r1 a2), (b1 ~r2 b2), and (c1 ~r3 c2)
+-- (where r1, r2, and r3, are the roles given by tyConRolesX tc r)
+-- See also Note [Decomposing TyConApp equalities] in "GHC.Tc.Solver.Canonical"
 isInjectiveTyCon :: TyCon -> Role -> Bool
-isInjectiveTyCon _                             Phantom          = False
+isInjectiveTyCon _ Phantom = True  -- Vacuously; (t1 ~P t2) holes for all t1, t2!
+
 isInjectiveTyCon (AlgTyCon {})                 Nominal          = True
 isInjectiveTyCon (AlgTyCon {algTcRhs = rhs})   Representational
   = isGenInjAlgRhs rhs
@@ -2139,9 +2140,9 @@ isInjectiveTyCon (TcTyCon {})                  _                = True
   -- See Note [How TcTyCons work] item (1) in GHC.Tc.TyCl
 
 -- | 'isGenerativeTyCon' is true of 'TyCon's for which this property holds
--- (where X is the role passed in):
---   If (T tys ~X t), then (t's head ~X T).
--- See also Note [Decomposing equality] in "GHC.Tc.Solver.Canonical"
+-- (where r is the role passed in):
+--   If (T tys ~r t), then (t's head ~r T).
+-- See also Note [Decomposing TyConApp equalities] in "GHC.Tc.Solver.Canonical"
 isGenerativeTyCon :: TyCon -> Role -> Bool
 isGenerativeTyCon (FamilyTyCon { famTcFlav = DataFamilyTyCon _ }) Nominal = True
 isGenerativeTyCon (FamilyTyCon {}) _ = False
diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs
index 10e992467e..2f0af16168 100644
--- a/compiler/GHC/Tc/Solver/Canonical.hs
+++ b/compiler/GHC/Tc/Solver/Canonical.hs
@@ -1073,7 +1073,8 @@ can_eq_nc' _rewritten _rdr_env _envs ev eq_rel
 
 -- See Note [Canonicalising type applications] about why we require rewritten types
 -- Use tcSplitAppTy, not matching on AppTy, to catch oversaturated type families
--- NB: Only decompose AppTy for nominal equality. See Note [Decomposing equality]
+-- NB: Only decompose AppTy for nominal equality.
+--     See Note [Decomposing AppTy equalities]
 can_eq_nc' True _rdr_env _envs ev NomEq ty1 _ ty2 _
   | Just (t1, s1) <- tcSplitAppTy_maybe ty1
   , Just (t2, s2) <- tcSplitAppTy_maybe ty2
@@ -1350,6 +1351,8 @@ zonk_eq_types = go
 
 {- See Note [Unwrap newtypes first]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+See also Note [Decomposing newtype equalities]
+
 Consider
   newtype N m a = MkN (m a)
 Then N will get a conservative, Nominal role for its second parameter 'a',
@@ -1463,7 +1466,7 @@ can_eq_app :: CtEvidence       -- :: s1 t1 ~N s2 t2
 
 -- AppTys only decompose for nominal equality, so this case just leads
 -- to an irreducible constraint; see typecheck/should_compile/T10494
--- See Note [Decomposing AppTy at representational role]
+-- See Note [Decomposing AppTy equalities]
 can_eq_app ev s1 t1 s2 t2
   | CtWanted { ctev_dest = dest, ctev_rewriters = rewriters } <- ev
   = do { co_s <- unifyWanted rewriters loc Nominal s1 s2
@@ -1530,8 +1533,9 @@ canTyConApp :: CtEvidence -> EqRel
             -> TyCon -> [TcType]
             -> TyCon -> [TcType]
             -> TcS (StopOrContinue Ct)
--- See Note [Decomposing TyConApps]
--- Neither tc1 nor tc2 is a saturated funTyCon
+-- See Note [Decomposing TyConApp equalities]
+-- Neither tc1 nor tc2 is a saturated funTyCon, nor a type family
+-- But they can be data families.
 canTyConApp ev eq_rel tc1 tys1 tc2 tys2
   | tc1 == tc2
   , tys1 `equalLength` tys2
@@ -1561,13 +1565,17 @@ canTyConApp ev eq_rel tc1 tys1 tc2 tys2
     ty1 = mkTyConApp tc1 tys1
     ty2 = mkTyConApp tc2 tys2
 
-    loc  = ctEvLoc ev
-    pred = ctEvPred ev
-
-     -- See Note [Decomposing equality]
+     -- See Note [Decomposing TyConApp equalities]
+     -- Note [Decomposing newtypes a bit more aggressively]
     can_decompose inerts
       =  isInjectiveTyCon tc1 (eqRelRole eq_rel)
-      || (ctEvFlavour ev /= Given && isEmptyBag (matchableGivens loc pred inerts))
+      || (assert (eq_rel == ReprEq) $
+          -- assert: isInjectiveTyCon is always True for Nominal except
+          --   for type synonyms/families, neither of which happen here
+          -- Moreover isInjectiveTyCon is True for Representational
+          --   for algebraic data types.  So we are down to newtypes
+          --   and data families.
+          ctEvFlavour ev == Wanted && noGivenIrreds inerts)
 
 {-
 Note [Use canEqFailure in canDecomposableTyConApp]
@@ -1601,219 +1609,329 @@ For example, see typecheck/should_compile/T10493, repeated here:
 That should compile, but only because we use canEqFailure and not
 canEqHardFailure.
 
-Note [Decomposing equality]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~
-If we have a constraint (of any flavour and role) that looks like
-T tys1 ~ T tys2, what can we conclude about tys1 and tys2? The answer,
-of course, is "it depends". This Note spells it all out.
-
-In this Note, "decomposition" refers to taking the constraint
-  [fl] (T tys1 ~X T tys2)
-(for some flavour fl and some role X) and replacing it with
-  [fls'] (tys1 ~Xs' tys2)
-where that notation indicates a list of new constraints, where the
-new constraints may have different flavours and different roles.
-
-The key property to consider is injectivity. When decomposing a Given, the
-decomposition is sound if and only if T is injective in all of its type
-arguments. When decomposing a Wanted, the decomposition is sound (assuming the
-correct roles in the produced equality constraints), but it may be a guess --
-that is, an unforced decision by the constraint solver. Decomposing Wanteds
-over injective TyCons does not entail guessing. But sometimes we want to
-decompose a Wanted even when the TyCon involved is not injective! (See below.)
-
-So, in broad strokes, we want this rule:
-
-(*) Decompose a constraint (T tys1 ~X T tys2) if and only if T is injective
-at role X.
-
-Pursuing the details requires exploring three axes:
-* Flavour: Given vs. Wanted
-* Role: Nominal vs. Representational
-* TyCon species: datatype vs. newtype vs. data family vs. type family vs. type variable
-
-(A type variable isn't a TyCon, of course, but it's convenient to put the AppTy case
-in the same table.)
-
-Here is a table (discussion following) detailing where decomposition of
-   (T s1 ... sn) ~r (T t1 .. tn)
-is allowed.  The first four lines (Data types ... type family) refer
-to TyConApps with various TyCons T; the last line is for AppTy, covering
-both where there is a type variable at the head and the case for an over-
-saturated type family.
-
-NOMINAL               GIVEN        WANTED                         WHERE
-
-Datatype               YES          YES                           canTyConApp
-Newtype                YES          YES                           canTyConApp
-Data family            YES          YES                           canTyConApp
-Type family            NO{1}        YES, in injective args{1}     canEqCanLHS2
-AppTy                  YES          YES                           can_eq_app
-
-REPRESENTATIONAL      GIVEN        WANTED
-
-Datatype               YES          YES                           canTyConApp
-Newtype                NO{2}       MAYBE{2}                canTyConApp(can_decompose)
-Data family            NO{3}       MAYBE{3}                canTyConApp(can_decompose)
-Type family            NO           NO                            canEqCanLHS2
-AppTy                  NO{4}        NO{4}                         can_eq_nc'
-
-{1}: Type families can be injective in some, but not all, of their arguments,
-so we want to do partial decomposition. This is quite different than the way
-other decomposition is done, where the decomposed equalities replace the original
-one. We thus proceed much like we do with superclasses, emitting new Wanteds
-when "decomposing" a partially-injective type family Wanted. Injective type
-families have no corresponding evidence of their injectivity, so we cannot
-decompose an injective-type-family Given.
-
-{2}: See Note [Decomposing newtypes at representational role]
-
-{3}: Because of the possibility of newtype instances, we must treat
-data families like newtypes. See also
-Note [Decomposing newtypes at representational role]. See #10534 and
-test case typecheck/should_fail/T10534.
-
-{4}: See Note [Decomposing AppTy at representational role]
-
-   Because type variables can stand in for newtypes, we conservatively do not
-   decompose AppTys over representational equality. Here are two examples that
-   demonstrate why we can't:
-
-   4a: newtype Phant a = MkPhant Int
-       [W] alpha Int ~R beta Bool
-
-   If we eventually solve alpha := Phant and beta := Phant, then we can solve
-   this equality by unwrapping. But it would have been disastrous to decompose
-   the wanted to produce Int ~ Bool, which is definitely insoluble.
-
-   4b: newtype Age = MkAge Int
-       [W] alpha Age ~R Maybe Int
-
-   First, a question: if we know that ty1 ~R ty2, can we conclude that
-   a ty1 ~R a ty2? Not for all a. This is precisely why we need role annotations
-   on type constructors. So, if we were to decompose, we would need to
-   decompose to [W] alpha ~R Maybe and [W] Age ~ Int. On the other hand, if we
-   later solve alpha := Maybe, then we would decompose to [W] Age ~R Int, and
-   that would be soluble.
-
-In the implementation of can_eq_nc and friends, we don't directly pattern
-match using lines like in the tables above, as those tables don't cover
-all cases (what about PrimTyCon? tuples?). Instead we just ask about injectivity,
-boiling the tables above down to rule (*). The exceptions to rule (*) are for
-injective type families, which are handled separately from other decompositions,
-and the MAYBE entries above.
-
-Note [Decomposing newtypes at representational role]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-This note discusses the 'newtype' line in the REPRESENTATIONAL table
-in Note [Decomposing equality]. (At nominal role, newtypes are fully
-decomposable.)
+Note [Fast path when decomposing TyConApps]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If we see (T s1 t1 ~ T s2 t2), then we can just decompose to
+  (s1 ~ s2, t1 ~ t2)
+and push those back into the work list.  But if
+  s1 = K k1    s2 = K k2
+then we will just decompose s1~s2, and it might be better to
+do so on the spot.  An important special case is where s1=s2,
+and we get just Refl.
 
-Here is a representative example of why representational equality over
-newtypes is tricky:
+So canDecomposableTyConAppOK uses unifyWanted etc to short-cut that work.
 
-  newtype Nt a = Mk Bool         -- NB: a is not used in the RHS,
-  type role Nt representational  -- but the user gives it an R role anyway
+Note [Decomposing TyConApp equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we have
+        [G/W] T ty1 ~r T ty2
+Can we decompose it, and replace it by
+        [G/W] ty1 ~r' ty2
+and if so what role is r'?  (In this Note, all the "~" are primitive
+equalities "~#", but I have dropped the noisy "#" symbols.)  Lots of
+background in the paper "Safe zero-cost coercions for Haskell".
+
+This Note covers the topic for
+  * Datatypes
+  * Newtypes
+  * Data families
+For the rest:
+  * Type synonyms: are always expanded
+  * Type families: see Note [Decomposing type family applications]
+  * AppTy:         see Note [Decomposing AppTy equalities].
+
+---- Roles of the decomposed constraints ----
+For a start, the role r' will always be defined like this:
+  * If r=N then r' = N
+  * If r=R then r' = role of T's first argument
+
+For example:
+   data TR a = MkTR a       -- Role of T's first arg is Representational
+   data TN a = MkTN (F a)   -- Role of T's first arg is Nominal
+
+The function tyConRolesX :: Role -> TyCon -> [Role] gets the argument
+role r' for a TyCon T at role r.  E.g.
+   tyConRolesX Nominal          TR = [Nominal]
+   tyConRolesX Representational TR = [Representational]
+
+---- Soundness and completeness ----
+For Givens, for /soundness/ of decomposition we need, forall ty1,ty2:
+    T ty1 ~r T ty2   ===>    ty1 ~r' ty2
+Here "===>" means "implies".  That is, given evidence for (co1 : T ty1 ~r T co2)
+we can produce evidence for (co2 : ty1 ~r' ty2).  But in the solver we
+/replace/ co1 with co2 in the inert set, and we don't want to lose any proofs
+thereby. So for /completeness/ of decomposition we also need the reverse:
+    ty1 ~r' ty2   ===>    T ty1 ~r T ty2
+
+For Wanteds, for /soundness/ of decomposition we need:
+    ty1 ~r' ty2   ===>    T ty1 ~r T ty2
+because if we do decompose we'll get evidence (co2 : ty1 ~r' ty2) and
+from that we want to derive evidence (T co2 : T ty1 ~r T ty2).
+For /completeness/ of decomposition we need the reverse implication too,
+else we may decompose to a new proof obligation that is stronger than
+the one we started with.  See Note [Decomposing newtype equalities].
+
+---- Injectivity ----
+When do these bi-implications hold? In one direction it is easy.
+We /always/ have
+    ty1 ~r'  ty2   ===>    T ty1 ~r T ty2
+This is the CO_TYCONAPP rule of the paper (Fig 5); see also the
+TyConAppCo case of GHC.Core.Lint.lintCoercion.
+
+In the other direction, we have
+    T ty1 ~r T ty2   ==>   ty1 ~r' ty2  if T is /injective at role r/
+This is the very /definition/ of injectivity: injectivity means result
+is the same => arguments are the same, modulo the role shift.
+See comments on GHC.Core.TyCon.isInjectiveTyCon.  This is also
+the CO_NTH rule in Fig 5 of the paper, except in the paper only
+newtypes are non-injective at representation role, so the rule says "H
+is not a newtype".
+
+Injectivity is a bit subtle:
+                 Nominal   Representational
+   Datatype        YES        YES
+   Newtype         YES        NO{1}
+   Data family     YES        NO{2}
+
+{1} Consider newtype N a = MkN (F a)   -- Arg has Nominal role
+    Is it true that (N t1) ~R (N t2)   ==>   t1 ~N t2  ?
+    No, absolutely not.  E.g.
+       type instance F Int = Int; type instance F Bool = Char
+       Then (N Int) ~R (N Bool), by unwrapping, but we don't want Int~Char!
+
+    See Note [Decomposing newtype equalities]
+
+{2} We must treat data families precisely like newtypes, because of the
+    possibility of newtype instances. See also
+    Note [Decomposing newtype equalities]. See #10534 and
+    test case typecheck/should_fail/T10534.
+
+---- Takeaway summary -----
+For sound and complete decomposition, we simply need injectivity;
+that is for isInjectiveTyCon to be true:
+
+* At Nominal role, isInjectiveTyCon is True for all the TyCons we are
+  considering in this Note: datatypes, newtypes, and data families.
+
+* For Givens, injectivity is necessary for soundness; completeness has no
+  side conditions.
+
+* For Wanteds, soundness has no side conditions; but injectivity is needed
+  for completeness. See Note [Decomposing newtype equalities]
+
+This is implemented in `can_decompose` in `canTyConApp`; it looks at
+injectivity, just as specified above.
+
+
+Note [Decomposing type family applications]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Supose we have
+   [G/W]  (F ty1) ~r  (F ty2)
+This is handled by the TyFamLHS/TyFamLHS case of canEqCanLHS2.
+
+We never decompose to
+   [G/W]  ty1 ~r' ty2
+
+Instead
+
+* For Givens we do nothing. Injective type families have no corresponding
+  evidence of their injectivity, so we cannot decompose an
+  injective-type-family Given.
+
+* For Wanteds, for the Nominal role only, we emit new Wanteds rather like
+  functional dependencies, for each injective argument position.
+
+  E.g type family F a b   -- injective in first arg, but not second
+      [W] (F s1 t1) ~N (F s2 t2)
+  Emit new Wanteds
+      [W] s1 ~N s2
+  But retain the existing, unsolved constraint.
+
+Note [Decomposing newtype equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+This Note also applies to data families, which we treat like
+newtype in case of 'newtype instance'.
+
+As Note [Decomposing TyConApp equalities] describes, if N is injective
+at role r, we can do this decomposition?
+   [G/W] (N ty1) ~r (N ty2)    to     [G/W]  ty1 ~r' ty2
+
+For a Given with r=R, the answer is a solid NO: newtypes are not injective at
+representational role, and we must not decompose, or we lose soundness.
+Example is wrinkle {1} in Note [Decomposing TyConApp equalities].
+
+For a Wanted with r=R, since newtypes are not injective at representational
+role, decomposition is sound, but we may lose completeness.  Nevertheless,
+if the newtype is abstraction (so can't be unwrapped) we can only solve
+the equality by (a) using a Given or (b) decomposition.  If (a) is impossible
+(e.g. no Givens) then (b) is safe.
+
+Conclusion: decompose newtypes (at role R) only if there are no usable Givens.
+
+* Incompleteness example (EX1)
+      newtype Nt a = MkNt (Id a)
+      type family Id a where Id a = a
+
+      [W] Nt Int ~R Nt Age
+
+  Because of its use of a type family, Nt's parameter will get inferred to
+  have a nominal role. Thus, decomposing the wanted will yield [W] Int ~N Age,
+  which is unsatisfiable. Unwrapping, though, leads to a solution.
 
-If we have [W] Nt alpha ~R Nt beta, we *don't* want to decompose to
-[W] alpha ~R beta, because it's possible that alpha and beta aren't
-representationally equal. Here's another example.
+  Conclusion: always unwrap newtypes before attempting to decompose
+  them.  This is done in can_eq_nc'.  Of course, we can't unwrap if the data
+  constructor isn't in scope.  See See Note [Unwrap newtypes first].
 
-  newtype Nt a = MkNt (Id a)
-  type family Id a where Id a = a
+* Incompleteness example (EX2)
+      newtype Nt a = Mk Bool         -- NB: a is not used in the RHS,
+      type role Nt representational  -- but the user gives it an R role anyway
 
-  [W] Nt Int ~R Nt Age
+  If we have [W] Nt alpha ~R Nt beta, we *don't* want to decompose to
+  [W] alpha ~R beta, because it's possible that alpha and beta aren't
+  representationally equal.
 
-Because of its use of a type family, Nt's parameter will get inferred to have
-a nominal role. Thus, decomposing the wanted will yield [W] Int ~N Age, which
-is unsatisfiable. Unwrapping, though, leads to a solution.
+  and maybe there is a Given (Nt t1 ~R Nt t2), just waiting to be used, if we
+  figure out (elsewhere) that alpha:=t1 and beta:=t2.  This is somewhat
+  similar to the question of overlapping Givens for class constraints: see
+  Note [Instance and Given overlap] in GHC.Tc.Solver.Interact.
 
-Conclusion:
- * Unwrap newtypes before attempting to decompose them.
-   This is done in can_eq_nc'.
+  Conclusion: don't decompose [W] N s ~R N t, if there are any Given
+  equalities that could later solve it.
 
-It all comes from the fact that newtypes aren't necessarily injective
-w.r.t. representational equality.
+  But what does "any Given equalities that could later solve it" mean, precisely?
+  It must be a Given constraint that could turn into N s ~ N t.  But that
+  could include [G] (a b) ~ (c d), or even just [G] c.  But it'll definitely
+  be an CIrredCan.  So we settle for having no CIrredCans at all, which is
+  conservative but safe. See noGivenIrreds and #22331.
 
-Furthermore, as explained in Note [SelCo and newtypes] in GHC.Core.TyCo.Rep, we can't use
-SelCo on representational coercions over newtypes. SelCo comes into play
-only when decomposing givens.
+  Well not 100.0% safe. There could be a CDictCan with some un-expanded
+  superclasses; but only in some very obscure recursive-superclass
+  situations.
 
-Conclusion:
- * Do not decompose [G] N s ~R N t
+If there are no Irred Givens (which is quite common) then we will
+successfuly decompose [W] (IO Age) ~R (IO Int), and solve it.  But
+that won't happen and [W] (IO Age) ~R (IO Int) will be stuck.
+We /could/, however, be a bit more aggressive about decomposition;
+see Note [Decomposing newtypes a bit more aggressively].
 
-Is it sensible to decompose *Wanted* constraints over newtypes?  Yes!
-It's the only way we could ever prove (IO Int ~R IO Age), recalling
-that IO is a newtype.
+Remember: decomposing Wanteds is always /sound/. This Note is
+only about /completeness/.
 
-However we must be careful.  Consider
+Note [Decomposing newtypes a bit more aggressively]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+c.f. https://github.com/ghc-proposals/ghc-proposals/pull/549
+and discussion on !9282.
+
+Consider [G] c, [W] (IO Int) ~R (IO Age)
+where IO is abstract, and
+   newtype Age = MkAge Int   -- Not abstract
+With the above rules, if there any Given Irreds,
+the Wanted is insoluble because we can't decompose it.  But in fact,
+if we look at the defn of IO, roughly,
+    newtype IO a = State# -> (State#, a)
+we can see that decomposing [W] (IO Int) ~R (IO Age) to
+    [W] Int ~R Age
+definitely does not lose completeness. Why not? Because the role of
+IO's argment is representational.  Hence:
+
+  DecomposeNewtypeIdea:
+     decompose [W] (N s1 .. sn) ~R (N t1 .. tn)
+     if the roles of all N's arguments are representational
+
+If N's arguments really /are/ representational this will not lose
+completeness.  Here "really are representational" means "if you expand
+all newtypes in N's RHS, we'd infer a representational role for each
+of N's type variables in that expansion".  See Note [Role inference]
+in GHC.Tc.TyCl.Utils.
+
+But the user might /override/ a phantom role with an explicit role
+annotation, and then we could (obscurely) get incompleteness.
+Consider
 
-  type role Nt representational
+   module A( silly, T ) where
+     newtype T a = MkT Int
+     type role T representational  -- Override phantom role
 
-  [G] Nt a ~R Nt b       (1)
-  [W] NT alpha ~R Nt b   (2)
-  [W] alpha ~ a          (3)
+     silly :: Coercion (T Int) (T Bool)
+     silly = Coercion  -- Typechecks by unwrapping the newtype
 
-If we focus on (3) first, we'll substitute in (2), and now it's
-identical to the given (1), so we succeed.  But if we focus on (2)
-first, and decompose it, we'll get (alpha ~R b), which is not soluble.
-This is exactly like the question of overlapping Givens for class
-constraints: see Note [Instance and Given overlap] in GHC.Tc.Solver.Interact.
+     data Coercion a b where  -- Actually defined in Data.Type.Coercion
+       Coercion :: Coercible a b => Coercion a b
 
-Conclusion:
-  * Decompose [W] N s ~R N t  iff there no given constraint that could
-    later solve it.
+   module B where
+     import A
+     f :: T Int -> T Bool
+     f = case silly of Coercion -> coerce
 
-Note [Decomposing AppTy at representational role]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We never decompose AppTy at a representational role. For Givens, doing
-so is simply unsound: the LRCo coercion former requires a nominal-roled
-arguments. (See (1) for an example of why.) For Wanteds, decomposing
-would be sound, but it would be a guess, and a non-confluent one at that.
+Here the `coerce` gives [W] (T Int) ~R (T Bool) which, if we decompose,
+we'll get stuck with (Int ~R Bool).  Instead we want to use the
+[G] (T Int) ~R (T Bool), which will be in the Irreds.
 
-Here is an example:
+Summary: we could adopt (DecomposeNewtypeIdea), at the cost of a very
+obscure incompleteness (above).  But no one is reporting a problem from
+the lack of decompostion, so we'll just leave it for now.  This long
+Note is just to record the thinking for our future selves.
+
+Note [Decomposing AppTy equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+For AppTy all the same questions arise as in
+Note [Decomposing TyConApp equalities]. We have
+
+    s1 ~r s2,  t1 ~N t2   ==>   s1 t1 ~r s2 t2       (rule CO_APP)
+    s1 t1 ~N s2 t2        ==>   s1 ~N s2,  t1 ~N t2  (CO_LEFT, CO_RIGHT)
+
+In the first of these, why do we need Nominal equality in (t1 ~N t2)?
+See {2} below.
+
+For sound and complete solving, we need both directions to decompose. So:
+* At nominal role, all is well: we have both directions.
+* At representational role, decomposition of Givens is unsound (see {1} below),
+  and decomposition of Wanteds is incomplete.
+
+Here is an example of the incompleteness for Wanteds:
 
     [G] g1 :: a ~R b
     [W] w1 :: Maybe b ~R alpha a
-    [W] w2 :: alpha ~ Maybe
+    [W] w2 :: alpha ~N Maybe
 
-Suppose we see w1 before w2. If we were to decompose, we would decompose
-this to become
+Suppose we see w1 before w2. If we decompose, using AppCo to prove w1, we get
 
+    w1 := AppCo w3 w4
     [W] w3 :: Maybe ~R alpha
-    [W] w4 :: b ~ a
+    [W] w4 :: b ~N a
 
 Note that w4 is *nominal*. A nominal role here is necessary because AppCo
-requires a nominal role on its second argument. (See (2) for an example of
-why.) If we decomposed w1 to w3,w4, we would then get stuck, because w4
-is insoluble. On the other hand, if we see w2 first, setting alpha := Maybe,
-all is well, as we can decompose Maybe b ~R Maybe a into b ~R a.
+requires a nominal role on its second argument. (See {2} for an example of
+why.) Now we are stuck, because w4 is insoluble. On the other hand, if we
+see w2 first, setting alpha := Maybe, all is well, as we can decompose
+Maybe b ~R Maybe a into b ~R a.
 
 Another example:
-
     newtype Phant x = MkPhant Int
-
     [W] w1 :: Phant Int ~R alpha Bool
     [W] w2 :: alpha ~ Phant
 
 If we see w1 first, decomposing would be disastrous, as we would then try
 to solve Int ~ Bool. Instead, spotting w2 allows us to simplify w1 to become
-
     [W] w1' :: Phant Int ~R Phant Bool
 
 which can then (assuming MkPhant is in scope) be simplified to Int ~R Int,
 and all will be well. See also Note [Unwrap newtypes first].
 
-Bottom line: never decompose AppTy with representational roles.
+Bottom line:
+* Always decompose AppTy at nominal role: can_eq_app
+* Never decompose AppTy at representational role (neither Given nor Wanted):
+  the lack of an equation in can_eq_nc'
 
-(1) Decomposing a Given AppTy over a representational role is simply
-unsound. For example, if we have co1 :: Phant Int ~R a Bool (for
-the newtype Phant, above), then we surely don't want any relationship
-between Int and Bool, lest we also have co2 :: Phant ~ a around.
+Extra points
+{1}  Decomposing a Given AppTy over a representational role is simply
+     unsound. For example, if we have co1 :: Phant Int ~R a Bool (for
+     the newtype Phant, above), then we surely don't want any relationship
+     between Int and Bool, lest we also have co2 :: Phant ~ a around.
 
-(2) The role on the AppCo coercion is a conservative choice, because we don't
-know the role signature of the function. For example, let's assume we could
-have a representational role on the second argument of AppCo. Then, consider
+{2} The role on the AppCo coercion is a conservative choice, because we don't
+    know the role signature of the function. For example, let's assume we could
+    have a representational role on the second argument of AppCo. Then, consider
 
     data G a where    -- G will have a nominal role, as G is a GADT
       MkG :: G Int
@@ -1823,9 +1941,8 @@ have a representational role on the second argument of AppCo. Then, consider
     co2 :: Age ~R Int    -- by newtype axiom
     co3 = AppCo co1 co2 :: G Age ~R a Int    -- by our broken AppCo
 
-and now co3 can be used to cast MkG to have type G Age, in violation of
-the way GADTs are supposed to work (which is to use nominal equality).
-
+    and now co3 can be used to cast MkG to have type G Age, in violation of
+    the way GADTs are supposed to work (which is to use nominal equality).
 -}
 
 canDecomposableTyConAppOK :: CtEvidence -> EqRel
@@ -1842,6 +1959,7 @@ canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
                   -- we are guaranteed that cos has the same length
                   -- as tys1 and tys2
              -> do { cos <- zipWith4M (unifyWanted rewriters) new_locs tc_roles tys1 tys2
+                            -- See Note [Fast path when decomposing TyConApps]
                    ; setWantedEq dest (mkTyConAppCo role tc cos) }
 
            CtGiven { ctev_evar = evar }
@@ -1945,19 +2063,6 @@ canEqHardFailure ev ty1 ty2
        ; continueWith (mkIrredCt ShapeMismatchReason new_ev) }
 
 {-
-Note [Decomposing TyConApps]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-If we see (T s1 t1 ~ T s2 t2), then we can just decompose to
-  (s1 ~ s2, t1 ~ t2)
-and push those back into the work list.  But if
-  s1 = K k1    s2 = K k2
-then we will just decompose s1~s2, and it might be better to
-do so on the spot.  An important special case is where s1=s2,
-and we get just Refl.
-
-So canDecomposableTyCon is a fast-path decomposition that uses
-unifyWanted etc to short-cut that work.
-
 Note [Canonicalising type applications]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Given (s1 t1) ~ ty2, how should we proceed?
@@ -2192,6 +2297,7 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco
 
   | TyFamLHS fun_tc1 fun_args1 <- lhs1
   , TyFamLHS fun_tc2 fun_args2 <- lhs2
+  -- See Note [Decomposing type family applications]
   = do { traceTcS "canEqCanLHS2 two type families" (ppr lhs1 $$ ppr lhs2)
 
          -- emit wanted equalities for injective type families
diff --git a/compiler/GHC/Tc/Solver/InertSet.hs b/compiler/GHC/Tc/Solver/InertSet.hs
index a413c06346..b3dcb3f5b1 100644
--- a/compiler/GHC/Tc/Solver/InertSet.hs
+++ b/compiler/GHC/Tc/Solver/InertSet.hs
@@ -20,7 +20,8 @@ module GHC.Tc.Solver.InertSet (
     emptyInert,
     addInertItem,
 
-    matchableGivens,
+    noMatchableGivenDicts,
+    noGivenIrreds,
     mightEqualLater,
     prohibitedSuperClassSolve,
 
@@ -53,6 +54,7 @@ import GHC.Core.Reduction
 import GHC.Core.Predicate
 import GHC.Core.TyCo.FVs
 import qualified GHC.Core.TyCo.Rep as Rep
+import GHC.Core.Class( Class )
 import GHC.Core.TyCon
 import GHC.Core.Unify
 
@@ -1535,25 +1537,20 @@ isOuterTyVar tclvl tv
     -- becomes "outer" even though its level numbers says it isn't.
   | otherwise  = False  -- Coercion variables; doesn't much matter
 
--- | Returns Given constraints that might,
--- potentially, match the given pred. This is used when checking to see if a
+noGivenIrreds :: InertSet -> Bool
+noGivenIrreds (IS { inert_cans = inert_cans })
+  = isEmptyBag (inert_irreds inert_cans)
+
+-- | Returns True iff there are no Given constraints that might,
+-- potentially, match the given class consraint. This is used when checking to see if a
 -- Given might overlap with an instance. See Note [Instance and Given overlap]
 -- in "GHC.Tc.Solver.Interact"
-matchableGivens :: CtLoc -> PredType -> InertSet -> Cts
-matchableGivens loc_w pred_w inerts@(IS { inert_cans = inert_cans })
-  = filterBag matchable_given all_relevant_givens
+noMatchableGivenDicts :: InertSet -> CtLoc -> Class -> [TcType] -> Bool
+noMatchableGivenDicts inerts@(IS { inert_cans = inert_cans }) loc_w clas tys
+  = not $ anyBag matchable_given $
+    findDictsByClass (inert_dicts inert_cans) clas
   where
-    -- just look in class constraints and irreds. matchableGivens does get called
-    -- for ~R constraints, but we don't need to look through equalities, because
-    -- canonical equalities are used for rewriting. We'll only get caught by
-    -- non-canonical -- that is, irreducible -- equalities.
-    all_relevant_givens :: Cts
-    all_relevant_givens
-      | Just (clas, _) <- getClassPredTys_maybe pred_w
-      = findDictsByClass (inert_dicts inert_cans) clas
-        `unionBags` inert_irreds inert_cans
-      | otherwise
-      = inert_irreds inert_cans
+    pred_w = mkClassPred clas tys
 
     matchable_given :: Ct -> Bool
     matchable_given ct
diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs
index 139bb3b6b8..f17b520c94 100644
--- a/compiler/GHC/Tc/Solver/Interact.hs
+++ b/compiler/GHC/Tc/Solver/Interact.hs
@@ -1391,7 +1391,7 @@ We generate these Wanteds in three places, depending on how we notice the
 injectivity.
 
 1. When we have a [W] F tys1 ~ F tys2. This is handled in canEqCanLHS2, and
-described in Note [Decomposing equality] in GHC.Tc.Solver.Canonical.
+described in Note [Decomposing type family applications] in GHC.Tc.Solver.Canonical.
 
 2. When we have [W] F tys1 ~ T and [W] F tys2 ~ T. Note that neither of these
 constraints rewrites the other, as they have different LHSs. This is done
@@ -2283,11 +2283,9 @@ matchClassInst dflags inerts clas tys loc
 -- See Note [Instance and Given overlap]
   | not (xopt LangExt.IncoherentInstances dflags)
   , not (naturallyCoherentClass clas)
-  , let matchable_givens = matchableGivens loc pred inerts
-  , not (isEmptyBag matchable_givens)
+  , not (noMatchableGivenDicts inerts loc clas tys)
   = do { traceTcS "Delaying instance application" $
-           vcat [ text "Work item=" <+> pprClassPred clas tys
-                , text "Potential matching givens:" <+> ppr matchable_givens ]
+           vcat [ text "Work item=" <+> pprClassPred clas tys ]
        ; return NotSure }
 
   | otherwise
diff --git a/testsuite/tests/typecheck/should_compile/T22331.hs b/testsuite/tests/typecheck/should_compile/T22331.hs
new file mode 100644
index 0000000000..0454c97d7d
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T22331.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module T22331 where
+
+import Data.Coerce
+
+data family Fool a
+
+-- This works
+joe :: Coercible (Fool a) (Fool b) => Fool a -> Fool b
+joe = coerce
+
+-- This does not
+bob :: Coercible (Fool a) (Fool b) => Fool b -> Fool a
+bob = coerce
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 80738de7c1..46db37f854 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -850,3 +850,4 @@ test('T21951a', normal, compile, ['-Wredundant-strictness-flags'])
 test('T21951b', normal, compile, ['-Wredundant-strictness-flags'])
 test('T21550', normal, compile, [''])
 test('T22310', normal, compile, [''])
+test('T22331', normal, compile, [''])