[GHC] #14808: GHC HEAD regression: GADT constructors no longer quantify tyvars in topological order
#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
#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
#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
#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
#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
#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
#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
#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
#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
#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
#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
participants (1)
-
GHC