Instances in no-evidence implications

Trac #15290 showed that it's possible that we might attempt to use a
quantified constraint to solve an equality in a situation where we
don't have anywhere to put the evidence bindings.  This made GHC crash.

This patch stops the crash, but still rejects the pogram.  See
Note [Instances in no-evidence implications] in TcInteract.

Finding this bug revealed another lurking bug:

* An infelicity in the treatment of superclasses -- we were expanding
  them locally at the leaves, rather than at their binding site; see
  (3a) in Note [The superclass story].

  As a consequence, TcRnTypes.superclassesMightHelp must look inside
  implications.

In more detail:

* Stop the crash, by making TcInteract.chooseInstance test for
  the no-evidence-bindings case.  In that case we simply don't
  use the instance.  This entailed a slight change to the type
  of chooseInstance.

* Make TcSMonad.getPendingScDicts (now renamed getPendingGivenScs)
  return only Givens from the /current level/; and make
  TcRnTypes.superClassesMightHelp look inside implications.

* Refactor the simpl_loop and superclass-expansion stuff in
  TcSimplify.  The logic is much easier to understand now, and
  has less duplication.

4 files changed, 95 insertions, 0 deletions

diff --git a/testsuite/tests/quantified-constraints/T15290.hs b/testsuite/tests/quantified-constraints/T15290.hs
new file mode 100644
index 0000000000..8a0c3d989f
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T15290.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE TypeApplications, ImpredicativeTypes, ScopedTypeVariables,
+             QuantifiedConstraints, StandaloneDeriving, GeneralizedNewtypeDeriving #-}
+
+module T15290 where
+
+import Prelude hiding ( Monad(..) )
+import Data.Coerce ( Coercible, coerce )
+
+class Monad m where
+  join  :: m (m a) -> m a
+
+newtype StateT s m a = StateT { runStateT :: s -> m (s, a) }
+
+newtype IntStateT m a = IntStateT { runIntStateT :: StateT Int m a }
+
+instance Monad m => Monad (StateT s m) where
+  join = error "urk"
+
+instance (Monad m, forall p q. Coercible p q => Coercible (m p) (m q))
+      => Monad (IntStateT m) where
+
+--   Fails with the impredicative instantiation of coerce, succeeds without
+
+-- Impredicative version (fails)
+--    join = coerce
+--          @(forall a. StateT Int m (StateT Int m a) -> StateT Int m a)
+--          @(forall a. IntStateT m (IntStateT m a)   -> IntStateT m a)
+--          join
+
+
+-- Predicative version (succeeds)
+    join = (coerce
+           @(StateT Int m (StateT Int m a) -> StateT Int m a)
+           @(IntStateT m (IntStateT m a)   -> IntStateT m a)
+           join) :: forall a. IntStateT m (IntStateT m a)   -> IntStateT m a
diff --git a/testsuite/tests/quantified-constraints/T15290a.hs b/testsuite/tests/quantified-constraints/T15290a.hs
new file mode 100644
index 0000000000..bfb5b2a069
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T15290a.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE TypeApplications, ImpredicativeTypes, ScopedTypeVariables,
+             QuantifiedConstraints, StandaloneDeriving, GeneralizedNewtypeDeriving #-}
+
+module T15290a where
+
+import Prelude hiding ( Monad(..) )
+import Data.Coerce ( Coercible, coerce )
+
+class Monad m where
+  join  :: m (m a) -> m a
+
+newtype StateT s m a = StateT { runStateT :: s -> m (s, a) }
+
+newtype IntStateT m a = IntStateT { runIntStateT :: StateT Int m a }
+
+instance Monad m => Monad (StateT s m) where
+  join = error "urk"
+
+instance (Monad m, forall p q. Coercible p q => Coercible (m p) (m q))
+      => Monad (IntStateT m) where
+
+--   Fails with the impredicative instantiation of coerce, succeeds without
+
+-- Impredicative version (fails)
+    join = coerce
+          @(forall a. StateT Int m (StateT Int m a) -> StateT Int m a)
+          @(forall a. IntStateT m (IntStateT m a)   -> IntStateT m a)
+          join
+
+
+-- Predicative version (succeeds)
+--    join = (coerce
+--           @(StateT Int m (StateT Int m a) -> StateT Int m a)
+--           @(IntStateT m (IntStateT m a)   -> IntStateT m a)
+--           join) :: forall a. IntStateT m (IntStateT m a)   -> IntStateT m a
diff --git a/testsuite/tests/quantified-constraints/T15290a.stderr b/testsuite/tests/quantified-constraints/T15290a.stderr
new file mode 100644
index 0000000000..2efd784f31
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T15290a.stderr
@@ -0,0 +1,22 @@
+
+T15290a.hs:25:12: error:
+    • Couldn't match representation of type ‘m (Int, IntStateT m a1)’
+                               with that of ‘m (Int, StateT Int m a1)’
+        arising from a use of ‘coerce’
+      NB: We cannot know what roles the parameters to ‘m’ have;
+        we must assume that the role is nominal
+    • In the expression:
+        coerce
+          @(forall a. StateT Int m (StateT Int m a) -> StateT Int m a)
+          @(forall a. IntStateT m (IntStateT m a) -> IntStateT m a)
+          join
+      In an equation for ‘join’:
+          join
+            = coerce
+                @(forall a. StateT Int m (StateT Int m a) -> StateT Int m a)
+                @(forall a. IntStateT m (IntStateT m a) -> IntStateT m a)
+                join
+      In the instance declaration for ‘Monad (IntStateT m)’
+    • Relevant bindings include
+        join :: IntStateT m (IntStateT m a) -> IntStateT m a
+          (bound at T15290a.hs:25:5)
diff --git a/testsuite/tests/quantified-constraints/all.T b/testsuite/tests/quantified-constraints/all.T
index 75fcf8c772..5f8547b5a8 100644
--- a/testsuite/tests/quantified-constraints/all.T
+++ b/testsuite/tests/quantified-constraints/all.T
@@ -10,3 +10,6 @@ test('T14961', normal, compile, [''])
 test('T9123a', normal, compile, [''])
 test('T15244', normal, compile, [''])
 test('T15231', normal, compile_fail, [''])
+
+test('T15290', normal, compile, [''])
+test('T15290a', normal, compile_fail, [''])