Fix two constraint solving problemswip/T18855

This patch fixes two problems in the constraint solver.

* An actual bug #18555: we were floating out a constraint to eagerly,
  and that was ultimately fatal.  It's explained in
  Note [Do not float blocked constraints] in GHC.Core.Constraint.

  This is all very delicate, but it's all going to become irrelevant
  when we stop floating constraints (#17656).

* A major performance infelicity in the flattener.  When flattening
  (ty |> co) we *never* generated Refl, even when there was nothing
  at all to do.  Result: we would gratuitously rewrite the constraint
  to exactly the same thing, wasting work.  Described in #18413, and
  came up again in #18855.

  Solution: exploit the special case by calling the new function
  castCoercionKind1.  See Note [castCoercionKind1] in
  GHC.Core.Coercion

10 files changed, 129 insertions, 62 deletions

diff --git a/compiler/GHC/Core/Coercion.hs b/compiler/GHC/Core/Coercion.hs
index 401eed8edb..56d8938886 100644
--- a/compiler/GHC/Core/Coercion.hs
+++ b/compiler/GHC/Core/Coercion.hs
@@ -42,7 +42,8 @@ module GHC.Core.Coercion (
         mkAxiomInstCo, mkProofIrrelCo,
         downgradeRole, mkAxiomRuleCo,
         mkGReflRightCo, mkGReflLeftCo, mkCoherenceLeftCo, mkCoherenceRightCo,
-        mkKindCo, castCoercionKind, castCoercionKindI,
+        mkKindCo,
+        castCoercionKind, castCoercionKind1, castCoercionKind2,
         mkFamilyTyConAppCo,
 
         mkHeteroCoercionType,
@@ -1513,24 +1514,44 @@ instCoercions g ws
            ; return (piResultTy <$> g_tys <*> w_tys, g') }
 
 -- | Creates a new coercion with both of its types casted by different casts
--- @castCoercionKind g r t1 t2 h1 h2@, where @g :: t1 ~r t2@,
+-- @castCoercionKind2 g r t1 t2 h1 h2@, where @g :: t1 ~r t2@,
 -- has type @(t1 |> h1) ~r (t2 |> h2)@.
 -- @h1@ and @h2@ must be nominal.
-castCoercionKind :: Coercion -> Role -> Type -> Type
+castCoercionKind2 :: Coercion -> Role -> Type -> Type
                  -> CoercionN -> CoercionN -> Coercion
-castCoercionKind g r t1 t2 h1 h2
+castCoercionKind2 g r t1 t2 h1 h2
   = mkCoherenceRightCo r t2 h2 (mkCoherenceLeftCo r t1 h1 g)
 
+-- | @castCoercionKind1 g r t1 t2 h@ = @coercionKind g r t1 t2 h h@
+-- That is, it's a specialised form of castCoercionKind, where the two
+--          kind coercions are identical
+-- @castCoercionKind1 g r t1 t2 h@, where @g :: t1 ~r t2@,
+-- has type @(t1 |> h) ~r (t2 |> h)@.
+-- @h@ must be nominal.
+-- See Note [castCoercionKind1]
+castCoercionKind1 :: Coercion -> Role -> Type -> Type
+                  -> CoercionN -> Coercion
+castCoercionKind1 g r t1 t2 h
+  = case g of
+      Refl {} -> ASSERT( r == Nominal ) -- Refl is always Nominal
+                 mkNomReflCo (mkCastTy t2 h)
+      GRefl _ _ mco -> case mco of
+           MRefl       -> mkReflCo r (mkCastTy t2 h)
+           MCo kind_co -> GRefl r (mkCastTy t1 h) $
+                          MCo (mkSymCo h `mkTransCo` kind_co `mkTransCo` h)
+      _ -> castCoercionKind2 g r t1 t2 h h
+
 -- | Creates a new coercion with both of its types casted by different casts
 -- @castCoercionKind g h1 h2@, where @g :: t1 ~r t2@,
 -- has type @(t1 |> h1) ~r (t2 |> h2)@.
 -- @h1@ and @h2@ must be nominal.
 -- It calls @coercionKindRole@, so it's quite inefficient (which 'I' stands for)
--- Use @castCoercionKind@ instead if @t1@, @t2@, and @r@ are known beforehand.
-castCoercionKindI :: Coercion -> CoercionN -> CoercionN -> Coercion
-castCoercionKindI g h1 h2
-  = mkCoherenceRightCo r t2 h2 (mkCoherenceLeftCo r t1 h1 g)
-  where (Pair t1 t2, r) = coercionKindRole g
+-- Use @castCoercionKind2@ instead if @t1@, @t2@, and @r@ are known beforehand.
+castCoercionKind :: Coercion -> CoercionN -> CoercionN -> Coercion
+castCoercionKind g h1 h2
+  = castCoercionKind2 g r t1 t2 h1 h2
+  where
+    (Pair t1 t2, r) = coercionKindRole g
 
 mkFamilyTyConAppCo :: TyCon -> [CoercionN] -> CoercionN
 -- ^ Given a family instance 'TyCon' and its arg 'Coercion's, return the
@@ -1592,6 +1613,23 @@ mkCoCast c g
     (tc, _) = splitTyConApp (coercionLKind g)
     co_list = decomposeCo (tyConArity tc) g (tyConRolesRepresentational tc)
 
+{- Note [castCoercionKind1]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+castCoercionKind1 deals with the very important special case of castCoercionKind2
+where the two kind coercions are identical.  In that case we can exploit the
+situation where the main coercion is reflexive, via the special cases for Refl
+and GRefl.
+
+This is important when flattening  (ty |> co). We flatten ty, yielding
+   fco :: ty ~ ty'
+and now we want a coercion xco between
+   xco :: (ty |> co) ~ (ty' |> co)
+That's exactly what castCoercionKind1 does.  And it's very very common for
+fco to be Refl.  In that case we do NOT want to get some terrible composition
+of mkLeftCoherenceCo and mkRightCoherenceCo, which is what castCoercionKind2
+has to do in its full generality.  See #18413.
+-}
+
 {-
 %************************************************************************
 %*                                                                      *
@@ -1967,8 +2005,8 @@ ty_co_subst !lc role ty
          else pprPanic "ty_co_subst: covar is not almost devoid" (ppr t)
     go r ty@(LitTy {})     = ASSERT( r == Nominal )
                              mkNomReflCo ty
-    go r (CastTy ty co)    = castCoercionKindI (go r ty) (substLeftCo lc co)
-                                                         (substRightCo lc co)
+    go r (CastTy ty co)    = castCoercionKind (go r ty) (substLeftCo lc co)
+                                                        (substRightCo lc co)
     go r (CoercionTy co)   = mkProofIrrelCo r kco (substLeftCo lc co)
                                                   (substRightCo lc co)
       where kco = go Nominal (coercionType co)
diff --git a/compiler/GHC/Core/FamInstEnv.hs b/compiler/GHC/Core/FamInstEnv.hs
index 8b9af440cc..1331602c08 100644
--- a/compiler/GHC/Core/FamInstEnv.hs
+++ b/compiler/GHC/Core/FamInstEnv.hs
@@ -1447,7 +1447,7 @@ normalise_type ty
       = do { (nco, nty) <- go ty
            ; lc <- getLC
            ; let co' = substRightCo lc co
-           ; return (castCoercionKind nco Nominal ty nty co co'
+           ; return (castCoercionKind2 nco Nominal ty nty co co'
                     , mkCastTy nty co') }
     go (CoercionTy co)
       = do { lc <- getLC
diff --git a/compiler/GHC/Core/TyCo/Rep.hs b/compiler/GHC/Core/TyCo/Rep.hs
index 9503ba4ccf..4b81a39d75 100644
--- a/compiler/GHC/Core/TyCo/Rep.hs
+++ b/compiler/GHC/Core/TyCo/Rep.hs
@@ -1134,18 +1134,10 @@ data Coercion
 
   -- These ones mirror the shape of types
   = -- Refl :: _ -> N
+    -- A special case reflexivity for a very common case: Nominal reflexivity
+    -- If you need Representational, use (GRefl Representational ty MRefl)
+    --                               not (SubCo (Refl ty))
     Refl Type  -- See Note [Refl invariant]
-          -- Invariant: applications of (Refl T) to a bunch of identity coercions
-          --            always show up as Refl.
-          -- For example  (Refl T) (Refl a) (Refl b) shows up as (Refl (T a b)).
-
-          -- Applications of (Refl T) to some coercions, at least one of
-          -- which is NOT the identity, show up as TyConAppCo.
-          -- (They may not be fully saturated however.)
-          -- ConAppCo coercions (like all coercions other than Refl)
-          -- are NEVER the identity.
-
-          -- Use (GRefl Representational ty MRefl), not (SubCo (Refl ty))
 
   -- GRefl :: "e" -> _ -> Maybe N -> e
   -- See Note [Generalized reflexive coercion]
@@ -1254,26 +1246,30 @@ instance Outputable MCoercion where
   ppr MRefl    = text "MRefl"
   ppr (MCo co) = text "MCo" <+> ppr co
 
-{-
-Note [Refl invariant]
-~~~~~~~~~~~~~~~~~~~~~
-Invariant 1:
-
-Coercions have the following invariant
-     Refl (similar for GRefl r ty MRefl) is always lifted as far as possible.
-
-You might think that a consequences is:
-     Every identity coercions has Refl at the root
-
-But that's not quite true because of coercion variables.  Consider
-     g         where g :: Int~Int
-     Left h    where h :: Maybe Int ~ Maybe Int
-etc.  So the consequence is only true of coercions that
-have no coercion variables.
+{- Note [Refl invariant]
+~~~~~~~~~~~~~~~~~~~~~~~~
+Invariant 1: Refl lifting
+        Refl (similar for GRefl r ty MRefl) is always lifted as far as possible.
+    For example
+        (Refl T) (Refl a) (Refl b) is normalised (by mkAPpCo) to  (Refl (T a b)).
+
+    You might think that a consequences is:
+         Every identity coercion has Refl at the root
+
+    But that's not quite true because of coercion variables.  Consider
+         g         where g :: Int~Int
+         Left h    where h :: Maybe Int ~ Maybe Int
+    etc.  So the consequence is only true of coercions that
+    have no coercion variables.
+
+Invariant 2: TyConAppCo
+   An application of (Refl T) to some coercions, at least one of which is
+   NOT the identity, is normalised to TyConAppCo.  (They may not be
+   fully saturated however.)  TyConAppCo coercions (like all coercions
+   other than Refl) are NEVER the identity.
 
 Note [Generalized reflexive coercion]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
 GRefl is a generalized reflexive coercion (see #15192). It wraps a kind
 coercion, which might be reflexive (MRefl) or any coercion (MCo co). The typing
 rules for GRefl:
diff --git a/compiler/GHC/Core/Unify.hs b/compiler/GHC/Core/Unify.hs
index 37b30629d5..0bbc844189 100644
--- a/compiler/GHC/Core/Unify.hs
+++ b/compiler/GHC/Core/Unify.hs
@@ -1454,7 +1454,7 @@ ty_co_match menv subst (TyVarTy tv1) co lkco rkco
   = if any (inRnEnvR rn_env) (tyCoVarsOfCoList co)
     then Nothing      -- occurs check failed
     else Just $ extendVarEnv subst tv1' $
-                castCoercionKindI co (mkSymCo lkco) (mkSymCo rkco)
+                castCoercionKind co (mkSymCo lkco) (mkSymCo rkco)
 
   | otherwise
   = Nothing
diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs
index ab1e6d56d3..7f4bcdf871 100644
--- a/compiler/GHC/Tc/Solver.hs
+++ b/compiler/GHC/Tc/Solver.hs
@@ -2542,6 +2542,9 @@ floatEqualities skols given_ids ev_binds_var no_given_eqs
     is_float_eq_candidate ct
       | pred <- ctPred ct
       , EqPred NomEq ty1 ty2 <- classifyPredType pred
+      , case ct of
+           CIrredCan {} -> False   -- See Note [Do not float blocked constraints]
+           _            -> True    --   See #18855
       = float_eq ty1 ty2 || float_eq ty2 ty1
       | otherwise
       = False
@@ -2552,7 +2555,26 @@ floatEqualities skols given_ids ev_binds_var no_given_eqs
                    && (not (isTyVarTyVar tv1) || isTyVarTy ty2)
           Nothing  -> False
 
-{- Note [Float equalities from under a skolem binding]
+{- Note [Do not float blocked constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+As #18855 showed, we must not float an equality that is blocked.
+Consider
+     forall a[4]. [W] co1: alpha[4] ~ Maybe (a[4] |> bco)
+                  [W] co2: alpha[4] ~ Maybe (beta[4] |> bco])
+                  [W] bco: kappa[2] ~ Type
+
+Now co1, co2 are blocked by bco.  We will eventually float out bco
+and solve it at level 2.  But the danger is that we will *also*
+float out co2, and that is bad bad bad.  Because we'll promote alpha
+and beta to level 2, and then fail to unify the promoted beta
+with the skolem a[4].
+
+Solution: don't float out blocked equalities. Remember: we only want
+to float out if we can solve; see Note [Which equalities to float].
+
+(Future plan: kill floating altogether.)
+
+Note [Float equalities from under a skolem binding]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Which of the simple equalities can we float out?  Obviously, only
 ones that don't mention the skolem-bound variables.  But that is
diff --git a/compiler/GHC/Tc/Solver/Flatten.hs b/compiler/GHC/Tc/Solver/Flatten.hs
index dd214ceb7c..48b9c55588 100644
--- a/compiler/GHC/Tc/Solver/Flatten.hs
+++ b/compiler/GHC/Tc/Solver/Flatten.hs
@@ -1206,9 +1206,11 @@ flatten_one ty@(ForAllTy {})
 flatten_one (CastTy ty g)
   = do { (xi, co) <- flatten_one ty
        ; (g', _)   <- flatten_co g
-
        ; role <- getRole
-       ; return (mkCastTy xi g', castCoercionKind co role xi ty g' g) }
+       ; return (mkCastTy xi g', castCoercionKind1 co role xi ty g') }
+         -- It makes a /big/ difference to call castCoercionKind1 not
+         -- the more general castCoercionKind2.
+         -- See Note [castCoercionKind1] in GHC.Core.Coercion
 
 flatten_one (CoercionTy co) = first mkCoercionTy <$> flatten_co co
 
diff --git a/testsuite/tests/polykinds/T18855.hs b/testsuite/tests/polykinds/T18855.hs
new file mode 100644
index 0000000000..131cd9c8e7
--- /dev/null
+++ b/testsuite/tests/polykinds/T18855.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+module Bug where
+
+import Data.Kind
+
+type family Apply (f :: a -> b) (x :: a) :: b
+
+type F :: forall a.
+          forall (p :: forall bOne. Either a bOne -> Type)
+       -> forall bTwo.
+          forall (e :: Either a bTwo)
+       -> Apply p e
+
+type family F
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index b167b930dc..009172537b 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -225,3 +225,4 @@ test('T18451', normal, compile_fail, [''])
 test('T18451a', normal, compile_fail, [''])
 test('T18451b', normal, compile_fail, [''])
 test('T18522-ppr', normal, ghci_script, ['T18522-ppr.script'])
+test('T18855', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T10709b.stderr b/testsuite/tests/typecheck/should_fail/T10709b.stderr
index 5135165c55..53483efbad 100644
--- a/testsuite/tests/typecheck/should_fail/T10709b.stderr
+++ b/testsuite/tests/typecheck/should_fail/T10709b.stderr
@@ -11,44 +11,44 @@ T10709b.hs:6:22: error:
           x4 = (replicateM 2 . mask) (\ _ -> return ())
 
 T10709b.hs:7:22: error:
-    • Couldn't match type ‘t0’ with ‘forall a. IO a -> IO a’
+    • Couldn't match type ‘t0’ with ‘forall a1. IO a1 -> IO a1’
       Expected: (t0 -> IO a) -> IO a
         Actual: ((forall a1. IO a1 -> IO a1) -> IO a) -> IO a
       Cannot instantiate unification variable ‘t0’
-      with a type involving polytypes: forall a. IO a -> IO a
+      with a type involving polytypes: forall a1. IO a1 -> IO a1
     • In the second argument of ‘(.)’, namely ‘mask’
       In the expression: (replicateM 2 . mask) (\ x -> undefined x)
       In an equation for ‘x5’:
           x5 = (replicateM 2 . mask) (\ x -> undefined x)
 
 T10709b.hs:8:22: error:
-    • Couldn't match type ‘p0’ with ‘forall a. IO a -> IO a’
+    • Couldn't match type ‘p0’ with ‘forall a1. IO a1 -> IO a1’
       Expected: (p0 -> IO a) -> IO a
         Actual: ((forall a1. IO a1 -> IO a1) -> IO a) -> IO a
       Cannot instantiate unification variable ‘p0’
-      with a type involving polytypes: forall a. IO a -> IO a
+      with a type involving polytypes: forall a1. IO a1 -> IO a1
     • In the second argument of ‘(.)’, namely ‘mask’
       In the expression: (replicateM 2 . mask) (id (\ _ -> undefined))
       In an equation for ‘x6’:
           x6 = (replicateM 2 . mask) (id (\ _ -> undefined))
 
 T10709b.hs:9:22: error:
-    • Couldn't match type ‘b0’ with ‘forall a. IO a -> IO a’
+    • Couldn't match type ‘b0’ with ‘forall a1. IO a1 -> IO a1’
       Expected: (b0 -> IO a) -> IO a
         Actual: ((forall a1. IO a1 -> IO a1) -> IO a) -> IO a
       Cannot instantiate unification variable ‘b0’
-      with a type involving polytypes: forall a. IO a -> IO a
+      with a type involving polytypes: forall a1. IO a1 -> IO a1
     • In the second argument of ‘(.)’, namely ‘mask’
       In the expression: (replicateM 2 . mask) (const undefined)
       In an equation for ‘x7’:
           x7 = (replicateM 2 . mask) (const undefined)
 
 T10709b.hs:10:22: error:
-    • Couldn't match type ‘a0’ with ‘forall a. IO a -> IO a’
+    • Couldn't match type ‘a0’ with ‘forall a1. IO a1 -> IO a1’
       Expected: (a0 -> IO a) -> IO a
         Actual: ((forall a1. IO a1 -> IO a1) -> IO a) -> IO a
       Cannot instantiate unification variable ‘a0’
-      with a type involving polytypes: forall a. IO a -> IO a
+      with a type involving polytypes: forall a1. IO a1 -> IO a1
     • In the second argument of ‘(.)’, namely ‘mask’
       In the expression:
         (replicateM 2 . mask) ((\ x -> undefined x) :: a -> b)
diff --git a/testsuite/tests/typecheck/should_fail/T12589.stderr b/testsuite/tests/typecheck/should_fail/T12589.stderr
index 5f359090d9..a2587e2778 100644
--- a/testsuite/tests/typecheck/should_fail/T12589.stderr
+++ b/testsuite/tests/typecheck/should_fail/T12589.stderr
@@ -1,12 +1,2 @@
 
 T12589.hs:13:3: error: Variable not in scope: (&) :: t0 -> t1 -> t
-
-T12589.hs:13:5: error:
-    • Couldn't match expected type ‘t1’
-                  with actual type ‘(forall a. Bounded a => f0 a) -> h0 f0 xs0’
-      Cannot instantiate unification variable ‘t1’
-      with a type involving polytypes:
-        (forall a. Bounded a => f0 a) -> h0 f0 xs0
-    • In the second argument of ‘(&)’, namely ‘hcpure (Proxy @Bounded)’
-      In the expression: minBound & hcpure (Proxy @Bounded)
-      In an equation for ‘a’: a = minBound & hcpure (Proxy @Bounded)