Rewrite `Coercible` solver

Summary:
This is a rewrite of the algorithm to solve for Coercible "instances".

A preliminary form of these ideas is at
https://ghc.haskell.org/trac/ghc/wiki/Design/NewCoercibleSolver

The basic idea here is that the `EqPred` constructor of `PredTree`
now is parameterised by a new type `EqRel` (where
`data EqRel = NomEq | ReprEq`). Thus, every equality constraint can
now talk about nominal equality (the usual case) or representational
equality (the `Coercible` case).

This is a change from the previous
behavior where `Coercible` was just considered a regular class with
a special case in `matchClassInst`.

Because of this change, representational equalities are now
canonicalized just like nominal ones, allowing more equalities
to be solved -- in particular, the case at the top of #9117.

A knock-on effect is that the flattener must be aware of the
choice of equality relation, because the inert set now stores
both representational inert equalities alongside the nominal
inert equalities. Of course, we can use representational equalities
to rewrite only within another representational equality --
thus the parameterization of the flattener.

A nice side effect of this change is that I've introduced a new
type `CtFlavour`, which tracks G vs. W vs. D, removing some ugliness
in the flattener.

This commit includes some refactoring as discussed on D546.
It also removes the ability of Deriveds to rewrite Deriveds.

This fixes bugs #9117 and #8984.

Reviewers: simonpj, austin, nomeata

Subscribers: carter, thomie

Differential Revision: https://phabricator.haskell.org/D546

GHC Trac Issues: #9117, #8984

10 files changed, 81 insertions, 63 deletions

diff --git a/testsuite/tests/deriving/should_fail/T1496.stderr b/testsuite/tests/deriving/should_fail/T1496.stderr
index 867d6c6842..c9f3869846 100644
--- a/testsuite/tests/deriving/should_fail/T1496.stderr
+++ b/testsuite/tests/deriving/should_fail/T1496.stderr
@@ -1,11 +1,9 @@
 
 T1496.hs:10:32:
-    Could not coerce from ‘c Int’ to ‘c Moo’
-      because ‘c Int’ and ‘c Moo’ are different types.
-      arising from the coercion of the method ‘isInt’ from type
-                   ‘forall (c :: * -> *). c Int -> c Int’ to type
-                   ‘forall (c :: * -> *). c Int -> c Moo’
-    Possible fix:
-      use a standalone 'deriving instance' declaration,
-        so you can specify the instance context yourself
+    Couldn't match representation of type ‘c Int’ with that of ‘c Moo’
+    arising from the coercion of the method ‘isInt’
+      from type ‘forall (c :: * -> *). c Int -> c Int’
+        to type ‘forall (c :: * -> *). c Int -> c Moo’
+    NB: We cannot know what roles the parameters to ‘c’ have;
+      we must assume that the role is nominal
     When deriving the instance for (IsInt Moo)
diff --git a/testsuite/tests/deriving/should_fail/T4846.stderr b/testsuite/tests/deriving/should_fail/T4846.stderr
index 8d6198ea8e..ab24af374e 100644
--- a/testsuite/tests/deriving/should_fail/T4846.stderr
+++ b/testsuite/tests/deriving/should_fail/T4846.stderr
@@ -1,9 +1,10 @@
 
 T4846.hs:29:1:
-    Could not coerce from ‘Expr Bool’ to ‘Expr BOOL’
-      because the first type argument of ‘Expr’ has role Nominal,
-      but the arguments ‘Bool’ and ‘BOOL’ differ
-      arising from a use of ‘GHC.Prim.coerce’
+    Couldn't match type ‘BOOL’ with ‘Bool’
+    arising from trying to show that the representations of
+      ‘Expr Bool’ and
+      ‘Expr BOOL’ are the same
+    Relevant role signatures: type role Expr nominal
     In the expression:
         GHC.Prim.coerce (mkExpr :: Expr Bool) :: Expr BOOL
     In an equation for ‘mkExpr’:
diff --git a/testsuite/tests/deriving/should_fail/T5498.stderr b/testsuite/tests/deriving/should_fail/T5498.stderr
index b613eae368..ac91aaa4d0 100644
--- a/testsuite/tests/deriving/should_fail/T5498.stderr
+++ b/testsuite/tests/deriving/should_fail/T5498.stderr
@@ -1,11 +1,11 @@
 
 T5498.hs:30:39:
-    Could not coerce from ‘c a’ to ‘c (Down a)’
-      because ‘c a’ and ‘c (Down a)’ are different types.
-      arising from the coercion of the method ‘intIso’ from type
-                   ‘forall (c :: * -> *). c a -> c Int’ to type
-                   ‘forall (c :: * -> *). c (Down a) -> c Int’
-    Possible fix:
-      use a standalone 'deriving instance' declaration,
-        so you can specify the instance context yourself
+    Couldn't match representation of type ‘c a’
+                             with that of ‘c (Down a)’
+    arising from the coercion of the method ‘intIso’
+      from type ‘forall (c :: * -> *). c a -> c Int’
+        to type ‘forall (c :: * -> *). c (Down a) -> c Int’
+    Relevant role signatures: type role Down representational
+    NB: We cannot know what roles the parameters to ‘c’ have;
+      we must assume that the role is nominal
     When deriving the instance for (IntIso (Down a))
diff --git a/testsuite/tests/deriving/should_fail/T6147.stderr b/testsuite/tests/deriving/should_fail/T6147.stderr
index a346ac3216..7f851a656b 100644
--- a/testsuite/tests/deriving/should_fail/T6147.stderr
+++ b/testsuite/tests/deriving/should_fail/T6147.stderr
@@ -1,11 +1,7 @@
 
 T6147.hs:13:32:
-    Could not coerce from ‘T Int’ to ‘T Foo’
-      because the first type argument of ‘T’ has role Nominal,
-      but the arguments ‘Int’ and ‘Foo’ differ
-      arising from the coercion of the method ‘foo’ from type
-                   ‘Int -> T Int’ to type ‘Foo -> T Foo’
-    Possible fix:
-      use a standalone 'deriving instance' declaration,
-        so you can specify the instance context yourself
+    Couldn't match type ‘Int’ with ‘Foo’
+    arising from the coercion of the method ‘foo’
+      from type ‘Int -> T Int’ to type ‘Foo -> T Foo’
+    Relevant role signatures: type role T nominal
     When deriving the instance for (C Foo)
diff --git a/testsuite/tests/deriving/should_fail/T7148.stderr b/testsuite/tests/deriving/should_fail/T7148.stderr
index 9b1008a360..ba3a88b6fe 100644
--- a/testsuite/tests/deriving/should_fail/T7148.stderr
+++ b/testsuite/tests/deriving/should_fail/T7148.stderr
@@ -1,24 +1,20 @@
 
 T7148.hs:27:40:
-    Could not coerce from ‘SameType b1 b’ to ‘SameType b1 (Tagged a b)’
-      because the second type argument of ‘SameType’ has role Nominal,
-      but the arguments ‘b’ and ‘Tagged a b’ differ
-      arising from the coercion of the method ‘iso2’ from type
-                   ‘forall b. SameType b () -> SameType b b’ to type
-                   ‘forall b. SameType b () -> SameType b (Tagged a b)’
-    Possible fix:
-      use a standalone 'deriving instance' declaration,
-        so you can specify the instance context yourself
+    Occurs check: cannot construct the infinite type: b ~ Tagged a b
+    arising from the coercion of the method ‘iso2’
+      from type ‘forall b. SameType b () -> SameType b b’
+        to type ‘forall b. SameType b () -> SameType b (Tagged a b)’
+    Relevant role signatures:
+      type role Tagged phantom representational
+      type role SameType nominal nominal
     When deriving the instance for (IsoUnit (Tagged a b))
 
 T7148.hs:27:40:
-    Could not coerce from ‘SameType b b1’ to ‘SameType (Tagged a b) b1’
-      because the first type argument of ‘SameType’ has role Nominal,
-      but the arguments ‘b’ and ‘Tagged a b’ differ
-      arising from the coercion of the method ‘iso1’ from type
-                   ‘forall b. SameType () b -> SameType b b’ to type
-                   ‘forall b. SameType () b -> SameType (Tagged a b) b’
-    Possible fix:
-      use a standalone 'deriving instance' declaration,
-        so you can specify the instance context yourself
+    Occurs check: cannot construct the infinite type: b ~ Tagged a b
+    arising from the coercion of the method ‘iso1’
+      from type ‘forall b. SameType () b -> SameType b b’
+        to type ‘forall b. SameType () b -> SameType (Tagged a b) b’
+    Relevant role signatures:
+      type role Tagged phantom representational
+      type role SameType nominal nominal
     When deriving the instance for (IsoUnit (Tagged a b))
diff --git a/testsuite/tests/deriving/should_fail/T7148a.stderr b/testsuite/tests/deriving/should_fail/T7148a.stderr
index 5f865d1f5c..4edb968702 100644
--- a/testsuite/tests/deriving/should_fail/T7148a.stderr
+++ b/testsuite/tests/deriving/should_fail/T7148a.stderr
@@ -1,11 +1,14 @@
 
 T7148a.hs:19:50:
-    Could not coerce from ‘Result a b’ to ‘b’
-      because ‘Result a b’ and ‘b’ are different types.
-      arising from the coercion of the method ‘coerce’ from type
-                   ‘forall b. Proxy b -> a -> Result a b’ to type
-                   ‘forall b. Proxy b -> IS_NO_LONGER a -> Result (IS_NO_LONGER a) b’
-    Possible fix:
-      use a standalone 'deriving instance' declaration,
-        so you can specify the instance context yourself
+    Couldn't match representation of type ‘b’ with that of ‘Result a b’
+      ‘b’ is a rigid type variable bound by
+          the type forall b1. Proxy b1 -> a -> Result a b1 at T7148a.hs:19:50
+    arising from the coercion of the method ‘coerce’
+      from type ‘forall b. Proxy b -> a -> Result a b’
+        to type ‘forall b.
+                 Proxy b -> IS_NO_LONGER a -> Result (IS_NO_LONGER a) b’
+    Relevant role signatures:
+      type role IS_NO_LONGER representational
+      type role Result nominal nominal
+      type role Proxy phantom
     When deriving the instance for (Convert (IS_NO_LONGER a))
diff --git a/testsuite/tests/deriving/should_fail/T8851.stderr b/testsuite/tests/deriving/should_fail/T8851.stderr
index 348f1f1714..0a2b384bd1 100644
--- a/testsuite/tests/deriving/should_fail/T8851.stderr
+++ b/testsuite/tests/deriving/should_fail/T8851.stderr
@@ -1,12 +1,16 @@
 
 T8851.hs:24:12:
-    Could not coerce from ‘Monad Parser’ to ‘Monad MyParser’
-      because the first type argument of ‘Monad’ has role Nominal,
-      but the arguments ‘Parser’ and ‘MyParser’ differ
-      arising from the coercion of the method ‘notFollowedBy’ from type
-                   ‘forall a. (Monad Parser, Show a) => Parser a -> Parser ()’ to type
-                   ‘forall a. (Monad MyParser, Show a) => MyParser a -> MyParser ()’
-    Possible fix:
-      use a standalone 'deriving instance' declaration,
-        so you can specify the instance context yourself
+    Couldn't match type ‘Parser’ with ‘MyParser’
+    arising from the coercion of the method ‘notFollowedBy’
+      from type ‘forall a.
+                 (Monad Parser, Show a) =>
+                 Parser a -> Parser ()’
+        to type ‘forall a.
+                 (Monad MyParser, Show a) =>
+                 MyParser a -> MyParser ()’
+    Relevant role signatures:
+      type role Monad nominal
+      type role Show nominal
+      type role MyParser phantom
+      type role Parser phantom
     When deriving the instance for (Parsing MyParser)
diff --git a/testsuite/tests/deriving/should_fail/T8984.hs b/testsuite/tests/deriving/should_fail/T8984.hs
new file mode 100644
index 0000000000..6b0b39518d
--- /dev/null
+++ b/testsuite/tests/deriving/should_fail/T8984.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE ConstraintKinds, GeneralizedNewtypeDeriving #-}
+module T8984 where
+
+class C a where
+    app :: a (a Int)
+
+newtype N cat a b = MkN (cat a b)  deriving( C )
+-- The newtype coercion is   N cat ~R cat
diff --git a/testsuite/tests/deriving/should_fail/T8984.stderr b/testsuite/tests/deriving/should_fail/T8984.stderr
new file mode 100644
index 0000000000..6606d66f63
--- /dev/null
+++ b/testsuite/tests/deriving/should_fail/T8984.stderr
@@ -0,0 +1,11 @@
+
+T8984.hs:7:46:
+    Couldn't match representation of type ‘cat a (N cat a Int)’
+                             with that of ‘cat a (cat a Int)’
+    arising from the coercion of the method ‘app’
+      from type ‘cat a (cat a Int)’ to type ‘N cat a (N cat a Int)’
+    Relevant role signatures:
+      type role N representational nominal nominal
+    NB: We cannot know what roles the parameters to ‘cat a’ have;
+      we must assume that the role is nominal
+    When deriving the instance for (C (N cat a))
diff --git a/testsuite/tests/deriving/should_fail/all.T b/testsuite/tests/deriving/should_fail/all.T
index 54a6f95afc..df7957d9b0 100644
--- a/testsuite/tests/deriving/should_fail/all.T
+++ b/testsuite/tests/deriving/should_fail/all.T
@@ -53,3 +53,4 @@ test('T9071', normal, multimod_compile_fail, ['T9071',''])
 test('T9071_2', normal, compile_fail, [''])
 test('T9687', normal, compile_fail, [''])
 
+test('T8984', normal, compile_fail, [''])