Tweak kick-out condition K2b to deal with LHSs

Kick out condition K2b really only makes sense for
inerts with a type variable on the left. This updates
the commentary and the code to skip this check for
inerts with type families on the left.

Also cleans up some commentary around solver invariants
and adds Note [K2b].

Close #19042.

test case: typecheck/should_compile/T19042

1 files changed, 52 insertions, 1 deletions

diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs
index 03aff4fff4..27a7a3abbf 100644
--- a/compiler/GHC/Tc/Types/Constraint.hs
+++ b/compiler/GHC/Tc/Types/Constraint.hs
@@ -142,7 +142,9 @@ We thus perform an occurs-check. There is, of course, some subtlety:
   already inert, with all type family redexes reduced. So a simple
   syntactic check is just fine.
 
-The occurs check is performed in GHC.Tc.Utils.Unify.checkTypeEq.
+The occurs check is performed in GHC.Tc.Utils.Unify.checkTypeEq
+and forms condition T3 in Note [Extending the inert equalities]
+in GHC.Tc.Solver.Monad.
 
 -}
 
@@ -1708,6 +1710,55 @@ I thought maybe we could never get Derived ReprEq constraints, but
 we can; straight from the Wanteds during improvement. And from a Derived
 ReprEq we could conceivably get a Derived NomEq improvement (by decomposing
 a type constructor with Nomninal role), and hence unify.
+
+This restriction bites, in an obscure scenario:
+
+  data T a
+  type role T nominal
+
+  type family F a
+
+  g :: forall b a. (F a ~ T a, Coercible (F a) (T b)) => ()
+  g = ()
+
+  f :: forall a. (F a ~ T a) => ()
+  f = g @a
+
+The problem is in the body of f. We have
+
+  [G]  F a ~N T a
+  [WD] F alpha ~N T alpha
+  [WD] F alpha ~R T a
+
+The Wanteds aren't of use, so let's just look at Deriveds:
+
+  [G] F a ~N T a
+  [D] F alpha ~N T alpha
+  [D] F alpha ~R T a
+
+As written, this makes no progress, and GHC errors. But, if we
+allowed D/N to rewrite D/R, the first D could rewrite the second:
+
+  [G] F a ~N T a
+  [D] F alpha ~N T alpha
+  [D] T alpha ~R T a
+
+Now we decompose the second D to get
+
+  [D] alpha ~N a
+
+noting the role annotation on T. This causes (alpha := a), and then
+everything else unlocks.
+
+What to do? We could "decompose" nominal equalities into nominal-only
+("NO") equalities and representational ones, where a NO equality rewrites
+only nominals. That is, when considering whether [D] F alpha ~N T alpha
+should rewrite [D] F alpha ~R T a, we could require splitting the first D
+into [D] F alpha ~NO T alpha, [D] F alpha ~R T alpha. Then, we use the R
+half of the split to rewrite the second D, and off we go. This splitting
+would allow the split-off R equality to be rewritten by other equalities,
+thus avoiding the problem in Note [Why R2?] in GHC.Tc.Solver.Monad.
+
 -}
 
 eqCanRewrite :: EqRel -> EqRel -> Bool