Instantiate GND bindings with an explicit type signature

Summary:
Before, we were using visible type application to apply
impredicative types to `coerce` in
`GeneralizedNewtypeDeriving`-generated bindings. This approach breaks
down when combined with `QuantifiedConstraints` in certain ways,
which #14883 and #15290 provide examples of. See
Note [GND and QuantifiedConstraints] for all the gory details.

To avoid this issue, we instead use an explicit type signature to
instantiate each GND binding, and use that to bind any type variables
that might be bound by a class method's type signature. This reduces
the need to impredicative type applications, and more importantly,
makes the programs from #14883 and #15290 work again.

Test Plan: make test TEST="T15290b T15290c T15290d T14883"

Reviewers: simonpj, bgamari

Reviewed By: simonpj

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #14883, #15290

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

7 files changed, 132 insertions, 67 deletions

diff --git a/testsuite/tests/deriving/should_compile/T14578.stderr b/testsuite/tests/deriving/should_compile/T14578.stderr
index acbbdd627b..9f7ef67bf3 100644
--- a/testsuite/tests/deriving/should_compile/T14578.stderr
+++ b/testsuite/tests/deriving/should_compile/T14578.stderr
@@ -5,69 +5,61 @@ Derived class instances:
            GHC.Base.Functor (T14578.App f) where
     GHC.Base.fmap
       = GHC.Prim.coerce
-          @(forall (a :: TYPE GHC.Types.LiftedRep)
-                   (b :: TYPE GHC.Types.LiftedRep).
-            (a -> b) -> f a -> f b)
-          @(forall (a :: TYPE GHC.Types.LiftedRep)
-                   (b :: TYPE GHC.Types.LiftedRep).
-            (a -> b) -> T14578.App f a -> T14578.App f b)
-          GHC.Base.fmap
+          @((a -> b) -> f a -> f b)
+          @((a -> b) -> T14578.App f a -> T14578.App f b)
+          GHC.Base.fmap ::
+          forall (a :: TYPE GHC.Types.LiftedRep)
+                 (b :: TYPE GHC.Types.LiftedRep).
+          (a -> b) -> T14578.App f a -> T14578.App f b
     (GHC.Base.<$)
       = GHC.Prim.coerce
-          @(forall (a :: TYPE GHC.Types.LiftedRep)
-                   (b :: TYPE GHC.Types.LiftedRep).
-            a -> f b -> f a)
-          @(forall (a :: TYPE GHC.Types.LiftedRep)
-                   (b :: TYPE GHC.Types.LiftedRep).
-            a -> T14578.App f b -> T14578.App f a)
-          (GHC.Base.<$)
+          @(a -> f b -> f a)
+          @(a -> T14578.App f b -> T14578.App f a)
+          (GHC.Base.<$) ::
+          forall (a :: TYPE GHC.Types.LiftedRep)
+                 (b :: TYPE GHC.Types.LiftedRep).
+          a -> T14578.App f b -> T14578.App f a
   
   instance GHC.Base.Applicative f =>
            GHC.Base.Applicative (T14578.App f) where
     GHC.Base.pure
       = GHC.Prim.coerce
-          @(forall (a :: TYPE GHC.Types.LiftedRep). a -> f a)
-          @(forall (a :: TYPE GHC.Types.LiftedRep). a -> T14578.App f a)
-          GHC.Base.pure
+          @(a -> f a) @(a -> T14578.App f a) GHC.Base.pure ::
+          forall (a :: TYPE GHC.Types.LiftedRep). a -> T14578.App f a
     (GHC.Base.<*>)
       = GHC.Prim.coerce
-          @(forall (a :: TYPE GHC.Types.LiftedRep)
-                   (b :: TYPE GHC.Types.LiftedRep).
-            f (a -> b) -> f a -> f b)
-          @(forall (a :: TYPE GHC.Types.LiftedRep)
-                   (b :: TYPE GHC.Types.LiftedRep).
-            T14578.App f (a -> b) -> T14578.App f a -> T14578.App f b)
-          (GHC.Base.<*>)
+          @(f (a -> b) -> f a -> f b)
+          @(T14578.App f (a -> b) -> T14578.App f a -> T14578.App f b)
+          (GHC.Base.<*>) ::
+          forall (a :: TYPE GHC.Types.LiftedRep)
+                 (b :: TYPE GHC.Types.LiftedRep).
+          T14578.App f (a -> b) -> T14578.App f a -> T14578.App f b
     GHC.Base.liftA2
       = GHC.Prim.coerce
-          @(forall (a :: TYPE GHC.Types.LiftedRep)
-                   (b :: TYPE GHC.Types.LiftedRep)
-                   (c :: TYPE GHC.Types.LiftedRep).
-            (a -> b -> c) -> f a -> f b -> f c)
-          @(forall (a :: TYPE GHC.Types.LiftedRep)
-                   (b :: TYPE GHC.Types.LiftedRep)
-                   (c :: TYPE GHC.Types.LiftedRep).
-            (a -> b -> c)
+          @((a -> b -> c) -> f a -> f b -> f c)
+          @((a -> b -> c)
             -> T14578.App f a -> T14578.App f b -> T14578.App f c)
-          GHC.Base.liftA2
+          GHC.Base.liftA2 ::
+          forall (a :: TYPE GHC.Types.LiftedRep)
+                 (b :: TYPE GHC.Types.LiftedRep)
+                 (c :: TYPE GHC.Types.LiftedRep).
+          (a -> b -> c) -> T14578.App f a -> T14578.App f b -> T14578.App f c
     (GHC.Base.*>)
       = GHC.Prim.coerce
-          @(forall (a :: TYPE GHC.Types.LiftedRep)
-                   (b :: TYPE GHC.Types.LiftedRep).
-            f a -> f b -> f b)
-          @(forall (a :: TYPE GHC.Types.LiftedRep)
-                   (b :: TYPE GHC.Types.LiftedRep).
-            T14578.App f a -> T14578.App f b -> T14578.App f b)
-          (GHC.Base.*>)
+          @(f a -> f b -> f b)
+          @(T14578.App f a -> T14578.App f b -> T14578.App f b)
+          (GHC.Base.*>) ::
+          forall (a :: TYPE GHC.Types.LiftedRep)
+                 (b :: TYPE GHC.Types.LiftedRep).
+          T14578.App f a -> T14578.App f b -> T14578.App f b
     (GHC.Base.<*)
       = GHC.Prim.coerce
-          @(forall (a :: TYPE GHC.Types.LiftedRep)
-                   (b :: TYPE GHC.Types.LiftedRep).
-            f a -> f b -> f a)
-          @(forall (a :: TYPE GHC.Types.LiftedRep)
-                   (b :: TYPE GHC.Types.LiftedRep).
-            T14578.App f a -> T14578.App f b -> T14578.App f a)
-          (GHC.Base.<*)
+          @(f a -> f b -> f a)
+          @(T14578.App f a -> T14578.App f b -> T14578.App f a)
+          (GHC.Base.<*) ::
+          forall (a :: TYPE GHC.Types.LiftedRep)
+                 (b :: TYPE GHC.Types.LiftedRep).
+          T14578.App f a -> T14578.App f b -> T14578.App f a
   
   instance (GHC.Base.Applicative f, GHC.Base.Applicative g,
             GHC.Base.Semigroup a) =>
@@ -81,7 +73,8 @@ Derived class instances:
                -> T14578.App (Data.Functor.Compose.Compose f g :: TYPE GHC.Types.LiftedRep
                                                                   -> TYPE GHC.Types.LiftedRep) a)
           @(T14578.Wat f g a -> T14578.Wat f g a -> T14578.Wat f g a)
-          (GHC.Base.<>)
+          (GHC.Base.<>) ::
+          T14578.Wat f g a -> T14578.Wat f g a -> T14578.Wat f g a
     GHC.Base.sconcat
       = GHC.Prim.coerce
           @(GHC.Base.NonEmpty (T14578.App (Data.Functor.Compose.Compose f g :: TYPE GHC.Types.LiftedRep
@@ -89,19 +82,19 @@ Derived class instances:
             -> T14578.App (Data.Functor.Compose.Compose f g :: TYPE GHC.Types.LiftedRep
                                                                -> TYPE GHC.Types.LiftedRep) a)
           @(GHC.Base.NonEmpty (T14578.Wat f g a) -> T14578.Wat f g a)
-          GHC.Base.sconcat
+          GHC.Base.sconcat ::
+          GHC.Base.NonEmpty (T14578.Wat f g a) -> T14578.Wat f g a
     GHC.Base.stimes
       = GHC.Prim.coerce
-          @(forall (b :: TYPE GHC.Types.LiftedRep).
-            GHC.Real.Integral b =>
-            b
+          @(b
             -> T14578.App (Data.Functor.Compose.Compose f g :: TYPE GHC.Types.LiftedRep
                                                                -> TYPE GHC.Types.LiftedRep) a
                -> T14578.App (Data.Functor.Compose.Compose f g :: TYPE GHC.Types.LiftedRep
                                                                   -> TYPE GHC.Types.LiftedRep) a)
-          @(forall (b :: TYPE GHC.Types.LiftedRep).
-            GHC.Real.Integral b => b -> T14578.Wat f g a -> T14578.Wat f g a)
-          GHC.Base.stimes
+          @(b -> T14578.Wat f g a -> T14578.Wat f g a)
+          GHC.Base.stimes ::
+          forall (b :: TYPE GHC.Types.LiftedRep).
+          GHC.Real.Integral b => b -> T14578.Wat f g a -> T14578.Wat f g a
   
 
 Derived type family instances:
diff --git a/testsuite/tests/deriving/should_compile/T14883.hs b/testsuite/tests/deriving/should_compile/T14883.hs
new file mode 100644
index 0000000000..0ec4b5f786
--- /dev/null
+++ b/testsuite/tests/deriving/should_compile/T14883.hs
@@ -0,0 +1,30 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE ImpredicativeTypes #-}
+{-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeApplications #-}
+module T14883 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'
+deriving instance Traversable' m => Traversable' (T1 m)
diff --git a/testsuite/tests/deriving/should_compile/T15290c.hs b/testsuite/tests/deriving/should_compile/T15290c.hs
new file mode 100644
index 0000000000..5aa9c7187e
--- /dev/null
+++ b/testsuite/tests/deriving/should_compile/T15290c.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE QuantifiedConstraints, StandaloneDeriving, GeneralizedNewtypeDeriving #-}
+
+module T15290c where
+
+import Prelude hiding ( Monad(..) )
+import Data.Coerce ( Coercible )
+
+class Monad m where
+  (>>=) :: m a -> (a -> m b) -> m b
+  join  :: m (m a) -> m a
+
+newtype StateT s m a = StateT { runStateT :: s -> m (s, a) }
+
+instance Monad m => Monad (StateT s m) where
+  ma >>= fmb = StateT $ \s -> runStateT ma s >>= \(s1, a) -> runStateT (fmb a) s1
+  join ssa = StateT $ \s -> runStateT ssa s >>= \(s, sa) -> runStateT sa s
+
+newtype IntStateT m a = IntStateT { runIntStateT :: StateT Int m a }
+
+deriving instance (Monad m, forall p q. Coercible p q => Coercible (m p) (m q)) => Monad (IntStateT m)
diff --git a/testsuite/tests/deriving/should_compile/T15290d.hs b/testsuite/tests/deriving/should_compile/T15290d.hs
new file mode 100644
index 0000000000..f9fceb8aa4
--- /dev/null
+++ b/testsuite/tests/deriving/should_compile/T15290d.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE RankNTypes #-}
+module T15290d where
+
+class C a where
+  c :: Int -> forall b. b -> a
+
+instance C Int where
+  c _ _ = 42
+
+newtype Age = MkAge Int
+  deriving C
diff --git a/testsuite/tests/deriving/should_compile/all.T b/testsuite/tests/deriving/should_compile/all.T
index 61b888ea01..a224871b2a 100644
--- a/testsuite/tests/deriving/should_compile/all.T
+++ b/testsuite/tests/deriving/should_compile/all.T
@@ -106,5 +106,8 @@ test('T14331', normal, compile, [''])
 test('T14578', normal, compile, ['-ddump-deriv -dsuppress-uniques'])
 test('T14579', normal, compile, [''])
 test('T14682', normal, compile, ['-ddump-deriv -dsuppress-uniques'])
+test('T14883', normal, compile, [''])
 test('T14932', normal, compile, [''])
 test('T14933', normal, compile, [''])
+test('T15290c', normal, compile, [''])
+test('T15290d', normal, compile, [''])
diff --git a/testsuite/tests/deriving/should_fail/T15073.stderr b/testsuite/tests/deriving/should_fail/T15073.stderr
index 7658b8e422..87fd7e5225 100644
--- a/testsuite/tests/deriving/should_fail/T15073.stderr
+++ b/testsuite/tests/deriving/should_fail/T15073.stderr
@@ -1,22 +1,28 @@
 
 T15073.hs:8:12: error:
-    • Illegal unboxed tuple type as function argument: (# a #)
+    • Illegal unboxed tuple type as function argument: (# Foo a #)
       Perhaps you intended to use UnboxedTuples
-    • In the expression:
-        GHC.Prim.coerce
-          @(a
-            -> (Unit# a :: TYPE (GHC.Types.TupleRep ((:) GHC.Types.LiftedRep ([] :: [] GHC.Types.RuntimeRep) :: [] GHC.Types.RuntimeRep))))
-          @(Foo a
-            -> (Unit# (Foo a) :: TYPE (GHC.Types.TupleRep ((:) GHC.Types.LiftedRep ([] :: [] GHC.Types.RuntimeRep) :: [] GHC.Types.RuntimeRep))))
-          p
+    • In an expression type signature:
+        Foo a
+        -> (Unit# (Foo a) :: TYPE (GHC.Types.TupleRep ((:) GHC.Types.LiftedRep ([] :: [] GHC.Types.RuntimeRep) :: [] GHC.Types.RuntimeRep)))
+      In the expression:
+          GHC.Prim.coerce
+            @(a
+              -> (Unit# a :: TYPE (GHC.Types.TupleRep ((:) GHC.Types.LiftedRep ([] :: [] GHC.Types.RuntimeRep) :: [] GHC.Types.RuntimeRep))))
+            @(Foo a
+              -> (Unit# (Foo a) :: TYPE (GHC.Types.TupleRep ((:) GHC.Types.LiftedRep ([] :: [] GHC.Types.RuntimeRep) :: [] GHC.Types.RuntimeRep))))
+            p ::
+            Foo a
+            -> (Unit# (Foo a) :: TYPE (GHC.Types.TupleRep ((:) GHC.Types.LiftedRep ([] :: [] GHC.Types.RuntimeRep) :: [] GHC.Types.RuntimeRep)))
       In an equation for ‘p’:
           p = GHC.Prim.coerce
                 @(a
                   -> (Unit# a :: TYPE (GHC.Types.TupleRep ((:) GHC.Types.LiftedRep ([] :: [] GHC.Types.RuntimeRep) :: [] GHC.Types.RuntimeRep))))
                 @(Foo a
                   -> (Unit# (Foo a) :: TYPE (GHC.Types.TupleRep ((:) GHC.Types.LiftedRep ([] :: [] GHC.Types.RuntimeRep) :: [] GHC.Types.RuntimeRep))))
-                p
+                p ::
+                Foo a
+                -> (Unit# (Foo a) :: TYPE (GHC.Types.TupleRep ((:) GHC.Types.LiftedRep ([] :: [] GHC.Types.RuntimeRep) :: [] GHC.Types.RuntimeRep)))
       When typechecking the code for ‘p’
         in a derived instance for ‘P (Foo a)’:
         To see the code I am typechecking, use -ddump-deriv
-      In the instance declaration for ‘P (Foo a)’
diff --git a/testsuite/tests/deriving/should_fail/T4846.stderr b/testsuite/tests/deriving/should_fail/T4846.stderr
index 9642132f99..428f1a538b 100644
--- a/testsuite/tests/deriving/should_fail/T4846.stderr
+++ b/testsuite/tests/deriving/should_fail/T4846.stderr
@@ -3,9 +3,10 @@ T4846.hs:29:1: error:
     • Couldn't match type ‘Bool’ with ‘BOOL’
         arising from a use of ‘GHC.Prim.coerce’
     • In the expression:
-        GHC.Prim.coerce @(Expr Bool) @(Expr BOOL) mkExpr
+          GHC.Prim.coerce @(Expr Bool) @(Expr BOOL) mkExpr :: Expr BOOL
       In an equation for ‘mkExpr’:
-          mkExpr = GHC.Prim.coerce @(Expr Bool) @(Expr BOOL) mkExpr
+          mkExpr
+            = GHC.Prim.coerce @(Expr Bool) @(Expr BOOL) mkExpr :: Expr BOOL
       When typechecking the code for ‘mkExpr’
         in a derived instance for ‘B BOOL’:
         To see the code I am typechecking, use -ddump-deriv