Fix two constraint solving problems

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

1 files changed, 23 insertions, 1 deletions

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