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

4 files changed, 27 insertions, 18 deletions

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)