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.

5 files changed, 119 insertions, 0 deletions

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, [''])