Commit 132273f3 authored by Ryan Scott's avatar Ryan Scott
Browse files

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
parent 93b7ac8d
......@@ -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)
(==)
(==) :: Glurp a -> Glurp a -> Bool
(Where the visible type applications use types produced by typeToLHsType.)
......
......@@ -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)
(==)
(==) :: 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
......
......@@ -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
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,
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
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.
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
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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -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
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.
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
......@@ -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
(_, _, from_tau) = tcSplitSigmaTy from_ty
(_, _, to_tau) = tcSplitSigmaTy to_ty
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
......
......@@ -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:
......
{-# 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)
{-# 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)
{-# 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
......@@ -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, [''])
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)’
......@@ -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
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment