Test #19665 as expect_broken, with commentarywip/T19042

4 files changed, 35 insertions, 8 deletions

diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs
index 0d71c8026c..c12ffca1eb 100644
--- a/compiler/GHC/Tc/Solver/Monad.hs
+++ b/compiler/GHC/Tc/Solver/Monad.hs
@@ -990,12 +990,12 @@ Ignoring roles (for now): A CanEqLHS lhs is *rewritable* in a type t if the
 lhs tree appears as a subtree within t without traversing any of the following
 components of t:
   * coercions (whether they appear in casts CastTy or as arguments CoercionTy)
-  * kinds of variables
+  * kinds of variable occurrences
 The check for rewritability *does* look in kinds of the bound variable of a
 ForAllTy.
 
 Goal: If lhs is not rewritable in t, then t is a fixpoint of the generalised
-substitution containing lhs -f*-> t', where f* is a flavour such that f* >= f
+substitution containing only {lhs -f*-> t'}, where f* is a flavour such that f* >= f
 for all f.
 
 The reason for this definition is that the rewriter does not rewrite in coercions
@@ -1003,10 +1003,12 @@ or variables' kinds. In turn, the rewriter does not need to rewrite there becaus
 those places are never used for controlling the behaviour of the solver: these
 places are not used in matching instances or in decomposing equalities.
 
-There is one exception: we sometimes do an occurs-check to decide e.g. how to
-orient an equality. (See the comments on GHC.Tc.Solver.Canonical.canEqTyVarFunEq.)
-Accordingly, the presence of a variable in a kind or coercion just might influence
-the solver. Here is an example:
+There is one exception to the claim that non-rewritable parts of the tree do
+not affect the solver: we sometimes do an occurs-check to decide e.g. how to
+orient an equality. (See the comments on
+GHC.Tc.Solver.Canonical.canEqTyVarFunEq.) Accordingly, the presence of a
+variable in a kind or coercion just might influence the solver. Here is an
+example:
 
   type family Const x y where
     Const x y = x
@@ -1018,7 +1020,8 @@ the solver. Here is an example:
                       AxConst Type alpha ;;
                       sym (AxConst Type Nat))
 
-The cast is clearly ludicrous, but we can't quite rule it out. (See (EQ1) from
+The cast is clearly ludicrous (it ties together a cast and its symmetric version),
+but we can't quite rule it out. (See (EQ1) from
 Note [Respecting definitional equality] in GHC.Core.TyCo.Rep to see why we need
 the Const Type Nat bit.) And yet this cast will (quite rightly) prevent alpha
 from unifying with the RHS. I (Richard E) don't have an example of where this
@@ -1131,7 +1134,7 @@ The idea is that
   - (K2b): if lhs not in s, we have no further opportunity to apply the
     work item
 
-  - See Note [K4] about (K4)
+  - (K4): See Note [K4]
 
 * Lemma (L3). Suppose we have f* such that, for all f, f* >= f. Then
   if we are adding lhs -fw-> t (where T1, T2, and T3 hold), we will keep a -f*-> s.
diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs
index b702aaa77b..2cff342eee 100644
--- a/compiler/GHC/Tc/Types/Constraint.hs
+++ b/compiler/GHC/Tc/Types/Constraint.hs
@@ -1760,6 +1760,9 @@ 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.
 
+This infelicity is #19665 and tested in typecheck/should_compile/T19665
+(marked as expect_broken).
+
 -}
 
 eqCanRewrite :: EqRel -> EqRel -> Bool
diff --git a/testsuite/tests/typecheck/should_compile/T19665.hs b/testsuite/tests/typecheck/should_compile/T19665.hs
new file mode 100644
index 0000000000..a6ba719718
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T19665.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE ScopedTypeVariables, TypeApplications, TypeFamilies,
+             RoleAnnotations, FlexibleContexts, AllowAmbiguousTypes #-}
+
+-- See Note [Deriveds do rewrite Deriveds] in GHC.Tc.Types.Constraint
+-- for commentary.
+
+module T19665 where
+
+import Data.Coerce
+
+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
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 71cd232870..b02d64adcc 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -715,6 +715,7 @@ test('T17024', normal, compile, [''])
 test('T19186', normal, compile, [''])
 test('T17021a', normal, compile, [''])
 test('T17772', normal, compile, [''])
+test('T19665', expect_broken(19665), compile, [''])
 test('T18005', normal, compile, [''])
 test('T18023', normal, compile, [''])
 test('T18036', normal, compile, [''])