[GHC] #7873: A poly-kinded newtype existential crisis
#7873: A poly-kinded newtype existential crisis --------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: bug | Status: new Priority: normal | Component: Compiler Version: 7.6.3 | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: GHC rejects valid program | Blockedby: Blocking: | Related: --------------------------------------+------------------------------------- The following code worked on older GHCs and on other compilers clear back to Hugs, but based on reports I'm getting from a half-dozen users appears to broken on GHC 7.6.1+ and in GHC HEAD. {{{ class Reifies s a | s -> a where reflect :: proxy s -> a data Proxy a = Proxy newtype Magic a r = Magic (forall s. Reifies s a => Proxy s -> r) }}} {{{ fast/Data/Reflection.hs:92:21: A newtype constructor cannot have an existential context, but `Magic' does In the definition of data constructor `Magic' }}} There doesn't appear to be anything existential going on there, but that said, this issue does only occur when PolyKinds are turned on, so perhaps the issue is with the desugaring into PolyKinds? -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7873 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#7873: A poly-kinded newtype existential crisis --------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: bug | Status: new Priority: normal | Component: Compiler Version: 7.6.3 | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: GHC rejects valid program | Blockedby: Blocking: | Related: --------------------------------------+------------------------------------- Changes (by ekmett): * cc: ekmett@… (added) -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7873#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#7873: A poly-kinded newtype existential crisis --------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: bug | Status: new Priority: normal | Component: Compiler Version: 7.6.3 | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: GHC rejects valid program | Blockedby: Blocking: | Related: --------------------------------------+------------------------------------- Comment(by ekmett): It appears that as long as the module that defines Magic doesn't have PolyKinds enabled, everything works, even if Proxy and even Reifies, etc. were compiled with PolyKinds enabled, so I can probably hack around this by doing some creative importing, but this does seem to indicate that turning on PolyKinds makes a lot fewer things valid newtypes. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7873#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#7873: A poly-kinded newtype existential crisis --------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: bug | Status: new Priority: normal | Component: Compiler Version: 7.6.3 | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: GHC rejects valid program | Blockedby: Blocking: | Related: --------------------------------------+------------------------------------- Comment(by kosmikus): It works if you restrict `s` in `Magic` to be of a particular kind, for example `*`. I think it's indeed existential if not constrained. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7873#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#7873: A poly-kinded newtype existential crisis --------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: bug | Status: new Priority: normal | Component: Compiler Version: 7.6.3 | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: GHC rejects valid program | Blockedby: Blocking: | Related: --------------------------------------+------------------------------------- Comment(by ekmett): A version without classes or complicated desugarings: {{{ newtype Magic = Magic (forall p a. p a -> Int) }}} also exhibits the issue. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7873#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#7873: A poly-kinded newtype existential crisis --------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: bug | Status: new Priority: normal | Component: Compiler Version: 7.6.3 | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: GHC rejects valid program | Blockedby: Blocking: | Related: --------------------------------------+------------------------------------- Comment(by kosmikus): Actually, I meant to say "it seems to be treated as existential" if not constrained. I didn't mean to imply that this is a necessity. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7873#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#7873: A poly-kinded newtype existential crisis --------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: bug | Status: new Priority: normal | Component: Compiler Version: 7.6.3 | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: GHC rejects valid program | Blockedby: Blocking: | Related: --------------------------------------+------------------------------------- Comment(by goldfire): I agree with kosmikus. With {{{PolyKinds}}}, {{{Magic}}} is indeed existential. Here is the version with explicit kinds (which isn't valid Haskell): {{{ newtype Magic = forall (k :: BOX). Magic (forall (p :: k -> *) (a :: k). p a -> Int) }}} However, there is a happy workaround. GHC scopes the kind variable {{{k}}} appropriately when the annotation is explicit. The following compiles: {{{ newtype Magic = Magic (forall (p :: k -> *) (a :: k). p a -> Int) }}} This is slightly strange behavior, but I don't see an easy fix short of allowing explicit kind quantification. (Of course, I would love to have explicit kind quantification, but that's a story for another time.) -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7873#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#7873: A poly-kinded newtype existential crisis ---------------------------------+------------------------------------------ Reporter: ekmett | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Keywords: | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: GHC rejects valid program Difficulty: Unknown | Testcase: Blockedby: | Blocking: Related: | ---------------------------------+------------------------------------------ Changes (by simonpj): * difficulty: => Unknown Comment: Richard (goldfire) has it right. GHC puts the "forall k" at the outer level, if not told otherwise. Hence indeed the original `Magic` gets the type {{{ newtype Magic = Magic (forall p a. p a -> Int) -- Magic :: forall (k:BOX). (forall (p :: k -> *) (a :: k). p a -> Int) -- -> Magic }}} How can we "tell it otherwise". GHC has no notation for explicit kind quantification at the moment. We knew that we wanted ''implicit'' kind quantification, thus: {{{ data T (f :: k -> *) (a :: k) = MkT (f a ) }}} and that's the ''only'' kind quantification that's currently supported. The rule is that the kind-forall is wrapped immediately around the type- forall that binds it. Hence Richard's solution {{{ newtype Magic = Magic (forall p (a :: k). p a -> Int) -- Magic :: (forall (k:BOX) (p:k->*) (a:k). p a -> Int) -- -> Magic }}} Mind you, having written all this I find there's a bug in this kind quantification stuff, so that's not what happens right now, I'm afraid. Am fixing. I wish we had a simpler, clearer surface syntax for kind quantification; but the implicit version is so useful that I doubt we'll give it up. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7873#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#7873: A poly-kinded newtype existential crisis
----------------------------------------+-----------------------------------
Reporter: ekmett | Owner:
Type: bug | Status: closed
Priority: normal | Milestone:
Component: Compiler | Version: 7.6.3
Resolution: fixed | Keywords:
Os: Unknown/Multiple | Architecture: Unknown/Multiple
Failure: GHC rejects valid program | Difficulty: Unknown
Testcase: ghci/scripts/T7873 | Blockedby:
Blocking: | Related:
----------------------------------------+-----------------------------------
Changes (by simonpj):
* status: new => closed
* testcase: => ghci/scripts/T7873
* resolution: => fixed
Comment:
This commit fixes the bugs I mention above
{{{
commit 7a7530a9d4f7cb630ab8d69dd12324e1bf61faed
Author: Simon Peyton Jones
#7873: A poly-kinded newtype existential crisis
----------------------------------------+-----------------------------------
Reporter: ekmett | Owner:
Type: bug | Status: closed
Priority: normal | Milestone:
Component: Compiler | Version: 7.6.3
Resolution: fixed | Keywords:
Os: Unknown/Multiple | Architecture: Unknown/Multiple
Failure: GHC rejects valid program | Difficulty: Unknown
Testcase: ghci/scripts/T7873 | Blockedby:
Blocking: | Related:
----------------------------------------+-----------------------------------
Comment(by simonpj):
Oh, I also improve the rather cryptic "existential" error message
{{{
T7863.hs:5:17:
A newtype constructor cannot have existential type variables
Magic :: forall (k :: BOX).
(forall (p :: k -> *) (a :: k). p a -> Int) -> Magic
In the definition of data constructor ‛Magic’
In the newtype declaration for ‛Magic’
}}}
with this commit
{{{
commit bee30a6586ae157d8a5569f17f0e4cd14ab71653
Author: Simon Peyton Jones
participants (1)
-
GHC