GHC: Ticket #7503: Bug with PolyKinds, type synonyms & GADTs
http://ghc.haskell.org/trac/ghc/ticket/7503
<p>
GHC incorrectly rejects this program:
</p>
<pre class="wiki">{-# LANGUAGE ExistentialQuantification, DataKinds, PolyKinds, KindSignatures, GADTs #-}
module TestConstraintKinds where
import GHC.Exts hiding (Any)
data WrappedType = forall a. WrapType a
data A :: WrappedType -> * where
MkA :: forall (a :: *). AW a -> A (WrapType a)
type AW (a :: k) = A (WrapType a)
type AW' (a :: k) = A (WrapType a)
class C (a :: k) where
aw :: AW a -- workaround: AW'
instance C [] where
aw = aw
</pre><p>
GHC accepts the program when AW is replaced with AW' on that line.
</p>
en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/7503
Trac 1.0.1simonpjThu, 20 Dec 2012 13:42:55 GMTdifficulty set
http://ghc.haskell.org/trac/ghc/ticket/7503#comment:1
http://ghc.haskell.org/trac/ghc/ticket/7503#comment:1
<ul>
<li><strong>difficulty</strong>
set to <em>Unknown</em>
</li>
</ul>
<p>
Hmm. As stated, it fails both with <tt>AW</tt> and <tt>AW'</tt> in the commented line. But this simpler one fails:
</p>
<pre class="wiki">data Wrap a -- Wrap :: forall k. k -> *
data A a = MkA a (AW a)
type AW a = A (Wrap a)
type AW2 a = A (Wrap a)
class C (a :: k) where
aw :: AW a -- workaround: AW2
</pre><p>
With <tt>AW</tt> in the last line we get
</p>
<pre class="wiki">T7503.hs:15:14:
The first argument of `AW' should have kind `*',
but `a' has kind `k1'
In the type `AW a'
In the class declaration for `C'
</pre><p>
Replacing with the identical (!) <tt>AW2</tt> makes it go through. Here is what is happening:
</p>
<ul><li>Type synonym <tt>AW</tt> and data type <tt>A</tt> are mutually recursive.
</li><li>So they are kind-checked together, with <tt>AW</tt> being monomorphic.
</li><li><tt>AW</tt> is applied to <tt>a::*</tt> in the data type declaration of <tt>A</tt>, so <tt>AW</tt> ends up with kind <tt>*->*</tt>.
</li><li>But that is insufficiently polymorphic for its use in the class declaration.
</li><li>On the other hand <tt>AW2</tt> is not mutually recursive with <tt>A</tt>, so it is kind-checked after <tt>A</tt> is done, and gets the polymorphic kind <tt>AW2 :: forall k. k -> *</tt>.
</li></ul><p>
Very similar things happen in the world of terms. We solve them by <a href="http://www.haskell.org/ghc/docs/latest/html/users_guide/other-type-extensions.html#typing-binds">breaking the mutual recursion at a type signature</a>, and in principle we could do the same here. After all, <tt>A</tt> is given a full kind signature.
</p>
<p>
Still, it's not entirely trivial to implement. And we don't have a general mechanism for giving kind signatures; for example, how would you give a kind signature for a type synonym?
</p>
<p>
Worth thinking about. But perhpas not urgent. Yell if it is hurting you.
</p>
<p>
Simon
</p>
TicketiglooFri, 12 Apr 2013 21:24:20 GMTowner, milestone set
http://ghc.haskell.org/trac/ghc/ticket/7503#comment:2
http://ghc.haskell.org/trac/ghc/ticket/7503#comment:2
<ul>
<li><strong>owner</strong>
set to <em>simonpj</em>
</li>
<li><strong>milestone</strong>
set to <em>7.8.1</em>
</li>
</ul>
Ticket