Make dischargeFmv handle Deriveds

A Derived CFunEqCan does not "own" its FlatMetaTv (fmv), and should not
update it.  But one caller (canCFunEqCan) was failing to satisfy the
precondition to dischargeFmv, which led to a crash (Trac #15170).

I fixed this by making dischargeFmv handle Deriveds (to avoid forcing
each caller to do so separately).

NB: this does not completely fix the original #15170 bug, but I'll
explain that on the ticket.  The test case for this patch is actually
the program in comment:1.

6 files changed, 52 insertions, 18 deletions

diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs
index e2244a99e6..32a9307d1c 100644
--- a/compiler/typecheck/TcFlatten.hs
+++ b/compiler/typecheck/TcFlatten.hs
@@ -82,15 +82,17 @@ Note [The flattening story]
    - We unflatten Wanteds at the end of each attempt to simplify the
      wanteds; see unflattenWanteds, called from solveSimpleWanteds.
 
-* Each canonical [G], [W], or [WD] CFunEqCan x : F xis ~ fsk/fmv
-  has its own distinct evidence variable x and flatten-skolem fsk/fmv.
+* Ownership of fsk/fmv.  Each canonical [G], [W], or [WD]
+       CFunEqCan x : F xis ~ fsk/fmv
+  "owns" a distinct evidence variable x, and flatten-skolem fsk/fmv.
   Why? We make a fresh fsk/fmv when the constraint is born;
   and we never rewrite the RHS of a CFunEqCan.
 
-  In contrast a [D] CFunEqCan shares its fmv with its partner [W],
+  In contrast a [D] CFunEqCan /shares/ its fmv with its partner [W],
   but does not "own" it.  If we reduce a [D] F Int ~ fmv, where
   say type instance F Int = ty, then we don't discharge fmv := ty.
-  Rather we simply generate [D] fmv ~ ty (in TcInteract.reduce_top_fun_eq)
+  Rather we simply generate [D] fmv ~ ty (in TcInteract.reduce_top_fun_eq,
+  and dischargeFmv)
 
 * Inert set invariant: if F xis1 ~ fsk1, F xis2 ~ fsk2
                        then xis1 /= xis2
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index ab94ad21bd..09cfd15a30 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -1442,15 +1442,9 @@ reactFunEq from_this fsk1 solve_this fsk2
        ; new_ev <- newGivenEvVar loc (fsk_eq_pred, evCoercion fsk_eq_co)
        ; emitWorkNC [new_ev] }
 
-  | CtDerived { ctev_loc = loc } <- solve_this
-  = do { traceTcS "reactFunEq (Derived)" (ppr from_this $$ ppr fsk1 $$
-                                          ppr solve_this $$ ppr fsk2)
-       ; emitNewDerivedEq loc Nominal (mkTyVarTy fsk1) (mkTyVarTy fsk2) }
-              -- FunEqs are always at Nominal role
-
   | otherwise  -- Wanted
-  = do { traceTcS "reactFunEq" (ppr from_this $$ ppr fsk1 $$
-                                ppr solve_this $$ ppr fsk2)
+  = do { traceTcS "reactFunEq (Wanted/Derived)"
+            (vcat [ppr from_this, ppr fsk1, ppr solve_this, ppr fsk2])
        ; dischargeFmv solve_this fsk2 (ctEvCoercion from_this) (mkTyVarTy fsk1)
        ; traceTcS "reactFunEq done" (ppr from_this $$ ppr fsk1 $$
                                      ppr solve_this $$ ppr fsk2) }
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index ba07ff8deb..17d9504f37 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -1690,8 +1690,8 @@ data Ct
         --    *never* over-saturated (because if so
         --    we should have decomposed)
 
-      cc_fsk    :: TcTyVar  -- [Given]  always a FlatSkolTv
-                            -- [Wanted] always a FlatMetaTv
+      cc_fsk    :: TcTyVar  -- [G]  always a FlatSkolTv
+                            -- [W], [WD], or [D] always a FlatMetaTv
         -- See Note [The flattening story] in TcFlatten
     }
 
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index 580a33cd9d..f5d6ca9aa7 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -3045,23 +3045,34 @@ demoteUnfilledFmv fmv
 
 -----------------------------
 dischargeFmv :: CtEvidence -> TcTyVar -> TcCoercion -> TcType -> TcS ()
--- (dischargeFmv x fmv co ty)
+-- (dischargeFmv ev fmv co ty)
 --     [W] ev :: F tys ~ fmv
 --         co :: F tys ~ xi
 -- Precondition: fmv is not filled, and fmv `notElem` xi
---               ev is Wanted
+--               ev is Wanted or Derived
 --
--- Then set fmv := xi,
+-- Then for [W] or [WD], we actually fill in the fmv:
+--      set fmv := xi,
 --      set ev  := co
 --      kick out any inert things that are now rewritable
 --
--- Does not evaluate 'co' if 'ev' is Derived
+-- For [D], we instead emit an equality that must ultimately hold
+--      emit  xi ~ fmv
+--      Does not evaluate 'co' if 'ev' is Derived
+--
+-- See TcFlatten Note [The flattening story],
+-- especially "Ownership of fsk/fmv"
 dischargeFmv ev@(CtWanted { ctev_dest = dest }) fmv co xi
   = ASSERT2( not (fmv `elemVarSet` tyCoVarsOfType xi), ppr ev $$ ppr fmv $$ ppr xi )
     do { setWantedEvTerm dest (EvExpr (evCoercion co))
        ; unflattenFmv fmv xi
        ; n_kicked <- kickOutAfterUnification fmv
        ; traceTcS "dischargeFmv" (ppr fmv <+> equals <+> ppr xi $$ pprKicked n_kicked) }
+
+dischargeFmv (CtDerived { ctev_loc = loc }) fmv _co xi
+  = emitNewDerivedEq loc Nominal xi (mkTyVarTy fmv)
+              -- FunEqs are always at Nominal role
+
 dischargeFmv ev _ _ _ = pprPanic "dischargeFmv" (ppr ev)
 
 pprKicked :: Int -> SDoc
diff --git a/testsuite/tests/polykinds/T15170.hs b/testsuite/tests/polykinds/T15170.hs
new file mode 100644
index 0000000000..a105ca5344
--- /dev/null
+++ b/testsuite/tests/polykinds/T15170.hs
@@ -0,0 +1,26 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+module T15170  where
+
+import Data.Kind
+import Data.Proxy
+
+data TyFun :: Type -> Type -> Type
+type a ~> b = TyFun a b -> Type
+infixr 0 ~>
+
+type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
+type f @@ x = Apply f x
+infixl 9 @@
+
+wat :: forall (a :: Type)
+              (b :: a ~> Type)
+              (c :: forall (x :: a). Proxy x ~> b @@ x ~> Type)
+              (f :: forall (x :: a) (y :: b @@ x). Proxy x ~> Proxy y ~> c @@ ('Proxy :: Proxy x) @@ y)
+              (x :: a).
+      (forall (xx :: a) (yy :: b @@ xx). Proxy (f @@ ('Proxy :: Proxy xx) @@ ('Proxy :: Proxy yy)))
+   -> ()
+wat _ = ()
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 7992e283cd..5aaa217575 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -190,3 +190,4 @@ test('T14873', normal, compile, [''])
 test('SigTvKinds3', normal, compile_fail, [''])
 test('T15116', normal, compile_fail, [''])
 test('T15116a', normal, compile_fail, [''])
+test('T15170', normal, compile, [''])