[GHC] #12911: Levity polymorphism check eliminates non-levity-polymorphic data constructor
#12911: Levity polymorphism check eliminates non-levity-polymorphic data constructor -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Keywords: | Operating System: Unknown/Multiple LevityPolymorphism | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- When I say {{{ data X where MkX :: forall (a :: TYPE r). (a -> a) -> X }}} I get {{{ • A representation-polymorphic type is not allowed here: Type: a Kind: TYPE r • In the definition of data constructor ‘MkX’ In the data type declaration for ‘X’ }}} But that's silly, because the type is not levity-polymorphic! -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12911> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12911: Levity polymorphism check eliminates non-levity-polymorphic data constructor -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by josef): I think I hit upon this restriction when trying to implement some of the code from the levity polymorphism paper. The section on levity polymorphic type classes explains how the dictionary from levity polymorphic Num is perfectly safe. {{{ data Num (a :: TYPE r) = MkNum {(+) :: a → a → a, abs :: a → a} }}} But sadly GHC rejects the data type declaration above. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12911#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12911: Levity polymorphism check eliminates non-levity-polymorphic data constructor -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Yes, that's over-restrictive; when Richard gets around to implementing the paper (which is very much on his radar I think) it'll be fixed! -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12911#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12911: Levity polymorphism check eliminates non-levity-polymorphic data constructor -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Ben Gamari <ben@…>): In [changeset:"8906e7b79a585039712034d9e88ca49f3cea6554/ghc" 8906e7b7/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="8906e7b79a585039712034d9e88ca49f3cea6554" Reshuffle levity polymorphism checks. Previously, GHC checked for bad levity polymorphism to the left of all arrows in data constructors. This was wrong, as reported in #12911 (where an example is also shown). The solution is to check each individual argument for bad levity polymorphism. Thus the check has been moved from TcValidity to TcTyClsDecls. A similar situation exists with pattern synonyms, also fixed here. This patch also nabs #12819 while I was in town. Test cases: typecheck/should_compile/T12911, patsyn/should_fail/T12819 Test Plan: ./validate Reviewers: simonpj, austin, bgamari Reviewed By: bgamari Subscribers: thomie Differential Revision: https://phabricator.haskell.org/D2783 GHC Trac Issues: #12819, #12911 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12911#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12911: Levity polymorphism check eliminates non-levity-polymorphic data constructor -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: fixed | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_compile/T12911 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * testcase: => typecheck/should_compile/T12911 * status: new => closed * resolution: => fixed Comment: Thanks for merging, Ben! -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12911#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC