Fix floating of equalities

This rather subtle patch fixes Trac #14584.  The problem was
that we'd allowed a coercion, bound in a nested scope, to escape
into an outer scope.

The main changes are

* TcSimplify.floatEqualities takes more care when floating
  equalities to make sure we don't float one out that mentions
  a locally-bound coercion.
  See Note [What prevents a constraint from floating]

* TcSimplify.emitResidualConstraints (which emits the residual
  constraints in simplifyInfer) now avoids burying the constraints
  for escaping CoVars inside the implication constraint.

* Since I had do to this stuff with CoVars, I moved the
  fancy footwork about not quantifying over CoVars from
  TcMType.quantifyTyVars to its caller
  TcSimplify.decideQuantifiedTyVars.  I think its other
  callers don't need to worry about all this CoVar stuff.

This turned out to be surprisigly tricky, and took me a solid
day to get right.  I think the result is reasonably neat, though,
and well documented with Notes.

7 files changed, 125 insertions, 10 deletions

diff --git a/testsuite/tests/indexed-types/should_fail/T13877.stderr b/testsuite/tests/indexed-types/should_fail/T13877.stderr
index a90a4dd93a..9dc8534ca1 100644
--- a/testsuite/tests/indexed-types/should_fail/T13877.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T13877.stderr
@@ -2,7 +2,9 @@
 T13877.hs:65:17: error:
     • Couldn't match type ‘Apply p (x : xs)’ with ‘p (x : xs)’
       Expected type: Sing x
-                     -> Sing xs -> App [a] (':->) * p xs -> App [a] (':->) * p (x : xs)
+                     -> Sing xs
+                     -> App [a1] (':->) * p xs
+                     -> App [a1] (':->) * p (x : xs)
         Actual type: Sing x -> Sing xs -> (p @@ xs) -> p @@ (x : xs)
     • In the expression: listElimPoly @(:->) @a @p @l
       In an equation for ‘listElimTyFun’:
@@ -10,14 +12,14 @@ T13877.hs:65:17: error:
     • Relevant bindings include
         listElimTyFun :: Sing l
                          -> (p @@ '[])
-                         -> (forall (x :: a) (xs :: [a]).
+                         -> (forall (x :: a1) (xs :: [a1]).
                              Sing x -> Sing xs -> (p @@ xs) -> p @@ (x : xs))
                          -> p @@ l
           (bound at T13877.hs:65:1)
 
 T13877.hs:65:41: error:
     • Expecting one more argument to ‘p’
-      Expected kind ‘(-?>) [a] * (':->)’, but ‘p’ has kind ‘[a] ~> *’
+      Expected kind ‘(-?>) [a1] * (':->)’, but ‘p’ has kind ‘[a1] ~> *’
     • In the type ‘p’
       In the expression: listElimPoly @(:->) @a @p @l
       In an equation for ‘listElimTyFun’:
@@ -25,7 +27,7 @@ T13877.hs:65:41: error:
     • Relevant bindings include
         listElimTyFun :: Sing l
                          -> (p @@ '[])
-                         -> (forall (x :: a) (xs :: [a]).
+                         -> (forall (x :: a1) (xs :: [a1]).
                              Sing x -> Sing xs -> (p @@ xs) -> p @@ (x : xs))
                          -> p @@ l
           (bound at T13877.hs:65:1)
diff --git a/testsuite/tests/partial-sigs/should_fail/T14584.hs b/testsuite/tests/partial-sigs/should_fail/T14584.hs
new file mode 100644
index 0000000000..508725eec7
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_fail/T14584.hs
@@ -0,0 +1,56 @@
+{-# OPTIONS_GHC -fdefer-type-errors #-}     -- Very important to this bug!
+{-# Language PartialTypeSignatures #-}
+{-# Language TypeFamilyDependencies, KindSignatures #-}
+{-# Language PolyKinds #-}
+{-# Language DataKinds #-}
+{-# Language TypeFamilies #-}
+{-# Language RankNTypes #-}
+{-# Language NoImplicitPrelude #-}
+{-# Language FlexibleContexts #-}
+{-# Language MultiParamTypeClasses #-}
+{-# Language GADTs #-}
+{-# Language ConstraintKinds #-}
+{-# Language FlexibleInstances #-}
+{-# Language TypeOperators #-}
+{-# Language ScopedTypeVariables #-}
+{-# Language DefaultSignatures #-}
+{-# Language FunctionalDependencies #-}
+{-# Language UndecidableSuperClasses #-}
+{-# Language UndecidableInstances #-}
+{-# Language TypeInType #-}
+{-# Language AllowAmbiguousTypes #-}
+{-# Language InstanceSigs, TypeApplications #-}
+
+module T14584 where
+
+import Data.Monoid
+import Data.Kind
+
+data family Sing (a::k)
+
+class SingKind k where
+  type Demote k = (res :: Type) | res -> k
+  fromSing :: Sing (a::k) -> Demote k
+
+class SingI (a::k) where
+  sing :: Sing a
+
+data ACT  :: Type -> Type -> Type
+data MHOM :: Type -> Type -> Type
+
+type m %%-  a  = ACT  m a  -> Type
+type m %%-> m' = MHOM m m' -> Type
+
+class Monoid m => Action (act :: m %%- a) where
+  act :: m -> (a -> a)
+
+class (Monoid m, Monoid m') => MonHom (mhom :: m %%-> m') where
+  monHom :: m -> m'
+
+data MonHom_Distributive m :: (m %%- a) -> (a %%-> a)
+
+type Good k = (Demote k ~ k, SingKind k)
+
+instance (Action act, Monoid a, Good m) => MonHom (MonHom_Distributive m act :: a %%-> a) where
+  monHom :: a -> a
+  monHom = act @_ @_ @act (fromSing @m (sing @m @a :: Sing _))
diff --git a/testsuite/tests/partial-sigs/should_fail/T14584.stderr b/testsuite/tests/partial-sigs/should_fail/T14584.stderr
new file mode 100644
index 0000000000..65c2381ad4
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_fail/T14584.stderr
@@ -0,0 +1,21 @@
+
+T14584.hs:56:50: warning: [-Wdeferred-type-errors (in -Wdefault)]
+    • Expected kind ‘m1’, but ‘a’ has kind ‘*’
+    • In the type ‘a’
+      In the second argument of ‘fromSing’, namely
+        ‘(sing @m @a :: Sing _)’
+      In the fourth argument of ‘act’, namely
+        ‘(fromSing @m (sing @m @a :: Sing _))’
+
+T14584.hs:56:60: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘a :: m’
+      Where: ‘a’, ‘m’ are rigid type variables bound by
+               the instance declaration
+               at T14584.hs:54:10-89
+    • In an expression type signature: Sing _
+      In the second argument of ‘fromSing’, namely
+        ‘(sing @m @a :: Sing _)’
+      In the fourth argument of ‘act’, namely
+        ‘(fromSing @m (sing @m @a :: Sing _))’
+    • Relevant bindings include
+        monHom :: a -> a (bound at T14584.hs:56:3)
diff --git a/testsuite/tests/partial-sigs/should_fail/T14584a.hs b/testsuite/tests/partial-sigs/should_fail/T14584a.hs
new file mode 100644
index 0000000000..016295ac4f
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_fail/T14584a.hs
@@ -0,0 +1,16 @@
+{-# OPTIONS_GHC -fdefer-type-errors #-}     -- Very important to this bug!
+{-# Language PartialTypeSignatures #-}
+{-# Language KindSignatures #-}
+{-# Language PolyKinds #-}
+{-# Language ScopedTypeVariables #-}
+{-# Language AllowAmbiguousTypes #-}
+{-# Language TypeApplications #-}
+
+module T14584a where
+
+f :: forall m. ()
+f = id @m :: _
+
+g :: forall m. ()
+g = let h = id @m
+    in h
diff --git a/testsuite/tests/partial-sigs/should_fail/T14584a.stderr b/testsuite/tests/partial-sigs/should_fail/T14584a.stderr
new file mode 100644
index 0000000000..d6be3fc080
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_fail/T14584a.stderr
@@ -0,0 +1,24 @@
+
+T14584a.hs:12:5: warning: [-Wdeferred-type-errors (in -Wdefault)]
+    • Couldn't match expected type ‘()’ with actual type ‘m -> m’
+    • In the expression: id @m :: _
+      In an equation for ‘f’: f = id @m :: _
+
+T14584a.hs:12:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘m -> m’
+      Where: ‘m’, ‘k’ are rigid type variables bound by
+               the type signature for:
+                 f :: forall k2 (m :: k2). ()
+               at T14584a.hs:11:1-17
+    • In an expression type signature: _
+      In the expression: id @m :: _
+      In an equation for ‘f’: f = id @m :: _
+    • Relevant bindings include f :: () (bound at T14584a.hs:12:1)
+
+T14584a.hs:16:8: warning: [-Wdeferred-type-errors (in -Wdefault)]
+    • Couldn't match expected type ‘()’ with actual type ‘m -> m’
+    • Probable cause: ‘h’ is applied to too few arguments
+      In the expression: h
+      In the expression: let h = id @m in h
+      In an equation for ‘g’: g = let h = id @m in h
+    • Relevant bindings include h :: m -> m (bound at T14584a.hs:15:9)
diff --git a/testsuite/tests/partial-sigs/should_fail/all.T b/testsuite/tests/partial-sigs/should_fail/all.T
index 91509c4f36..b974ce8950 100644
--- a/testsuite/tests/partial-sigs/should_fail/all.T
+++ b/testsuite/tests/partial-sigs/should_fail/all.T
@@ -67,3 +67,5 @@ test('T12732', normal, compile_fail, ['-fobject-code -fdefer-typed-holes'])
 test('T14040a', normal, compile_fail, [''])
 test('T14449', normal, compile_fail, [''])
 test('T14479', normal, compile_fail, [''])
+test('T14584', normal, compile, [''])
+test('T14584a', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/VtaFail.stderr b/testsuite/tests/typecheck/should_fail/VtaFail.stderr
index 17486dfefa..a9958016ce 100644
--- a/testsuite/tests/typecheck/should_fail/VtaFail.stderr
+++ b/testsuite/tests/typecheck/should_fail/VtaFail.stderr
@@ -6,12 +6,6 @@ VtaFail.hs:7:16: error:
       In an equation for ‘answer_nosig’:
           answer_nosig = pairup_nosig @Int @Bool 5 True
 
-VtaFail.hs:12:26: error:
-    • No instance for (Num Bool) arising from a use of ‘addOne’
-    • In the expression: addOne @Bool 5
-      In an equation for ‘answer_constraint_fail’:
-          answer_constraint_fail = addOne @Bool 5
-
 VtaFail.hs:14:17: error:
     • Cannot apply expression of type ‘p0 -> p0’
       to a visible type argument ‘Int’