Deriving clauses can have forall types

mentioned in issue #14331

changed weight to 5

added Tbug Trac import deriving typechecker labels

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.

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?

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.

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.

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 that

it's a good design or that
it's implemented right

but it's there by design. I think there was a good reason for it too.

It appears to be undocumented in the user manual, which is bad.

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 ticket:14332#comment:143648, 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.

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.

Replying to [ticket:14332#comment:143656 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.

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 ticket:14332#comment:143657 should be rejected; the user should have to write Type, not k.

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

Right!

The example toward the end of ticket:14332#comment:143657 should be rejected

Which example, precisely?

Replying to [ticket:14332#comment:143666 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.

Replying to [ticket:14332#comment:143668 simonpj]:

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

Right!

The example toward the end of ticket:14332#comment:143657 should be rejected

Which example, precisely?

Oops. I meant ticket:14332#comment:143655.

I think I'm sold on this idea now, after hearing Simon's rationalization of it in #14331#ticket:14332#comment:143657.

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?

Replying to [ticket:14332#comment:143770 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 ticket:14332#comment:143666 is about. (I don't know if I could even give a proper definition of this word, let alone profitably implement it.)

Ryan, might you be able to do this?

I meant less than you think! I think.

In ticket:14332#comment:143770 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.

Replying to [ticket:14332#comment:144017 simonpj]:

In ticket:14332#comment:143770 I say that GHC is behaving right.

Except that it's clearly not, as evidenced in ticket:14332#comment:143656. 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 (closed) and #10561 (closed) in the past, as just two data points.

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:

diff --git a/compiler/parser/Parser.y b/compiler/parser/Parser.y
index af8c95f..7ad3025 100644
--- a/compiler/parser/Parser.y
+++ b/compiler/parser/Parser.y
@@ -1979,9 +1985,9 @@ inst_type :: { LHsSigType GhcPs }
         : 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.

Trac metadata

Trac field	Value
Related	- → #14331

mentioned in merge request !946 (merged)

On second thought, I retract my statement in #14332 (comment 162688), as I need the ability to parse explicit foralls in deriving clauses for a different task. I've opened !946 (merged) for this.

mentioned in commit e9b50621

mentioned in commit d07987db

mentioned in commit 8da29cea

mentioned in commit 4cc739eb

mentioned in commit b8683d7f

mentioned in commit ee2c5143

mentioned in commit 6dac6541

mentioned in commit fc83fb40

mentioned in commit 10831444

closed via commit 6eedbd83

Testsuite-tests: deriving/should_compile/T14332

mentioned in commit 6eedbd83

added Pnormal label

Trac field	Value
Version	8.2.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

Deriving clauses can have forall types

Child items 0

Activity

Deriving clauses can have forall types

Relates to

Activity