[GHC] #14332: Deriving clauses can have forall types
#14332: Deriving clauses can have forall types -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 (Type checker) | Keywords: deriving | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC accepts Unknown/Multiple | invalid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- I made a horrifying discovery today: GHC accepts this code! {{{#!hs {-# 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: {{{#!hs {-# 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14332 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14332: Deriving clauses can have forall types -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: deriving Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by 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 `forall`s there are just peachy. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14332#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14332: Deriving clauses can have forall types -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: deriving Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by 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: {{{#!hs data D d1 ... dn = ... deriving (C c1 ... cm) }}} is encountered, then an instance of the form: {{{#!hs 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? {{{#!hs 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? {{{#!hs 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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14332#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14332: Deriving clauses can have forall types -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: deriving Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14332#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14332: Deriving clauses can have forall types -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: deriving Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14332#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14332: Deriving clauses can have forall types -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: deriving Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14332#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14332: Deriving clauses can have forall types -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: deriving Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by 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 `forall`s 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 `forall`s, like this: {{{#!hs 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: {{{#!hs {-# 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: {{{#!hs 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14332#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14332: Deriving clauses can have forall types -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: deriving Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14332#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14332: Deriving clauses can have forall types -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: deriving Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:7 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: {{{#!hs {-# 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? {{{#!hs {-# 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14332#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14332: Deriving clauses can have forall types -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: deriving Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by 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`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14332#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14332: Deriving clauses can have forall types -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: deriving Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by 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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14332#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14332: Deriving clauses can have forall types -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: deriving Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:9 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14332#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14332: Deriving clauses can have forall types -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: deriving Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:10 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14332#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14332: Deriving clauses can have forall types -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: deriving Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14332#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14332: Deriving clauses can have forall types -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: deriving Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): OK, so to review: * We need to write up [https://ghc.haskell.org/trac/ghc/ticket/14331#comment:8 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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14332#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14332: Deriving clauses can have forall types -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: deriving Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:14 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: {{{#!hs 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.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14332#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14332: Deriving clauses can have forall types -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: deriving Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14332#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14332: Deriving clauses can have forall types -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: deriving Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:16 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14332#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14332: Deriving clauses can have forall types -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: deriving Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: #14331 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: => #14331 Comment: It turns out that the changes in the parser necessary to accommodate `forall`s in `deriving` clauses (without the double parentheses junk) is essentially just this: {{{#!diff 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14332#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC