canCFunEqCan: use isTcReflexiveCo (not isTcReflCo)

As Trac #15577 showed, it was possible for a /homo-kinded/
constraint to trigger the /hetero-kinded/ branch of canCFunEqCan,
and that triggered an infinite loop.

The fix is easier, but there remains a deeper questions: why is
the flattener producing giant refexive coercions?

(cherry picked from commit 2e226a46c422c12f78dc3d3f62fe5a15e22bd986)

4 files changed, 109 insertions, 4 deletions

diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index 188065f754..8509de5ff9 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -1714,6 +1714,11 @@ the new one, so we use dischargeFmv. This also kicks out constraints
 from the inert set; this behavior is correct, as the kind-change may
 allow more constraints to be solved.
 
+We use `isTcReflexiveCo`, to ensure that we only use the hetero-kinded case
+if we really need to.  Of course `flattenArgsNom` should return `Refl`
+whenever possible, but Trac #15577 was an infinite loop because even
+though the coercion was homo-kinded, `kind_co` was not `Refl`, so we
+made a new (identical) CFunEqCan, and then the entire process repeated.
 -}
 
 canCFunEqCan :: CtEvidence
@@ -1733,13 +1738,20 @@ canCFunEqCan ev fn tys fsk
 
              flav    = ctEvFlavour ev
        ; (ev', fsk')
-              -- See Note [canCFunEqCan]
-           <- if isTcReflCo kind_co
-              then do { let fsk_ty = mkTyVarTy fsk
+           <- if isTcReflexiveCo kind_co   -- See Note [canCFunEqCan]
+              then do { traceTcS "canCFunEqCan: refl" (ppr new_lhs $$ ppr lhs_co)
+                      ; let fsk_ty = mkTyVarTy fsk
                       ; ev' <- rewriteEqEvidence ev NotSwapped new_lhs fsk_ty
                                                  lhs_co (mkTcNomReflCo fsk_ty)
                       ; return (ev', fsk) }
-              else do { (ev', new_co, new_fsk)
+              else do { traceTcS "canCFunEqCan: non-refl" $
+                        vcat [ text "Kind co:" <+> ppr kind_co
+                             , text "RHS:" <+> ppr fsk <+> dcolon <+> ppr (tyVarKind fsk)
+                             , text "LHS:" <+> hang (ppr (mkTyConApp fn tys))
+                                                  2 (dcolon <+> ppr (typeKind (mkTyConApp fn tys)))
+                             , text "New LHS" <+> hang (ppr new_lhs)
+                                                     2 (dcolon <+> ppr (typeKind new_lhs)) ]
+                      ; (ev', new_co, new_fsk)
                           <- newFlattenSkolem flav (ctEvLoc ev) fn tys'
                       ; let xi = mkTyVarTy new_fsk `mkCastTy` kind_co
                                -- sym lhs_co :: F tys ~ F tys'
diff --git a/testsuite/tests/polykinds/T15577.hs b/testsuite/tests/polykinds/T15577.hs
new file mode 100644
index 0000000000..18ebc42f92
--- /dev/null
+++ b/testsuite/tests/polykinds/T15577.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+module Bug where
+
+import Data.Kind
+import Data.Proxy
+import Data.Type.Equality
+
+type family F (x :: f (a :: k)) :: f a
+
+f :: forall k (f :: k -> Type) (a :: k) (r :: f a). Proxy r -> F r :~: r
+f = undefined
+
+g :: forall (f :: Type -> Type) (a :: Type) (r :: f a). Proxy r -> F r :~: r
+g r | Refl <- f -- Uncommenting the line below makes it work again
+                -- @Type
+                @f @a @r r
+    = Refl
diff --git a/testsuite/tests/polykinds/T15577.stderr b/testsuite/tests/polykinds/T15577.stderr
new file mode 100644
index 0000000000..a098ad152d
--- /dev/null
+++ b/testsuite/tests/polykinds/T15577.stderr
@@ -0,0 +1,71 @@
+
+T15577.hs:20:18: error:
+    • Expecting one more argument to ‘f’
+      Expected a type, but ‘f’ has kind ‘* -> *’
+    • In the type ‘f’
+      In a stmt of a pattern guard for
+                     an equation for ‘g’:
+        Refl <- f @f @a @r r
+      In an equation for ‘g’: g r | Refl <- f @f @a @r r = Refl
+
+T15577.hs:20:21: error:
+    • Expected kind ‘f1 -> *’, but ‘a’ has kind ‘*’
+    • In the type ‘a’
+      In a stmt of a pattern guard for
+                     an equation for ‘g’:
+        Refl <- f @f @a @r r
+      In an equation for ‘g’: g r | Refl <- f @f @a @r r = Refl
+    • Relevant bindings include
+        r :: Proxy r1 (bound at T15577.hs:18:3)
+        g :: Proxy r1 -> F r1 :~: r1 (bound at T15577.hs:18:1)
+
+T15577.hs:20:24: error:
+    • Couldn't match kind ‘* -> *’ with ‘*’
+      When matching kinds
+        f1 :: * -> *
+        f1 a1 :: *
+      Expected kind ‘f1’, but ‘r’ has kind ‘f1 a1’
+    • In the type ‘r’
+      In a stmt of a pattern guard for
+                     an equation for ‘g’:
+        Refl <- f @f @a @r r
+      In an equation for ‘g’: g r | Refl <- f @f @a @r r = Refl
+    • Relevant bindings include
+        r :: Proxy r1 (bound at T15577.hs:18:3)
+        g :: Proxy r1 -> F r1 :~: r1 (bound at T15577.hs:18:1)
+
+T15577.hs:20:26: error:
+    • Couldn't match kind ‘*’ with ‘* -> *’
+      When matching kinds
+        a1 :: *
+        f1 :: * -> *
+    • In the fourth argument of ‘f’, namely ‘r’
+      In a stmt of a pattern guard for
+                     an equation for ‘g’:
+        Refl <- f @f @a @r r
+      In an equation for ‘g’: g r | Refl <- f @f @a @r r = Refl
+    • Relevant bindings include
+        r :: Proxy r1 (bound at T15577.hs:18:3)
+        g :: Proxy r1 -> F r1 :~: r1 (bound at T15577.hs:18:1)
+
+T15577.hs:21:7: error:
+    • Could not deduce: F r1 ~ r1
+      from the context: r0 ~ F r0
+        bound by a pattern with constructor:
+                   Refl :: forall k (a :: k). a :~: a,
+                 in a pattern binding in
+                      a pattern guard for
+                        an equation for ‘g’
+        at T15577.hs:18:7-10
+      ‘r1’ is a rigid type variable bound by
+        the type signature for:
+          g :: forall (f1 :: * -> *) a1 (r1 :: f1 a1).
+               Proxy r1 -> F r1 :~: r1
+        at T15577.hs:17:1-76
+      Expected type: F r1 :~: r1
+        Actual type: r1 :~: r1
+    • In the expression: Refl
+      In an equation for ‘g’: g r | Refl <- f @f @a @r r = Refl
+    • Relevant bindings include
+        r :: Proxy r1 (bound at T15577.hs:18:3)
+        g :: Proxy r1 -> F r1 :~: r1 (bound at T15577.hs:18:1)
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 425e57a946..2d0f993b17 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -192,3 +192,4 @@ test('T15116', normal, compile_fail, [''])
 test('T15116a', normal, compile_fail, [''])
 test('T15170', normal, compile, [''])
 test('T14939', normal, compile, ['-O'])
+test('T15577', normal, compile_fail, ['-O'])