[GHC] #14808: GHC HEAD regression: GADT constructors no longer quantify tyvars in topological order

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

[GHC] #14808: GHC HEAD regression: GADT constructors no longer quantify tyvars in topological order

GHC - devs mailing list
#14808: GHC HEAD regression: GADT constructors no longer quantify tyvars in
topological order
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  highest        |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.5
  (Type checker)                     |
           Keywords:  GADTs          |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:  #14529, #14796
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Originally noticed in #14796. This program:

 {{{#!hs
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE TypeApplications #-}
 module Bug where

 import Data.Kind

 data ECC ctx f a where
   ECC :: ctx => f a -> ECC ctx f a

 f :: [()] -> ECC () [] ()
 f = ECC @() @[] @()
 }}}

 Typechecks in GHC 8.2.2 and 8.4.1, but not in GHC HEAD:

 {{{
 $ ~/Software/ghc2/inplace/bin/ghc-stage2 Bug.hs
 [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

 Bug.hs:12:5: error:
     • Couldn't match type ‘()’ with ‘[]’
       Expected type: [()] -> ECC (() :: Constraint) [] ()
         Actual type: () [] -> ECC (() :: Constraint) () []
     • In the expression: ECC @() @[] @()
       In an equation for ‘f’: f = ECC @() @[] @()
    |
 12 | f = ECC @() @[] @()
    |     ^^^^^^^^^^^^^^^

 Bug.hs:12:10: error:
     • Expected kind ‘* -> *’, but ‘()’ has kind ‘*’
     • In the type ‘()’
       In the expression: ECC @() @[] @()
       In an equation for ‘f’: f = ECC @() @[] @()
    |
 12 | f = ECC @() @[] @()
    |          ^^

 Bug.hs:12:14: error:
     • Expecting one more argument to ‘[]’
       Expected a type, but ‘[]’ has kind ‘* -> *’
     • In the type ‘[]’
       In the expression: ECC @() @[] @()
       In an equation for ‘f’: f = ECC @() @[] @()
    |
 12 | f = ECC @() @[] @()
    |              ^^
 }}}

 This is because the order of type variables for `ECC` has changed between
 GHC 8.4.1 and HEAD. In 8.4.1, it's

 {{{
 $ /opt/ghc/8.4.1/bin/ghci Bug.hs -XTypeApplications -fprint-explicit-
 foralls
 GHCi, version 8.4.0.20180209: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )
 Ok, one module loaded.
 λ> :type +v ECC
 ECC
   :: forall (ctx :: Constraint) (f :: * -> *) a.
      ctx =>
      f a -> ECC ctx f a
 }}}

 In GHC HEAD, however, it's:

 {{{
 $ ~/Software/ghc2/inplace/bin/ghc-stage2 --interactive Bug.hs
 -XTypeApplications -fprint-explicit-foralls
 GHCi, version 8.5.20180213: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )
 Ok, one module loaded.
 λ> :type +v ECC
 ECC
   :: forall (f :: * -> *) a (ctx :: Constraint).
      ctx =>
      f a -> ECC ctx f a
 }}}

 This regression was introduced in fa29df02a1b0b926afb2525a258172dcbf0ea460
 (Refactor ConDecl: Trac #14529).

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14808>
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] #14808: GHC HEAD regression: GADT constructors no longer quantify tyvars in topological order

GHC - devs mailing list
#14808: GHC HEAD regression: GADT constructors no longer quantify tyvars in
topological order
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  patch
        Priority:  highest           |            Milestone:  8.6.1
       Component:  Compiler (Type    |              Version:  8.5
  checker)                           |
      Resolution:                    |             Keywords:  GADTs
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #14529, #14796    |  Differential Rev(s):  Phab:D4413
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by RyanGlScott):

 * status:  new => patch
 * differential:   => Phab:D4413


--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14808#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] #14808: GHC HEAD regression: GADT constructors no longer quantify tyvars in topological order

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14808: GHC HEAD regression: GADT constructors no longer quantify tyvars in
topological order
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  patch
        Priority:  highest           |            Milestone:  8.6.1
       Component:  Compiler (Type    |              Version:  8.5
  checker)                           |
      Resolution:                    |             Keywords:  GADTs
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #14529, #14796    |  Differential Rev(s):  Phab:D4413
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by Ben Gamari <ben@…>):

 In [changeset:"043466b9aac403553e2aaf8054c064016f963f80/ghc"
 043466b9/ghc]:
 {{{
 #!CommitTicketReference repository="ghc"
 revision="043466b9aac403553e2aaf8054c064016f963f80"
 Rename the types in a GADT constructor in toposorted order

 Previously, we were extracting the free variables from a
 GADT constructor in an incorrect order, which caused the type
 variables for the constructor's type signature to end up in
 non-toposorted order. Thankfully, rearranging the order of types
 during renaming makes swift work of this bug.

 This fixes a regression introduced in commit
 fa29df02a1b0b926afb2525a258172dcbf0ea460.
 For whatever reason, that commit also commented out a
 significant portion of the `T13123` test. This code appears
 to work, so I've opted to uncomment it.

 Test Plan: make test TEST=T14808

 Reviewers: simonpj, bgamari

 Reviewed By: bgamari

 Subscribers: rwbarton, thomie, carter

 GHC Trac Issues: #14808

 Differential Revision: https://phabricator.haskell.org/D4413
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14808#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] #14808: GHC HEAD regression: GADT constructors no longer quantify tyvars in topological order

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14808: GHC HEAD regression: GADT constructors no longer quantify tyvars in
topological order
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  closed
        Priority:  highest           |            Milestone:  8.6.1
       Component:  Compiler (Type    |              Version:  8.5
  checker)                           |
      Resolution:  fixed             |             Keywords:  GADTs
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #14529, #14796    |  Differential Rev(s):  Phab:D4413
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by bgamari):

 * status:  patch => closed
 * resolution:   => fixed


--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14808#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] #14808: GHC HEAD regression: GADT constructors no longer quantify tyvars in topological order

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14808: GHC HEAD regression: GADT constructors no longer quantify tyvars in
topological order
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  highest           |            Milestone:  8.6.1
       Component:  Compiler (Type    |              Version:  8.5
  checker)                           |
      Resolution:                    |             Keywords:  GADTs
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #14529, #14796    |  Differential Rev(s):  Phab:D4413
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by simonpj):

 * status:  closed => new
 * resolution:  fixed =>


Comment:

 Richard, I'm disturbed by this.

 * The [http://downloads.haskell.org/~ghc/master/users-
 guide/glasgow_exts.html#visible-type-application spec for visible type
 application] says that we quantify implicit variables in left-to-right
 order; but that we perturb that order to respect dependency, speaking of a
 "table topological sort".

 * But I can't find a single comment or Note in the source code to point
 out where these things are implemented.

 * In the case in point for #14808, we have
 [https://phabricator.haskell.org/D4413 this fix] in `RnSource`.  Although
 the comment doesn't say ''why'' the order is important, I infer (from
 detective work) that:
   * `extractHsTysRdrTyVarsDups` guarantees to return variables in left-to-
 right order
   * The `hsq_implicit` field of `LHsQTyVars` is an ''ordered'' list,
 specifically in left to right order.  Can it contain duplicates?  I think
 not, but again that is not duplicated.
   * There is a `toposortTyVars` in `TcImplicitTKBndrsX` which does the
 perturbing to respect dependency.  But again there is zero documentation
 that it must be a stable topo-sort, or why.

 It should not take detective work to infer this info. If my suppositions
 are correct, could you
 * Document the key invariants on data types
 * Add a Note to explain the moving parts and
 * Refer to it from appropriate places.
 E.g. I bet the same ordering constraints apply to `hsib_ars` field of
 `HsImplicitBndrs`?

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14808#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] #14808: GHC HEAD regression: GADT constructors no longer quantify tyvars in topological order

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14808: GHC HEAD regression: GADT constructors no longer quantify tyvars in
topological order
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  highest           |            Milestone:  8.6.1
       Component:  Compiler (Type    |              Version:  8.5
  checker)                           |
      Resolution:                    |             Keywords:  GADTs
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #14529, #14796    |  Differential Rev(s):  Phab:D4413
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by simonpj):

 * owner:  (none) => goldfire


--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14808#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] #14808: GHC HEAD regression: GADT constructors no longer quantify tyvars in topological order

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14808: GHC HEAD regression: GADT constructors no longer quantify tyvars in
topological order
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  highest           |            Milestone:  8.6.1
       Component:  Compiler (Type    |              Version:  8.5
  checker)                           |
      Resolution:                    |             Keywords:  GADTs
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #14529, #14796    |  Differential Rev(s):  Phab:D4413
       Wiki Page:                    |
-------------------------------------+-------------------------------------

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

 In [changeset:"e7653bc3c4f57d2282e982b9eb83bd1fcbae6e30/ghc" e7653bc/ghc]:
 {{{
 #!CommitTicketReference repository="ghc"
 revision="e7653bc3c4f57d2282e982b9eb83bd1fcbae6e30"
 Wombling around in Trac #14808

 Comment:4 in Trac #14808 explains why I'm unhappy with the current
 state of affairs -- at least the lack of documentation.

 This smallpatch does nothing major:

 * adds comments
 * uses existing type synonyms more (notably FreeKiTyVarsWithDups)
 * adds another test case to T14808
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14808#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] #14808: GHC HEAD regression: GADT constructors no longer quantify tyvars in topological order

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14808: GHC HEAD regression: GADT constructors no longer quantify tyvars in
topological order
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  highest           |            Milestone:  8.6.1
       Component:  Compiler (Type    |              Version:  8.5
  checker)                           |
      Resolution:                    |             Keywords:  GADTs
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #14529, #14796    |  Differential Rev(s):  Phab:D4413
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by Richard Eisenberg <rae@…>):

 In [changeset:"7f4dd888f12ec9a24cc2d7f60f214706bd33a1ab/ghc" 7f4dd88/ghc]:
 {{{
 #!CommitTicketReference repository="ghc"
 revision="7f4dd888f12ec9a24cc2d7f60f214706bd33a1ab"
 Note [Ordering of implicit variables]

 This addresses #14808

 [ci skip]
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14808#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] #14808: GHC HEAD regression: GADT constructors no longer quantify tyvars in topological order

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14808: GHC HEAD regression: GADT constructors no longer quantify tyvars in
topological order
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  goldfire
            Type:  bug               |               Status:  merge
        Priority:  highest           |            Milestone:  8.6.1
       Component:  Compiler (Type    |              Version:  8.5
  checker)                           |
      Resolution:                    |             Keywords:  GADTs
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #14529, #14796    |  Differential Rev(s):  Phab:D4413
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by goldfire):

 * status:  new => merge


Comment:

 The remaining piece was to improve documentation, which the last commit
 does. It's worth merging this last piece, as it clarifies the manual.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14808#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] #14808: GHC HEAD regression: GADT constructors no longer quantify tyvars in topological order

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14808: GHC HEAD regression: GADT constructors no longer quantify tyvars in
topological order
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  goldfire
            Type:  bug               |               Status:  merge
        Priority:  highest           |            Milestone:  8.6.1
       Component:  Compiler (Type    |              Version:  8.5
  checker)                           |
      Resolution:                    |             Keywords:  GADTs
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #14529, #14796    |  Differential Rev(s):  Phab:D4413
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Thanks Richard!  That's an improvement.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14808#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] #14808: GHC HEAD regression: GADT constructors no longer quantify tyvars in topological order

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14808: GHC HEAD regression: GADT constructors no longer quantify tyvars in
topological order
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  goldfire
            Type:  bug               |               Status:  closed
        Priority:  highest           |            Milestone:  8.6.1
       Component:  Compiler (Type    |              Version:  8.5
  checker)                           |
      Resolution:  fixed             |             Keywords:  GADTs
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #14529, #14796    |  Differential Rev(s):  Phab:D4413
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by bgamari):

 * status:  merge => closed
 * resolution:   => fixed


Comment:

 comment:2 merged in 043466b9aac403553e2aaf8054c064016f963f80.

 comment:6 merged in e7653bc3c4f57d2282e982b9eb83bd1fcbae6e30.

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