Instantiate GND bindings with an explicit type signature
authorRyan Scott <ryan.gl.scott@gmail.com>
Thu, 5 Jul 2018 12:30:05 +0000 (08:30 -0400)
committerRyan Scott <ryan.gl.scott@gmail.com>
Thu, 5 Jul 2018 12:48:16 +0000 (08:48 -0400)
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

compiler/hsSyn/HsUtils.hs
compiler/rename/RnSource.hs
compiler/typecheck/TcGenDeriv.hs
testsuite/tests/deriving/should_compile/T14578.stderr
testsuite/tests/deriving/should_compile/T14883.hs [new file with mode: 0644]
testsuite/tests/deriving/should_compile/T15290c.hs [new file with mode: 0644]
testsuite/tests/deriving/should_compile/T15290d.hs [new file with mode: 0644]
testsuite/tests/deriving/should_compile/all.T
testsuite/tests/deriving/should_fail/T15073.stderr
testsuite/tests/deriving/should_fail/T4846.stderr

index 9a66b4a..ca0cb92 100644 (file)
@@ -700,7 +700,7 @@ The derived Eq instance for Glurp (without any kind signatures) would be:
   instance Eq a => Eq (Glurp a) where
     (==) = coerce @(Wat 'Proxy -> Wat 'Proxy -> Bool)
                   @(Glurp a    -> Glurp a    -> Bool)
   instance Eq a => Eq (Glurp a) where
     (==) = coerce @(Wat 'Proxy -> Wat 'Proxy -> Bool)
                   @(Glurp a    -> Glurp a    -> Bool)
-                  (==)
+                  (==) :: Glurp a -> Glurp a -> Bool
 
 (Where the visible type applications use types produced by typeToLHsType.)
 
 
 (Where the visible type applications use types produced by typeToLHsType.)
 
index bff6694..33e7c7d 100644 (file)
@@ -1745,7 +1745,7 @@ This should be rejected. Why? Because it would generate the following instance:
     instance Eq Quux where
       (==) = coerce @(Quux         -> Quux         -> Bool)
                     @(Const a Quux -> Const a Quux -> Bool)
     instance Eq Quux where
       (==) = coerce @(Quux         -> Quux         -> Bool)
                     @(Const a Quux -> Const a Quux -> Bool)
-                    (==)
+                    (==) :: Const a Quux -> Const a Quux -> Bool
 
 This instance is ill-formed, as the `a` in `Const a Quux` is unbound. The
 problem is that `a` is never used anywhere in the derived class `Eq`. Since
 
 This instance is ill-formed, as the `a` in `Const a Quux` is unbound. The
 problem is that `a` is never used anywhere in the derived class `Eq`. Since
index b944520..e1665e2 100644 (file)
@@ -1583,39 +1583,55 @@ mk_appE_app a b = nlHsApps appE_RDR [a, b]
 Note [Newtype-deriving instances]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We take every method in the original instance and `coerce` it to fit
 Note [Newtype-deriving instances]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We take every method in the original instance and `coerce` it to fit
-into the derived instance. We need a type annotation on the argument
+into the derived instance. We need type applications on the argument
 to `coerce` to make it obvious what instantiation of the method we're
 coercing from.  So from, say,
 to `coerce` to make it obvious what instantiation of the method we're
 coercing from.  So from, say,
+
   class C a b where
   class C a b where
-    op :: a -> [b] -> Int
+    op :: forall c. a -> [b] -> c -> Int
 
   newtype T x = MkT <rep-ty>
 
   instance C a <rep-ty> => C a (T x) where
 
   newtype T x = MkT <rep-ty>
 
   instance C a <rep-ty> => C a (T x) where
-    op = coerce @ (a -> [<rep-ty>] -> Int)
-                @ (a -> [T x]      -> Int)
-                op
+    op = coerce @ (a -> [<rep-ty>] -> c -> Int)
+                @ (a -> [T x]      -> c -> Int)
+                op :: forall c. a -> [T x] -> c -> Int
+
+In addition to the type applications, we also have an explicit
+type signature on the entire RHS. This brings the method-bound variable
+`c` into scope over the two type applications.
+See Note [GND and QuantifiedConstraints] for more information on why this
+is important.
 
 
-Notice that we give the 'coerce' two explicitly-visible type arguments
-to say how it should be instantiated.  Recall
+Giving 'coerce' two explicitly-visible type arguments grants us finer control
+over how it should be instantiated. Recall
 
 
-  coerce :: Coeercible a b => a -> b
+  coerce :: Coercible a b => a -> b
 
 By giving it explicit type arguments we deal with the case where
 'op' has a higher rank type, and so we must instantiate 'coerce' with
 a polytype.  E.g.
 
 By giving it explicit type arguments we deal with the case where
 'op' has a higher rank type, and so we must instantiate 'coerce' with
 a polytype.  E.g.
-   class C a where op :: forall b. a -> b -> b
+
+   class C a where op :: a -> forall b. b -> b
    newtype T x = MkT <rep-ty>
    instance C <rep-ty> => C (T x) where
    newtype T x = MkT <rep-ty>
    instance C <rep-ty> => C (T x) where
-     op = coerce @ (forall b. <rep-ty> -> b -> b)
-                 @ (forall b. T x -> b -> b)
-                op
+     op = coerce @ (<rep-ty> -> forall b. b -> b)
+                 @ (T x      -> forall b. b -> b)
+                op :: T x -> forall b. b -> b
 
 
-The type checker checks this code, and it currently requires
--XImpredicativeTypes to permit that polymorphic type instantiation,
-so we have to switch that flag on locally in TcDeriv.genInst.
+The use of type applications is crucial here. If we had tried using only
+explicit type signatures, like so:
 
 
-See #8503 for more discussion.
+   instance C <rep-ty> => C (T x) where
+     op = coerce (op :: <rep-ty> -> forall b. b -> b)
+                     :: T x      -> forall b. b -> b
+
+Then GHC will attempt to deeply skolemize the two type signatures, which will
+wreak havoc with the Coercible solver. Therefore, we instead use type
+applications, which do not deeply skolemize and thus avoid this issue.
+The downside is that we currently require -XImpredicativeTypes to permit this
+polymorphic type instantiation, so we have to switch that flag on locally in
+TcDeriv.genInst. See #8503 for more discussion.
 
 Note [Newtype-deriving trickiness]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 Note [Newtype-deriving trickiness]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1636,13 +1652,98 @@ coercing opList, thus:
   instance C a => C (N a) where { op = opN }
 
   opN :: (C a, D (N a)) => N a -> N a
   instance C a => C (N a) where { op = opN }
 
   opN :: (C a, D (N a)) => N a -> N a
-  opN = coerce @(D [a]   => [a] -> [a])
-               @(D (N a) => [N a] -> [N a]
-               opList
+  opN = coerce @([a]   -> [a])
+               @([N a] -> [N a]
+               opList :: D (N a) => [N a] -> [N a]
 
 But there is no reason to suppose that (D [a]) and (D (N a))
 are inter-coercible; these instances might completely different.
 So GHC rightly rejects this code.
 
 But there is no reason to suppose that (D [a]) and (D (N a))
 are inter-coercible; these instances might completely different.
 So GHC rightly rejects this code.
+
+Note [GND and QuantifiedConstraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider the following example from #15290:
+
+  class C m where
+    join :: m (m a) -> m a
+
+  newtype T m a = MkT (m a)
+
+  deriving instance
+    (C m, forall p q. Coercible p q => Coercible (m p) (m q)) =>
+    C (T m)
+
+The code that GHC used to generate for this was:
+
+  instance (C m, forall p q. Coercible p q => Coercible (m p) (m q)) =>
+      C (T m) where
+    join = coerce @(forall a.   m   (m a) ->   m a)
+                  @(forall a. T m (T m a) -> T m a)
+                  join
+
+This instantiates `coerce` at a polymorphic type, a form of impredicative
+polymorphism, so we're already on thin ice. And in fact the ice breaks,
+as we'll explain:
+
+The call to `coerce` gives rise to:
+
+  Coercible (forall a.   m   (m a) ->   m a)
+            (forall a. T m (T m a) -> T m a)
+
+And that simplified to the following implication constraint:
+
+  forall a <no-ev>. m (T m a) ~R# m (m a)
+
+But because this constraint is under a `forall`, inside a type, we have to
+prove it *without computing any term evidence* (hence the <no-ev>). Alas, we
+*must* generate a term-level evidence binding in order to instantiate the
+quantified constraint! In response, GHC currently chooses not to use such
+a quantified constraint.
+See Note [Instances in no-evidence implications] in TcInteract.
+
+But this isn't the death knell for combining QuantifiedConstraints with GND.
+On the contrary, if we generate GND bindings in a slightly different way, then
+we can avoid this situation altogether. Instead of applying `coerce` to two
+polymorphic types, we instead let an explicit type signature do the polymorphic
+instantiation, and omit the `forall`s in the type applications.
+More concretely, we generate the following code instead:
+
+  instance (C m, forall p q. Coercible p q => Coercible (m p) (m q)) =>
+      C (T m) where
+    join = coerce @(  m   (m a) ->   m a)
+                  @(T m (T m a) -> T m a)
+                  join :: forall a. T m (T m a) -> T m a
+
+Now the visible type arguments are both monotypes, so we need do any of this
+funny quantified constraint instantiation business.
+
+You might think that that second @(T m (T m a) -> T m a) argument is redundant
+in the presence of the explicit `:: forall a. T m (T m a) -> T m a` type
+signature, but in fact leaving it off will break this example (from the
+T15290d test case):
+
+  class C a where
+    c :: Int -> forall b. b -> a
+
+  instance C Int
+
+  instance C Age where
+    c = coerce @(Int -> forall b. b -> Int)
+               c :: Int -> forall b. b -> Age
+
+That is because the explicit type signature deeply skolemizes the forall-bound
+`b`, which wreaks havoc with the `Coercible` solver. An additional visible type
+argument of @(Int -> forall b. b -> Age) is enough to prevent this.
+
+Be aware that the use of an explicit type signature doesn't /solve/ this
+problem; it just makes it less likely to occur. For example, if a class has
+a truly higher-rank type like so:
+
+  class CProblem m where
+    op :: (forall b. ... (m b) ...) -> Int
+
+Then the same situation will arise again. But at least it won't arise for the
+common case of methods with ordinary, prenex-quantified types.
 -}
 
 gen_Newtype_binds :: SrcSpan
 -}
 
 gen_Newtype_binds :: SrcSpan
@@ -1668,13 +1769,16 @@ gen_Newtype_binds loc cls inst_tvs inst_tys rhs_ty
                                           [] rhs_expr]
       where
         Pair from_ty to_ty = mkCoerceClassMethEqn cls inst_tvs inst_tys rhs_ty meth_id
                                           [] rhs_expr]
       where
         Pair from_ty to_ty = mkCoerceClassMethEqn cls inst_tvs inst_tys rhs_ty meth_id
+        (_, _, from_tau) = tcSplitSigmaTy from_ty
+        (_, _, to_tau)   = tcSplitSigmaTy to_ty
 
         meth_RDR = getRdrName meth_id
 
         rhs_expr = nlHsVar (getRdrName coerceId)
 
         meth_RDR = getRdrName meth_id
 
         rhs_expr = nlHsVar (getRdrName coerceId)
-                                      `nlHsAppType` from_ty
-                                      `nlHsAppType` to_ty
-                                      `nlHsApp`     nlHsVar meth_RDR
+                                      `nlHsAppType`     from_tau
+                                      `nlHsAppType`     to_tau
+                                      `nlHsApp`         nlHsVar meth_RDR
+                                      `nlExprWithTySig` to_ty
 
     mk_atf_inst :: TyCon -> TcM FamInst
     mk_atf_inst fam_tc = do
 
     mk_atf_inst :: TyCon -> TcM FamInst
     mk_atf_inst fam_tc = do
index acbbdd6..9f7ef67 100644 (file)
@@ -5,69 +5,61 @@ Derived class instances:
            GHC.Base.Functor (T14578.App f) where
     GHC.Base.fmap
       = GHC.Prim.coerce
            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
     (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
   
   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
     (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
     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)
             -> 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
     (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
     (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) =>
   
   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)
                -> 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
     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)
             -> 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
     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)
             -> 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:
   
 
 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 (file)
index 0000000..0ec4b5f
--- /dev/null
@@ -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 (file)
index 0000000..5aa9c71
--- /dev/null
@@ -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 (file)
index 0000000..f9fceb8
--- /dev/null
@@ -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
index 61b888e..a224871 100644 (file)
@@ -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('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('T14932', normal, compile, [''])
 test('T14933', normal, compile, [''])
+test('T15290c', normal, compile, [''])
+test('T15290d', normal, compile, [''])
index 7658b8e..87fd7e5 100644 (file)
@@ -1,22 +1,28 @@
 
 T15073.hs:8:12: error:
 
 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
       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))))
       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
       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)’
index 9642132..428f1a5 100644 (file)
@@ -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:
     • 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’:
       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
       When typechecking the code for ‘mkExpr’
         in a derived instance for ‘B BOOL’:
         To see the code I am typechecking, use -ddump-deriv