#6049: Kind variable generalization error in GADTs ---------------------------------------+------------------------------------ Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Component: Compiler (Type checker) Version: 7.5 | Keywords: PolyKinds Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: GHC rejects valid program | Testcase: Blockedby: | Blocking: Related: | ---------------------------------------+------------------------------------ The following code fails to compile with 7.5.20120426:
{{{ {-# LANGUAGE DataKinds, KindSignatures, PolyKinds, GADTs, ExistentialQuantification #-} data SMaybe :: (k -> *) -> Maybe k -> * where SNothing :: forall (s :: k -> *). SMaybe s Nothing SJust :: forall (s :: k -> *) (a :: k). s a -> SMaybe s (Just a) }}} The reported error is {{{ Kind mis-match The first argument of `SMaybe' should have kind `k1 -> *', but `s' has kind `k -> *' In the type `SMaybe s (Just a)' In the definition of data constructor `SJust' In the data declaration for `SMaybe' }}} The code compiles fine without the explicit {{{forall}}} annotations, but other, more involved code I'm working on (involving {{{Proxy}}}) requires the annotations, so simply omitting the explicit kind annotations is not always a viable workaround. -- Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6049> 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