[GHC] #14332: Deriving clauses can have forall types

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
18 messages Options
Reply | Threaded
Open this post in threaded view
|

[GHC] #14332: Deriving clauses can have forall types

GHC - devs mailing list
#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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14332: Deriving clauses can have forall types

GHC - devs mailing list
#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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14332: Deriving clauses can have forall types

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14332: Deriving clauses can have forall types

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14332: Deriving clauses can have forall types

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14332: Deriving clauses can have forall types

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14332: Deriving clauses can have forall types

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14332: Deriving clauses can have forall types

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14332: Deriving clauses can have forall types

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14332: Deriving clauses can have forall types

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14332: Deriving clauses can have forall types

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14332: Deriving clauses can have forall types

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14332: Deriving clauses can have forall types

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14332: Deriving clauses can have forall types

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14332: Deriving clauses can have forall types

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14332: Deriving clauses can have forall types

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14332: Deriving clauses can have forall types

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14332: Deriving clauses can have forall types

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets