GND generates code that instantiates coerce too much
Consider this code from #18148 (comment 270603):
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
module Bug where
class Foo a where
bar :: forall (x :: a). ()
bar = ()
instance Foo Int
newtype Quux a = Quux a
-- deriving newtype instance _ => Foo (Quux Int)
deriving newtype instance Foo (Quux Int)
This typechecks in GHC 8.10.1. However, if you comment out the original deriving newtype instance Foo (Quux Int)
line and uncomment the very similar line above it, it no longer typechecks:
Bug.hs:19:1: error:
• Couldn't match type ‘Int’ with ‘Quux Int’
arising from the coercion of the method ‘bar’
from type ‘forall (x :: Int). ()’
to type ‘forall (x :: Quux Int). ()’
• When deriving the instance for (Foo (Quux Int))
|
19 | deriving newtype instance _ => Foo (Quux Int)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
This is a strange inconsistency, given how similar these standalone deriving
declarations are. Why does the original succeed but the line above it fail?
As it turns out, both of these really ought to fail, but the original only succeeds due to an unfortunate fluke in the way GeneralizedNewtypeDeriving
works. Here is the code that the original declaration generates (with -ddump-deriv
):
==================== Derived instances ====================
Derived class instances:
instance Bug.Foo (Bug.Quux GHC.Types.Int) where
Bug.bar
= GHC.Prim.coerce @() @() (Bug.bar @GHC.Types.Int) ::
forall (x_aKF :: Bug.Quux GHC.Types.Int). ()
Notice that we are instantiating coerce
with @() @()
. But this is blatantly wrong—it really ought to be coerce @(forall (x :: Int). ()) @(forall (x :: Quux Int). ())
, which the typechecker would reject (as it should). But GND generates coerce @() @()
instead, and as a result, the use of bar
on the RHS gets instantiated with @Any
, which is not what was intended at all.
In contrast, the deriving newtype instance _ => Foo (Quux Int)
line infers a Coercible (forall (x :: Int). ()) (forall (x :: Quux Int). ())
constraint, which the constraint solver rejects (as it should). The original line does not use the same constraint-inference machinery, so it bypasses this step.
What can be done about this? It's tempting to have the original declaration generate this code instead:
instance Foo (Quux Int) where
bar = coerce @(forall (x :: Int). ())
@(forall (x :: Quux Int). ())
bar
Sadly, doing so would break a number of test cases that involve quantified constraints in instance contexts, such as T15290
. See Note [GND and QuantifiedConstraints]
for the full story. In order to make these test cases succeed (as a part of the fix for #15290 (closed)), we employed an ugly hack where we split the forall
s off of any types used to instantiate coerce
in GND-generated code. But, as the example above demonstrates, this hack creates just as many problems as it solves.
@simonpj believes that this hack (and all of Note [GND and QuantifiedConstraints]
) could be avoided. I don't quite understand his grand vision, so I'll let him comment here about what his vision entails.
Another similar example of this bug arising can be found in #18148. However, that issue is ensnared in a separate discussion about the roles of arguments to type classes, as the examples in #18148 crucially involve ConstrainedClassMethods
. The underlying bug in this issue, on the other hand, does not fundamentally involve ConstrainedClassMethods
in any way, so @simonpj and I have decided to track it separately here.