Deriving clauses can have forall types

[RyanGlScott]

I made a horrifying discovery today: GHC accepts this code!

{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# OPTIONS_GHC -ddump-deriv #-}
module Bug1 where

class C a b

data D a = D deriving ((forall a. C a))

GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug1             ( Bug.hs, interpreted )

==================== Derived instances ====================
Derived class instances:
  instance Bug1.C a1 (Bug1.D a2) where
  

Derived type family instances:


Ok, 1 module loaded.

It gets even worse with this example:

{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}
{-# OPTIONS_GHC -ddump-deriv -fprint-explicit-kinds #-}
module Bug1 where

import Data.Kind
import GHC.Generics

data Proxy (a :: k) = Proxy
  deriving ((forall k. (Generic1 :: (k -> Type) -> Constraint)))

GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug1             ( Bug.hs, interpreted )

==================== Derived instances ====================
Derived class instances:
  instance GHC.Generics.Generic1 k (Bug1.Proxy k) where
    GHC.Generics.from1 x_a3ip
      = GHC.Generics.M1
          (case x_a3ip of { Bug1.Proxy -> GHC.Generics.M1 GHC.Generics.U1 })
    GHC.Generics.to1 (GHC.Generics.M1 x_a3iq)
      = case x_a3iq of {
          (GHC.Generics.M1 GHC.Generics.U1) -> Bug1.Proxy }
  

Derived type family instances:
  type GHC.Generics.Rep1 k_a2mY (Bug1.Proxy k_a2mY) = GHC.Generics.D1
                                                        k_a2mY
                                                        ('GHC.Generics.MetaData
                                                           "Proxy" "Bug1" "main" 'GHC.Types.False)
                                                        (GHC.Generics.C1
                                                           k_a2mY
                                                           ('GHC.Generics.MetaCons
                                                              "Proxy"
                                                              'GHC.Generics.PrefixI
                                                              'GHC.Types.False)
                                                           (GHC.Generics.U1 k_a2mY))


Ok, 1 module loaded.

In this example, the forall'd k from the deriving clause is discarded and then unified with the k from data Proxy (a :: k).

All of this is incredibly unsettling. We really shouldn't be allowing forall types in deriving clauses in the first place.

[goldfire]

Why shouldn't we allow forall in deriving clauses? I agree that the current implementation is buggy (for example, that you need two sets of parens!), but I think foralls there are just peachy.

[RyanGlScott]

To my knowledge, there's no formalism that states what the static semantics of deriving clauses are, so saying what should or shouldn't be allowed leaves a lot up to personal interpretation. But I can at least give my interpretation: whenever something of the form:

data D d1 ... dn = ... deriving (C c1 ... cm)

is encountered, then an instance of the form:

instance ... => C c1 ... cm (D d1 ... dn)

is emitted. To put it less formally, one takes the derived type and plops the datatype to the right of it, forming the instance.

Having established this, let me turn the tables on you and ask: what do you think should happen if something of this form is encountered?

data D d1 ... dn = ... deriving (forall <...>. C c1 ... cm)

I for one can't come up with a consistent semantics for this. Do you emit this?

instance ... => (forall <...>. C c1 ... cm) (D d1 ... dn)

Clearly not, since instances have to be headed by an actual type class constructor. So do you attempt to beta-reduce the forall'd type? What happens if there is more than one forall'd type variable?

In my view, trying to make sense of this is opening up a giant can of worms. I'm open to being proved wrong though—is there an interpretation of this which makes sense, and has a consistent semantics?

[goldfire]

I intended to move the forall to the left of the context. So deriving (forall <...>. C tys) is like instance forall <...>. ... => C tys. That's nice and simple, I think.

[RyanGlScott]

OK, that's a start. But I have more questions:

• Are the forall'd type variables in a deriving clause's type assumed to be distinct from the type variables bound by a data type itself? If so, how should GHC treat derived instances that would only work if kind unification were to occur? For instance, data Proxy (a :: k) = Proxy deriving (Generic1 :: (k -> Type) -> Constraint) is clearly OK, but data Proxy (a :: k) = Proxy deriving (forall k. Generic1 :: (k -> Type) -> Constraint) isn't, since it can't unify the k from the derived type and the k from the datatype. What should GHC do here?
• What happens if one of the variables isn't quantified over (e.g., data D = D deriving (forall a. C a b))? Is this an error?

Many I'd be convinced if I did see a full write-up of this in a proposal. But as it stands, I'm quite unconvinced that this would work out if you actually sat down and attempted to implement this.

[simonpj]

I intended to move the forall to the left of the context.

Aha, that makes a huge difference. I thought you were advocating generating a derived instance like

instance ... => C (forall k. T k a) where ...

which would be bad. (We don't allow that in source code, so we shouldn't in deriving-generated code.)

But if you mean just moving the foralls to the left, then we've supported that for ages in the abstract syntax

data HsDerivingClause pass
  -- See Note [Deriving strategies] in TcDeriv
  = HsDerivingClause
    { deriv_clause_strategy :: Maybe (Located DerivStrategy)
      -- ^ The user-specified strategy (if any) to use when deriving
      -- 'deriv_clause_tys'.
    , deriv_clause_tys :: Located [LHsSigType pass]
      -- ^ The types to derive.
      --
      -- It uses 'LHsSigType's because, with @-XGeneralizedNewtypeDeriving@,
      -- we can mention type variables that aren't bound by the datatype, e.g.
      --
      -- > data T b = ... deriving (C [a])
      --
      -- should produce a derived instance for @C [a] (T b)@.
    }

Note the LHsSigType and comment.

I'm not saying it's implemented right, and it appears to be undocumented in the user manual, but it's there by design.

[RyanGlScott]

I'm well aware of the fact that deriv_clause_tys uses LHsSigType. That is indeed there for a good reason—deriving clauses need to support implicit quantification. But just because LHsSigType supports explicit quantification via foralls doesn't mean it's a good idea to actually allow them in deriving clauses. After all, the fact that we use LHsSigType in class instances means that it's possible to write instances with nested foralls, like this:

instance forall a. forall b. (Show a, Show b) => Show (Either a b)

But despite this, GHC will reject this will Malformed instance: forall a. forall b. Show (Either a b). Similarly, we should think carefully about whether deriving (forall <<>>. C c1 ... cn) well formed or not.

I thought about this some more last night, and another reason why deriving (forall <<>>. C c1 ... cn) bothers me is because unlike the forall in a class instance, this proposed forall in a deriving clause doesn't scope over a "real" type in some ways. That is to say, the C c1 ... cn in deriving C c1 ... cn isn't so much of a type as a "type former". There is a rather involved process in taking C c1 ... cn, applying it to the datatype (possibly after eta reducing some of its type variables), and unifying their kinds. In fact, after this kind unification, it's possible that some of these type variables will vanish completely! Take this example, for instance:

{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeInType #-}
{-# OPTIONS_GHC -ddump-deriv #-}

class C k (a :: k)

data D = D deriving (C k)

Here, the actual instance that gets emitted (as shown by -ddump-deriv) is:

GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/ryanglscott/.ghci
[1 of 1] Compiling Main             ( Bug.hs, interpreted )

==================== Derived instances ====================
Derived class instances:
  instance Main.C * Main.D where

Notice how the k has become * due to kind unification! But according to this proposal, you could have alternatively written this as:

data D = D deriving (forall k. C k)

And according to the specification given in comment:3, this should emit an instance of the form forall k. ... => C k D. But that's clearly not true when you inspect -ddump-deriv! So this forall here is an utter lie.

[simonpj]

Notice how the k has become * due to kind unification!

I'd say this is an outright bug. You should say

data D = D deriving (C Type)

Would you like to open a ticket?

I grant that it's odd to quantify over a type former. But it's odd not to have ANY way to explicitly quantify. (Well, I suppose you could use standalone deriving.)

I'm not pressing hard for an explicit forall.

[RyanGlScott]

Replying to simonpj:

I'd say this is an outright bug. You should say

data D = D deriving (C Type)

Would you like to open a ticket?

No, because this is behaving as I would expect it to! Kind unification is fundamental to the way deriving works, and I'm leery of any design which doesn't incorporate it as a guiding principle. Here is another example where deriving must unify kinds:

{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeInType #-}
{-# OPTIONS_GHC -ddump-deriv #-}

data Proxy k (a :: k) = Proxy deriving Functor

GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/ryanglscott/.ghci
[1 of 1] Compiling Main             ( Bug.hs, interpreted )

==================== Derived instances ====================
Derived class instances:
  instance GHC.Base.Functor (Main.Proxy *) where

Here, if k weren't unified with *, then the instance simply wouldn't be well kinded.

How about another example?

{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeInType #-}
{-# OPTIONS_GHC -ddump-deriv #-}

import Data.Kind

class C k (f :: k -> *)

data T j (a :: j) deriving (C k)

GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/ryanglscott/.ghci
[1 of 1] Compiling Main             ( Bug.hs, interpreted )

==================== Derived instances ====================
Derived class instances:
  instance Main.C k (Main.T k) where

Notice that GHC didn't attempt to emit an instance of the form forall k j. C k (T j)—instead, it deliberately unified k and j! This is a good thing, because otherwise GHC would spit out utter nonsense that wouldn't pass muster.

[goldfire]

In both of your examples, IIUC, the unification happens to the datatype variables, not the newly-quantified variables in the deriving clause. I agree that this kind unification is good. I further agree that any unwritten kinds in a deriving clause should be unified. But I think any explicitly written kinds are skolems, and that this doesn't cause problems.

The example toward the end of comment:8 should be rejected; the user should have to write Type, not k.

[simonpj]

But I think any explicitly written kinds are skolems, and that this doesn't cause problems.

Right!

The example toward the end of comment:8 should be rejected

Which example, precisely?

[RyanGlScott]

Replying to goldfire:

In both of your examples, IIUC, the unification happens to the datatype variables, not the newly-quantified variables in the deriving clause. I agree that this kind unification is good. I further agree that any unwritten kinds in a deriving clause should be unified.

I am baffled as to why we are drawing these arbitrary distinctions among slightly different positionings of kind variables in a data declaration. I want to believe that there is some overarching principle behind these viewpoints, but it's either not spelled out anywhere, or I'm too dense to discern it from the subtext (or both).

But I think any explicitly written kinds are skolems, and that this doesn't cause problems.

OK. But in data Proxy (a :: k) = Proxy deriving Functor, k is also a user-written kind! Why should this not be considered rigid, but the k in data D = D deriving (C k) should be considered rigid?

I swear I'm not trying to be contrarian here simply to be stubborn. But from my viewpoint, all of these proposed changes are adding a ton of complexity, and moreover, they are ruling out classes of programs that currently typecheck. I don't think it's healthy to view the C c1 ... cn in deriving (C1 ... cn) like the types in other class instance heads, because C c1 ... cn isn't like other types—it's a macro, not a standalone thing. We shouldn't foist our biases of other types onto this construct, which is quite different from anything else in Haskell.

[goldfire]

Replying to simonpj:

But I think any explicitly written kinds are skolems, and that this doesn't cause problems.

Right!

The example toward the end of comment:8 should be rejected

Which example, precisely?

Oops. I meant comment:6.

[RyanGlScott]

I think I'm sold on this idea now, after hearing Simon's rationalization of it in ​https://ghc.haskell.org/trac/ghc/ticket/14331#comment:8.

[simonpj]

OK, so to review:

• We need to write up ​the rationalisation in the user manual.

• If we are going to make it a proper feature (which it already is), we should not require silly parens. E.g. this example from the Description

  data D a = D deriving ((forall a. C a))
  

  works just as we intend, but should not require the second pair of parens -- a parser bug.

• The second example from the Description is also OK

  data Proxy (a :: k) = Proxy
    deriving ((forall k2. (Generic1 :: (k2 -> Type) -> Constraint)))
  

  As I put it in the rationalisation, k comes from the data type decl, and k2 from the instance; but it's fine to instantiate k to k2 in that instance decl. And that is just what happens. Worth an example in the user manual perhaps, after the one about Functor Proxy.

Ryan, might you be able to do this?

[RyanGlScott]

Replying to simonpj:

Ryan, might you be able to do this?

Er, I doubt it. This sounds like it goes well beyond my abilities as a GHC hacker, since it requires intricate knowledge of:

• Somehow informing GHC of which type variables are "OK to unify" for instance, the k in data Proxy (a :: k) is OK to unify, but the k in deriving (C (a :: k)) is not—what is the secret sauce in GHC to specify this? I have no idea.

Actually, it's even more subtle than that. There are scenarios when you'd want to unify kind variables in deriving types: when they're invisible. For instance:

newtype Identity a = Identity a deriving Generic1

Here, Generic1 :: (k -> *) -> Constraint. But note that we never write k explicitly, so it's more like deriving (Generic1 {k}). However, we ultimately unify k with * in the end, giving us deriving (Generic1 {*}). Somehow, we also have to inform GHC that this is OK. Urp...

• WTF this "skolem" business from comment:9 is about. (I don't know if I could even give a proper definition of this word, let alone profitably implement it.)

[simonpj]

Ryan, might you be able to do this?

I meant less than you think! I think.

In comment:14 I say that GHC is behaving right. We just need

• Document the behaviour and rationale in the user manual.
• Make it work without requirinng extra parens (this is mostly just syuntax I think
• Add an example in the manual along the lines of the second example.

In short, virtually no implementation, just documentation.

You seem to think I'm asking for something subtle in the implementationn, but I'm not.

[RyanGlScott]

Replying to simonpj:

In comment:14 I say that GHC is behaving right.

Except that it's clearly not, as evidenced in comment:7. I don't see a way to fix that short of overhauling how deriving clauses are renamed/typechecked, which I don't feel like I'd be able to accomplish without some mentoring.

You seem to think I'm asking for something subtle in the implementationn, but I'm not.

I firmly disagree here—the way GHC typechecks deriving clauses is ripe with subtlety! It's caused me endless amounts of headaches trying to fix bugs like #10524 and #10561 in the past, as just two data points.

[RyanGlScott]

It turns out that the changes in the parser necessary to accommodate foralls in deriving clauses (without the double parentheses junk) is essentially just this:

compiler/parser/Parser.y

@@ -1979 +1985 @@
         : sigtype                       { mkLHsSigType $1 }
 
 deriv_types :: { [LHsSigType GhcPs] }
-        : typedoc                       { [mkLHsSigType $1] }
+        : ktypedoc                     { [mkLHsSigType $1] }
 
-        | typedoc ',' deriv_types       {% addAnnotation (gl $1) AnnComma (gl $2)
+        | ktypedoc ',' deriv_types     {% addAnnotation (gl $1) AnnComma (gl $2)
                                            >> return (mkLHsSigType $1 : $3) }
 
 comma_types0  :: { [LHsType GhcPs] }  -- Zero or more:  ty,ty,ty

I'm not going to open a Diff for this now, since it would be nice to combine the fix for this ticket with that of #14331. But I'll record this here for posterity's sake.

[Marge Bot <ben+marge-bot@…>]

In 6eedbd83/ghc:

Some forall-related cleanup in deriving code

* Tweak the parser to allow `deriving` clauses to mention explicit
  `forall`s or kind signatures without gratuitous parentheses.
  (This fixes #14332 as a consequence.)
* Allow Haddock comments on `deriving` clauses with explicit
  `forall`s. This requires corresponding changes in Haddock.