#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