GitLab

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 foralls 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.