[GHC] #14331: Overzealous free-floating kind check causes deriving clause to be rejected

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

[GHC] #14331: Overzealous free-floating kind check causes deriving clause to be rejected

GHC - devs mailing list
#14331: Overzealous free-floating kind check causes deriving clause to be rejected
-------------------------------------+-------------------------------------
           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 rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 GHC rejects this program:

 {{{#!hs
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PolyKinds #-}
 module Bug where

 class C a b

 data D = D deriving (C (a :: k))
 }}}

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

 Bug.hs:8:1: error:
     Kind variable ‘k’ is implicitly bound in datatype
     ‘D’, but does not appear as the kind of any
     of its type variables. Perhaps you meant
     to bind it (with TypeInType) explicitly somewhere?
   |
 8 | data D = D deriving (C (a :: k))
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 }}}

 But it really shouldn't, since it's quite possible to write the code that
 is should generate:

 {{{#!hs
 instance C (a :: k) D
 }}}

 Curiously, this does not appear to happen for data family instances, as
 this typechecks:

 {{{#!hs
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE TypeFamilies #-}
 module Bug where

 class C a b

 data family D1
 data instance D1 = D1 deriving (C (a :: k))

 class E where
   data D2

 instance E where
   data D2 = D2 deriving (C (a :: k))
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14331>
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] #14331: Overzealous free-floating kind check causes deriving clause to be rejected

GHC - devs mailing list
#14331: Overzealous free-floating kind check causes deriving clause to be rejected
-------------------------------------+-------------------------------------
        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 rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 I spoke too soon about that second program (with data families) working.
 It turns out that it's rejected on GHC HEAD:

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

 Bug.hs:10:1: error:
     • Kind variable ‘k’ is implicitly bound in data family
       ‘D1’, but does not appear as the kind of any
       of its type variables. Perhaps you meant
       to bind it (with TypeInType) explicitly somewhere?
     • In the data instance declaration for ‘D1’
    |
 10 | data instance D1 = D1 deriving (C (a :: k))
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

 Bug.hs:16:3: error:
     • Kind variable ‘k’ is implicitly bound in data family
       ‘D2’, but does not appear as the kind of any
       of its type variables. Perhaps you meant
       to bind it (with TypeInType) explicitly somewhere?
     • In the data instance declaration for ‘D2’
       In the instance declaration for ‘E’
    |
 16 |   data D2 = D2 deriving (C (a :: k))
    |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14331#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] #14331: Overzealous free-floating kind check causes deriving clause to be rejected

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14331: Overzealous free-floating kind check causes deriving clause to be rejected
-------------------------------------+-------------------------------------
        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 rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 I assume you really meant

 {{{#!hs
 data D = D deriving (forall k a. C (a :: k))
 }}}

 but that GHC doesn't quantify `k` the right way. So it's a bug in kind
 quantification, not the free-floating kind variable check.

 (Sidenote: that `forall` isn't allowed there. But perhaps it should be
 incorporated into [https://github.com/ghc-proposals/ghc-
 proposals/blob/master/proposals/0007-instance-foralls.rst the recent
 proposal expanding where `forall` can be used.)

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14331#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] #14331: Overzealous free-floating kind check causes deriving clause to be rejected

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14331: Overzealous free-floating kind check causes deriving clause to be rejected
-------------------------------------+-------------------------------------
        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 rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Replying to [comment:2 goldfire]:
 > I assume you really meant
 >
 > {{{#!hs
 > data D = D deriving (forall k a. C (a :: k))
 > }}}
 >
 > but that GHC doesn't quantify `k` the right way.

 I most certainly didn't. (In fact, I've opened a
 [https://ghc.haskell.org/trac/ghc/ticket/14332 separate bug] about the
 fact that you //can// put `forall`s in `deriving` clauses, which horrifies
 me.)

 It's somewhat surprising, but `deriving` clauses can bind type variables
 themselves. Note that this is currently accepted:

 {{{#!hs
 data D = D deriving (C a)
 }}}

 Here, `a` isn't bound by the data type `D`, so it is in fact bound in the
 `deriving` clause. By the same principle, `deriving (C (a :: k))` should
 be allowed, and the free-floating kind check is mistaken to reject it.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14331#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] #14331: Overzealous free-floating kind check causes deriving clause to be rejected

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14331: Overzealous free-floating kind check causes deriving clause to be rejected
-------------------------------------+-------------------------------------
        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 rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 So, if `deriving (C (a :: k))` doesn't mean to quantify, what do you
 expect it to mean? I agree that the current error is wrong, but I'm not
 sure what behavior you want GHC to take here.

 If you want GHC to accept your original declaration, creating `instance
 forall k (a :: k). C a D`, then we're basically in agreement.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14331#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] #14331: Overzealous free-floating kind check causes deriving clause to be rejected

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14331: Overzealous free-floating kind check causes deriving clause to be rejected
-------------------------------------+-------------------------------------
        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 rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 I meant exactly what I wrote in the original description: it should emit:

 {{{#!hs
 instance C (a :: k) D
 }}}

 After all, the user wrote `deriving (C (a :: k))`, and the data type is
 `D`. What you get after doing the whole `deriving` macro-application-eta-
 reduction-kind-unification shebang is `C (a :: k) D`.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14331#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] #14331: Overzealous free-floating kind check causes deriving clause to be rejected

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14331: Overzealous free-floating kind check causes deriving clause to be rejected
-------------------------------------+-------------------------------------
        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 rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 But I see `instance C (a :: k) D` as fully equivalent to `instance forall
 k (a :: k). C a D`. They just make different things explicit, but both
 declarations have the same static and dynamic semantics.

 And, I don't quite agree that clauses in a `deriving` are macro-like. They
 are types of kind `... -> Type -> Constraint`, where the `...` may be
 empty. My desire to put `forall` in there is more macro-like, I admit...
 but no more so than the syntax for pattern synonym types or even GADT
 constructor types.

 I believe that you are genuinely confused here. But I'm afraid I'm equally
 confused as to why you're confused.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14331#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] #14331: Overzealous free-floating kind check causes deriving clause to be rejected

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14331: Overzealous free-floating kind check causes deriving clause to be rejected
-------------------------------------+-------------------------------------
        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 rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Replying to [comment:6 goldfire]:
 > But I see `instance C (a :: k) D` as fully equivalent to `instance
 forall k (a :: k). C a D`. They just make different things explicit, but
 both declarations have the same static and dynamic semantics.

 Yes, agreed.

 > And, I don't quite agree that clauses in a `deriving` are macro-like.
 They are types of kind `... -> Type -> Constraint`, where the `...` may be
 empty.

 Surely you mean kind `k -> Constraint`? You certainly can't say `deriving
 Z`, where `class Z a b`, for instance.

 To elaborate what I mean by "macro" here: yes, the `C c1 ... cn` in
 `deriving (C c1 ... cn)` is a type, and one that is thrust into the
 typechecker at one point as a sanity-check to make sure you aren't writing
 utter garbage. But it's not like other types in that `C c1 ... cn` doesn't
 appear on its own in the emitted code—it only makes sense to talk about `C
 c1 ... cn` in the final program //after it has been combined// with its
 corresponding data type. Trying to stick `forall`s on just `C c1 ... cn`
 feels nonsensical, because the scoping needs to happen for the whole
 derived instance, not just `C c1 ... cn`, which happens to be one part of
 the recipe.

 > I believe that you are genuinely confused here. But I'm afraid I'm
 equally confused as to why you're confused.

 The thing that I am confused on above all else is this business on skolems
 you mention in https://ghc.haskell.org/trac/ghc/ticket/14332#comment:9,
 and why the user-written kinds of a data type's type variables don't fall
 under the same scrutiny. I can't even begin to understand how this would
 work without an explanation of what is motivating this design choice.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14331#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] #14331: Overzealous free-floating kind check causes deriving clause to be rejected

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14331: Overzealous free-floating kind check causes deriving clause to be rejected
-------------------------------------+-------------------------------------
        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 rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 > Trying to stick foralls on just C c1 ... cn feels nonsensical,

 You could try not thinking of them as foralls.  Say
 {{{
 data D = D deriving ({k a}. C (a :: k))
 }}}
 where I'm using `{k a}` to bring `k` and `a` into scope.

 But they ARE skolems. I'm sure you wouldn't be happy with
 {{{
 data D = D deriving( {a}. C a }
 }}}
 it the derived instance declaration ended up being
 {{{
 instance C Int D
 }}}
 where the `a` gets unified with `Int` somehow.  (Fundeps or something.)
 This quantification is ''per-deriving-clause''.  If you say `a` you mean
 `a` and not `Int`!

 > why the user-written kinds of a data type's type variables don't fall
 under the same scrutiny

 Because they are shared across the data type decl itself, ''and'' all the
 deriving clauses. So in
 {{{
 data Proxy k (a :: k) = Proxy deriving(  Functor, ...others... )
 }}}
 the `Functor` instance only makes sense when `k=*`, so we specialise it to
 that
 {{{
   instance GHC.Base.Functor (Main.Proxy *) where
 }}}
 We ''can't'' turn that `k` into `*` in the decl without crippling `Proxy`.

 To put it another way:
 * The kind binders in the data decl belong to the data decl
 * The freshly bound variables in the deriving clause belong to the
 instance decl
 * Naturally, the quantified variables of the data decl may be instantiated
 in the instance decl.

 Does that help?

 Is this essentially the same ticket as #14332?  Can we combine?

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14331#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] #14331: Overzealous free-floating kind check causes deriving clause to be rejected

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14331: Overzealous free-floating kind check causes deriving clause to be rejected
-------------------------------------+-------------------------------------
        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 rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Replying to [comment:8 simonpj]:
 > Does that help?

 Thank you Simon, that was the careful explanation I was searching for. I
 think I'm sold on this idea now.

 > Is this essentially the same ticket as #14332?  Can we combine?

 I'm not sure. Do we know for sure that the bug described in this ticket is
 caused by a deficient treatment of quantification in `deriving` clauses?

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14331#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] #14331: Overzealous free-floating kind check causes deriving clause to be rejected

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14331: Overzealous free-floating kind check causes deriving clause to be rejected
-------------------------------------+-------------------------------------
        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 rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by Simon Peyton Jones <simonpj@…>):

 In [changeset:"82b77ec375ab74678ac2afecf55dc574fa24490f/ghc" 82b77ec/ghc]:
 {{{
 #!CommitTicketReference repository="ghc"
 revision="82b77ec375ab74678ac2afecf55dc574fa24490f"
 Do not quantify over deriving clauses

 Trac #14331 showed that in a data type decl like

    data D = D deriving (C (a :: k))

 we were quantifying D over the 'k' in the deriving clause.  Yikes.

 Easily fixed, by deleting code in RnTypes.extractDataDefnKindVars

 See the discussion on the ticket, esp comment:8.
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14331#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] #14331: Overzealous free-floating kind check causes deriving clause to be rejected

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14331: Overzealous free-floating kind check causes deriving clause to be rejected
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  merge
        Priority:  normal            |            Milestone:  8.2.2
       Component:  Compiler (Type    |              Version:  8.2.1
  checker)                           |
      Resolution:                    |             Keywords:  deriving
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  GHC rejects       |            Test Case:
  valid program                      |  deriving/should_compile/T14331
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by simonpj):

 * status:  new => merge
 * testcase:   => deriving/should_compile/T14331
 * milestone:   => 8.2.2


Comment:

 OK I fixed the bug for this ticket.  Remaining work is on #14332.

 Merge if/when convenient.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14331#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] #14331: Overzealous free-floating kind check causes deriving clause to be rejected

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14331: Overzealous free-floating kind check causes deriving clause to be rejected
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  merge
        Priority:  normal            |            Milestone:  8.2.2
       Component:  Compiler (Type    |              Version:  8.2.1
  checker)                           |
      Resolution:                    |             Keywords:  deriving
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  GHC rejects       |            Test Case:
  valid program                      |  deriving/should_compile/T14331
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 I still don't think this is quite right. Look at what happens now when you
 try to compile this variation of the original program:

 {{{#!hs
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PolyKinds #-}
 module Bug where

 class C a b

 data D a = D deriving (C (a :: k))
 }}}
 {{{
 GHCi, version 8.3.20171011: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )

 Bug.hs:8:27: error:
     • Expected kind ‘k1’, but ‘a’ has kind ‘k’
     • In the first argument of ‘C’, namely ‘(a :: k)’
       In the data declaration for ‘D’
   |
 8 | data D a = D deriving (C (a :: k))
   |                           ^
 }}}

 This is wrong—the `a` in `D a` and `C a` should have the same kind, since
 they're the same `a`.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14331#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] #14331: Overzealous free-floating kind check causes deriving clause to be rejected

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14331: Overzealous free-floating kind check causes deriving clause to be rejected
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  merge
        Priority:  normal            |            Milestone:  8.2.2
       Component:  Compiler (Type    |              Version:  8.2.1
  checker)                           |
      Resolution:                    |             Keywords:  deriving
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  GHC rejects       |            Test Case:
  valid program                      |  deriving/should_compile/T14331
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 I agree.  After elaboration we expect
 {{{
 class C {k1 k2} (p::k1) (q::k2)
 data D {k3} (r::k3) = D

 instance forall {k2} k (a:k) (b:k2). C a (D {k2} b) where ...
 }}}
 So we instantiate the `k3` belonging to the data declaration to `k2`
 belonging to the instance.  The `forall k` in the `deriving` clause is
 just the kind on `a`, the first parameter for `C`.

 Right?

 Why this doesn't work I don't know.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14331#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] #14331: Overzealous free-floating kind check causes deriving clause to be rejected

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14331: Overzealous free-floating kind check causes deriving clause to be rejected
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  merge
        Priority:  normal            |            Milestone:  8.2.2
       Component:  Compiler (Type    |              Version:  8.2.1
  checker)                           |
      Resolution:                    |             Keywords:  deriving
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  GHC rejects       |            Test Case:
  valid program                      |  deriving/should_compile/T14331
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Huh? That is not what I would have expected at all. I would have expected:

 {{{#!hs
 class C {k1 k2} (a :: k1) (b :: k2)
 data D {k3} (r :: k3) = D

 instance forall k1 (a :: k1). C a (D a) where ...
 }}}

 In other words, you should unify `r` with `a`. After all, the `a` in `data
 D a = D deriving (C (a :: k))` scopes over the data type, not the
 `deriving` clause!

 Now if you had chosen to use a different scoping with `data D a = D
 deriving (forall (a :: k). C a)`, //then// I could see the instance being
 derived that you suggested. But I don't think users would expect that
 behavior to be the default (that is, in lieu of explicit `forall`s on a
 `deriving` clause, one should assume that the user-written type variables
 are bound by the data type if they appear in the `<tvbs>` in `data D
 <tvbs>`).

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14331#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] #14331: Overzealous free-floating kind check causes deriving clause to be rejected

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14331: Overzealous free-floating kind check causes deriving clause to be rejected
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  merge
        Priority:  normal            |            Milestone:  8.2.2
       Component:  Compiler (Type    |              Version:  8.2.1
  checker)                           |
      Resolution:                    |             Keywords:  deriving
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  GHC rejects       |            Test Case:
  valid program                      |  deriving/should_compile/T14331
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 For what it's worth, I agree with Ryan in what GHC should do here.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14331#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] #14331: Overzealous free-floating kind check causes deriving clause to be rejected

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14331: Overzealous free-floating kind check causes deriving clause to be rejected
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  merge
        Priority:  normal            |            Milestone:  8.2.2
       Component:  Compiler (Type    |              Version:  8.2.1
  checker)                           |
      Resolution:                    |             Keywords:  deriving
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  GHC rejects       |            Test Case:
  valid program                      |  deriving/should_compile/T14331
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Ah yes, you're right.   I was focusing on the `k`, but there's the `a` as
 well.

 But then I'd say that the error message is dead right.
 Let's put the implicit binders in:
 {{{
 data D {k1} (a::k1) = D deriving (forall k. C (a :: k))
 }}}
 Look at that!  `a` has kind `k1`; but in the `deriving` clause we claim
 that
 the occurrence of `a` ahs type `k`.  Boom.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14331#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] #14331: Overzealous free-floating kind check causes deriving clause to be rejected

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14331: Overzealous free-floating kind check causes deriving clause to be rejected
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  merge
        Priority:  normal            |            Milestone:  8.2.2
       Component:  Compiler (Type    |              Version:  8.2.1
  checker)                           |
      Resolution:                    |             Keywords:  deriving
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  GHC rejects       |            Test Case:
  valid program                      |  deriving/should_compile/T14331
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 I don't understand your reasoning in comment:16. After all, we don't
 reject this:

 {{{#!hs
 {-# LANGUAGE TypeInType #-}

 import Data.Proxy

 data Foo a = Foo (Proxy (a :: k))
 }}}

 After all, `k` is implicitly bound by the datatype `D`, so everything
 works out. The same situation applies in:

 {{{#!hs
 data D a = D deriving (C (a :: k))
 }}}

 Once again, `k` is implicitly bound by `D`, so `k` and the kind of `a` are
 one and the same.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14331#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
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14331: Overzealous free-floating kind check causes deriving clause to be rejected

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14331: Overzealous free-floating kind check causes deriving clause to be rejected
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  merge
        Priority:  normal            |            Milestone:  8.2.2
       Component:  Compiler (Type    |              Version:  8.2.1
  checker)                           |
      Resolution:                    |             Keywords:  deriving
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  GHC rejects       |            Test Case:
  valid program                      |  deriving/should_compile/T14331
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 I'm not convinced by comment:17, as I consider `deriving` clauses to be
 more separate from the definition. My reasoning is that we do unification
 for deriving. Thus, the kind `k2` of `a` will be unified with the newly-
 quantified kind `k`, leading to an accepted definition.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14331#comment:18>
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] #14331: Overzealous free-floating kind check causes deriving clause to be rejected

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14331: Overzealous free-floating kind check causes deriving clause to be rejected
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  merge
        Priority:  normal            |            Milestone:  8.2.2
       Component:  Compiler (Type    |              Version:  8.2.1
  checker)                           |
      Resolution:                    |             Keywords:  deriving
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  GHC rejects       |            Test Case:
  valid program                      |  deriving/should_compile/T14331
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 It will lead to an accepting definition, yes, but I don't think it's the
 definition you'd want (or at least, it seems to differ from the proposal I
 put forth in comment:14). If I understand your argument correctly, you
 want all type variables in a `deriving` clause's type to be scoped
 differently from the data type, and expect unification to save you in the
 end? That is, this:

 {{{#!hs
 data D a = D deriving (C (a :: k))
 }}}

 Would be treated like this?

 {{{#!hs
 data D {k1} (a1 :: k1) = D deriving (forall {j} k (a :: k). C @k @j a)
 }}}

 If so, we have a problem—the //only// kinds we'd unify are the `j` in `C a
 :: j -> Constraint` and `Type` (the kind of `D a`), so the instance we'd
 get in the end is:

 {{{#!hs
 instance forall {k1} k {a1 :: k1} (a :: k). C @k @Type a (D @k1 a1) where
 ...
 }}}

 Which is not what I'd expect, since `a` and `a1` are distinct. The only
 way to ensure that they're the same is to interpret the scope like this:

 {{{#!hs
 data D {k} (a :: k) = D deriving (forall {j}. C @k @j a)
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14331#comment:19>
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
12