Fix TcLevel manipulation in TcDerivInfer.simplifyDeriv

The level numbers we were getting simply didn't obey the
invariant (ImplicInv) in TcType
   Note [TcLevel and untouchable type variables]

That leads to chaos. Easy to fix.  I improved the documentation.

I also added an assertion in TcSimplify that checks that
level numbers go up by 1 as we dive inside implications, so
that we catch the problem at source rather than than through
its obscure consequences.

That in turn showed up that TcRules was also generating
constraints that didn't obey (ImplicInv), so I fixed that too.
I have no idea what consequences were lurking behing that
bug, but anyway now it's fixed.  Hooray.

3 files changed, 43 insertions, 0 deletions

diff --git a/testsuite/tests/quantified-constraints/T15290b.hs b/testsuite/tests/quantified-constraints/T15290b.hs
new file mode 100644
index 0000000000..ce99aa9454
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T15290b.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE ImpredicativeTypes #-}
+{-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+module T15290b where
+
+import Data.Coerce
+import Data.Kind
+
+type Representational1 m = (forall a b. Coercible a b => Coercible (m a) (m b) :: Constraint)
+
+class Representational1 f => Functor' f where
+  fmap' :: (a -> b) -> f a -> f b
+
+class Functor' f => Applicative' f where
+  pure'  :: a -> f a
+  (<*>@) :: f (a -> b) -> f a -> f b
+
+class Functor' t => Traversable' t where
+  traverse' :: Applicative' f => (a -> f b) -> t a -> f (t b)
+
+-- Typechecks
+newtype T1 m a = MkT1 (m a) deriving (Functor', Traversable')
diff --git a/testsuite/tests/quantified-constraints/T15290b.stderr b/testsuite/tests/quantified-constraints/T15290b.stderr
new file mode 100644
index 0000000000..7dc1852c6d
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T15290b.stderr
@@ -0,0 +1,14 @@
+
+T15290b.hs:28:49: error:
+    • Couldn't match representation of type ‘f (m b)’
+                               with that of ‘f (T1 m b)’
+        arising from the coercion of the method ‘traverse'’
+          from type ‘forall (f :: * -> *) a b.
+                     Applicative' f =>
+                     (a -> f b) -> m a -> f (m b)’
+            to type ‘forall (f :: * -> *) a b.
+                     Applicative' f =>
+                     (a -> f b) -> T1 m a -> f (T1 m b)’
+      NB: We cannot know what roles the parameters to ‘f’ have;
+        we must assume that the role is nominal
+    • When deriving the instance for (Traversable' (T1 m))
diff --git a/testsuite/tests/quantified-constraints/all.T b/testsuite/tests/quantified-constraints/all.T
index 5f8547b5a8..65e636744f 100644
--- a/testsuite/tests/quantified-constraints/all.T
+++ b/testsuite/tests/quantified-constraints/all.T
@@ -13,3 +13,4 @@ test('T15231', normal, compile_fail, [''])
 
 test('T15290', normal, compile, [''])
 test('T15290a', normal, compile_fail, [''])
+test('T15290b', normal, compile_fail, [''])