#7503: Bug with PolyKinds, type synonyms & GADTs
----------------------------------------+-----------------------------------
Reporter: Ashley Yakeley | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler (Type checker) | Version: 7.6.1
Keywords: | Os: Linux
Architecture: x86_64 (amd64) | Failure: GHC rejects valid
program
Difficulty: Unknown | Testcase:
Blockedby: | Blocking:
Related: |
----------------------------------------+-----------------------------------
Changes (by simonpj):
* difficulty: => Unknown
Comment:
Hmm. As stated, it fails both with `AW` and `AW'` in the commented line.
But this simpler one fails:
{{{
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
}}}
With `AW` in the last line we get
{{{
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'
}}}
Replacing with the identical (!) `AW2` makes it go through. Here is what
is happening:
* Type synonym `AW` and data type `A` are mutually recursive.
* So they are kind-checked together, with `AW` being monomorphic.
* `AW` is applied to `a::*` in the data type declaration of `A`, so `AW`
ends up with kind `*->*`.
* But that is insufficiently polymorphic for its use in the class
declaration.
* On the other hand `AW2` is not mutually recursive with `A`, so it is
kind-checked after `A` is done, and gets the polymorphic kind `AW2 ::
forall k. k -> *`.
Very similar things happen in the world of terms. We solve them by
[http://www.haskell.org/ghc/docs/latest/html/users_guide/other-type-
extensions.html#typing-binds breaking the mutual recursion at a type
signature], and in principle we could do the same here. After all, `A` is
given a full kind signature.
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?
Worth thinking about. But perhpas not urgent. Yell if it is hurting you.
Simon
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7503#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
