From 261dd83cacec71edd551e9c581d05285c9ea3226 Mon Sep 17 00:00:00 2001
From: Simon Peyton Jones <simonpj@microsoft.com>
Date: Mon, 25 Jun 2018 17:42:57 +0100
Subject: 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.
---
 testsuite/tests/quantified-constraints/T15290b.hs  | 28 ++++++++++++++++++++++
 .../tests/quantified-constraints/T15290b.stderr    | 14 +++++++++++
 testsuite/tests/quantified-constraints/all.T       |  1 +
 3 files changed, 43 insertions(+)
 create mode 100644 testsuite/tests/quantified-constraints/T15290b.hs
 create mode 100644 testsuite/tests/quantified-constraints/T15290b.stderr

(limited to 'testsuite/tests/quantified-constraints')

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, [''])
-- 
cgit v1.2.1