GHC: Ticket #7873: A poly-kinded newtype existential crisis
http://ghc.haskell.org/trac/ghc/ticket/7873
<p>
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.
</p>
<pre class="wiki">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)
</pre><pre class="wiki">fast/Data/Reflection.hs:92:21:
A newtype constructor cannot have an existential context,
but `Magic' does
In the definition of data constructor `Magic'
</pre><p>
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?
</p>
en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/7873
Trac 1.2.2.dev0ekmettTue, 30 Apr 2013 19:02:52 GMTcc set
http://ghc.haskell.org/trac/ghc/ticket/7873#comment:1
http://ghc.haskell.org/trac/ghc/ticket/7873#comment:1
<ul>
<li><strong>cc</strong>
<em>ekmett@…</em> added
</li>
</ul>
TicketekmettTue, 30 Apr 2013 19:09:52 GMT
http://ghc.haskell.org/trac/ghc/ticket/7873#comment:2
http://ghc.haskell.org/trac/ghc/ticket/7873#comment:2
<p>
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.
</p>
TicketkosmikusTue, 30 Apr 2013 19:11:48 GMT
http://ghc.haskell.org/trac/ghc/ticket/7873#comment:3
http://ghc.haskell.org/trac/ghc/ticket/7873#comment:3
<p>
It works if you restrict <code>s</code> in <code>Magic</code> to be of a particular kind, for example <code>*</code>. I think it's indeed existential if not constrained.
</p>
TicketekmettTue, 30 Apr 2013 19:12:42 GMT
http://ghc.haskell.org/trac/ghc/ticket/7873#comment:4
http://ghc.haskell.org/trac/ghc/ticket/7873#comment:4
<p>
A version without classes or complicated desugarings:
</p>
<pre class="wiki">newtype Magic = Magic (forall p a. p a -> Int)
</pre><p>
also exhibits the issue.
</p>
TicketkosmikusTue, 30 Apr 2013 19:15:04 GMT
http://ghc.haskell.org/trac/ghc/ticket/7873#comment:5
http://ghc.haskell.org/trac/ghc/ticket/7873#comment:5
<p>
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.
</p>
TicketgoldfireWed, 01 May 2013 01:32:39 GMT
http://ghc.haskell.org/trac/ghc/ticket/7873#comment:6
http://ghc.haskell.org/trac/ghc/ticket/7873#comment:6
<p>
I agree with kosmikus. With <code>PolyKinds</code>, <code>Magic</code> is indeed existential. Here is the version with explicit kinds (which isn't valid Haskell):
</p>
<pre class="wiki">newtype Magic = forall (k :: BOX). Magic (forall (p :: k -> *) (a :: k). p a -> Int)
</pre><p>
However, there is a happy workaround. GHC scopes the kind variable <code>k</code> appropriately when the annotation is explicit. The following compiles:
</p>
<pre class="wiki">newtype Magic = Magic (forall (p :: k -> *) (a :: k). p a -> Int)
</pre><p>
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.)
</p>
TicketsimonpjThu, 02 May 2013 10:36:34 GMTdifficulty set
http://ghc.haskell.org/trac/ghc/ticket/7873#comment:7
http://ghc.haskell.org/trac/ghc/ticket/7873#comment:7
<ul>
<li><strong>difficulty</strong>
set to <em>Unknown</em>
</li>
</ul>
<p>
Richard (goldfire) has it right.
</p>
<p>
GHC puts the "forall k" at the outer level, if not told otherwise. Hence indeed the original <code>Magic</code> gets the type
</p>
<pre class="wiki">newtype Magic = Magic (forall p a. p a -> Int)
-- Magic :: forall (k:BOX). (forall (p :: k -> *) (a :: k). p a -> Int)
-- -> Magic
</pre><p>
How can we "tell it otherwise". GHC has no notation for explicit kind quantification at the moment. We knew that we wanted <em>implicit</em> kind quantification, thus:
</p>
<pre class="wiki">data T (f :: k -> *) (a :: k) = MkT (f a )
</pre><p>
and that's the <em>only</em> 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
</p>
<pre class="wiki">newtype Magic = Magic (forall p (a :: k). p a -> Int)
-- Magic :: (forall (k:BOX) (p:k->*) (a:k). p a -> Int)
-- -> Magic
</pre><p>
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.
</p>
<p>
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.
</p>
TicketsimonpjFri, 03 May 2013 07:00:12 GMTstatus changed; testcase, resolution set
http://ghc.haskell.org/trac/ghc/ticket/7873#comment:8
http://ghc.haskell.org/trac/ghc/ticket/7873#comment:8
<ul>
<li><strong>testcase</strong>
set to <em>ghci/scripts/T7873</em>
</li>
<li><strong>status</strong>
changed from <em>new</em> to <em>closed</em>
</li>
<li><strong>resolution</strong>
set to <em>fixed</em>
</li>
</ul>
<p>
This commit fixes the bugs I mention above
</p>
<pre class="wiki">commit 7a7530a9d4f7cb630ab8d69dd12324e1bf61faed
Author: Simon Peyton Jones <simonpj@microsoft.com>
Date: Thu May 2 17:28:20 2013 +0100
Fix kind quantification (again)
We simply weren't quantifying kind variables at the points we
were claiming. In paritcular, in
forall (a:k). blah
we quantify the 'k' around the 'forall a', provided k isn't
already in scope
compiler/hsSyn/HsTypes.lhs | 6 ++---
compiler/rename/RnTypes.lhs | 12 ++++------
compiler/typecheck/TcHsType.lhs | 37 +++++++++++++++++------------
compiler/typecheck/TcInteract.lhs | 50 +++++++++++++++++++++++++++------------
compiler/typecheck/TcMType.lhs | 11 ++++++++-
compiler/typecheck/TcSMonad.lhs | 16 +++++++------
6 files changed, 84 insertions(+), 48 deletions(-)
</pre><p>
while this improves the docs
</p>
<pre class="wiki">commit 3722f034d0907fcd20179ce4dd91e53c51d4e87f
Author: Simon Peyton Jones <simonpj@microsoft.com>
Date: Thu May 2 17:06:13 2013 +0100
Improve documentation of kind polymorphism
</pre>
TicketsimonpjFri, 03 May 2013 09:10:06 GMT
http://ghc.haskell.org/trac/ghc/ticket/7873#comment:9
http://ghc.haskell.org/trac/ghc/ticket/7873#comment:9
<p>
Oh, I also improve the rather cryptic "existential" error message
</p>
<pre class="wiki">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’
</pre><p>
with this commit
</p>
<pre class="wiki">commit bee30a6586ae157d8a5569f17f0e4cd14ab71653
Author: Simon Peyton Jones <simonpj@microsoft.com>
Date: Fri May 3 10:06:19 2013 +0100
Improve error message for existential newtypes
compiler/typecheck/TcTyClsDecls.lhs | 24 ++++++++++++------------
1 file changed, 12 insertions(+), 12 deletions(-)
</pre>
Ticket