Refactor validity checking for constraints

There are several changes here.

* TcInteract has gotten too big, so I moved all the class-instance
  matching out of TcInteract into a new module ClsInst. It parallels
  the FamInst module.

  The main export of ClsInst is matchGlobalInst.
  This now works in TcM not TcS.

* A big reason to make matchGlobalInst work in TcM is that we can
  then use it from TcValidity.checkSimplifiableClassConstraint.
  That extends checkSimplifiableClassConstraint to work uniformly
  for built-in instances, which means that we now get a warning
  if we have givens (Typeable x, KnownNat n); see Trac #15322.

* This change also made me refactor LookupInstResult, in particular
  by adding the InstanceWhat field.  I also changed the name of the
  type to ClsInstResult.

  Then instead of matchGlobalInst reporting a staging error (which is
  inappropriate for the call from TcValidity), we can do so in
  TcInteract.checkInstanceOK.

* In TcValidity, we now check quantified constraints for termination.
  For example, this signature should be rejected:
     f :: (forall a. Eq (m a) => Eq (m a)) => blah
  as discussed in Trac #15316.   The main change here is that
  TcValidity.check_pred_help now uses classifyPredType, and has a
  case for ForAllPred which it didn't before.

  This had knock-on refactoring effects in TcValidity.

3 files changed, 28 insertions, 0 deletions

diff --git a/testsuite/tests/quantified-constraints/T15316.hs b/testsuite/tests/quantified-constraints/T15316.hs
new file mode 100644
index 0000000000..07539e3183
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T15316.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE RankNTypes, QuantifiedConstraints, ConstraintKinds  #-}
+-- NB: disabling these if enabled:
+{-# LANGUAGE NoUndecidableInstances, NoUndecidableSuperClasses #-}
+
+module T15316 where
+
+import Data.Proxy
+
+{-
+class Class a where
+         method :: a
+
+subsume :: (Class a => Class b) => Proxy a -> Proxy b -> ((Class a => Class b) => r) -> r
+subsume _ _ x = x
+
+value :: Proxy a -> a
+value p = subsume p p method
+-}
+
+subsume' :: Proxy c -> ((c => c) => r) -> r
+subsume' _ x = x
diff --git a/testsuite/tests/quantified-constraints/T15316.stderr b/testsuite/tests/quantified-constraints/T15316.stderr
new file mode 100644
index 0000000000..4444c2c453
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T15316.stderr
@@ -0,0 +1,6 @@
+
+T15316.hs:20:13: error:
+    • The constraint ‘c’ is no smaller than the instance head ‘c’
+      (Use UndecidableInstances to permit this)
+    • In the quantified constraint ‘c => c’
+      In the type signature: subsume' :: Proxy c -> ((c => c) => r) -> r
diff --git a/testsuite/tests/quantified-constraints/all.T b/testsuite/tests/quantified-constraints/all.T
index 65e636744f..3145f47cf1 100644
--- a/testsuite/tests/quantified-constraints/all.T
+++ b/testsuite/tests/quantified-constraints/all.T
@@ -14,3 +14,4 @@ test('T15231', normal, compile_fail, [''])
 test('T15290', normal, compile, [''])
 test('T15290a', normal, compile_fail, [''])
 test('T15290b', normal, compile_fail, [''])
+test('T15316', normal, compile_fail, [''])