#6049: Kind variable generalization error in GADTs ----------------------------------------+----------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.5 Keywords: PolyKinds | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: GHC rejects valid program Difficulty: Unknown | Testcase: Blockedby: | Blocking: Related: | ----------------------------------------+-----------------------------------
Comment(by simonpj): Actually I think it's harder than I thought to "hack around". Suppose we had {{{ data SMaybe :: (k -> *) -> Maybe k -> * where SNothing :: Int -> (forall kk. forall (ss :: kk -> *). SMaybe ss Nothing) -> SMaybe s a }}} I have used a nested forall, so now really impossible (without lots of hackery) to make this work with a kind-monomorphic `SMaybe`. This can't really happen unless we have explicit kind-foralls, but sooner or later we will. I think the simplest path is to say that for GADT-style syntax you must give the kind of the type constructor in the header; and if you don't you'll get `* -> * -> *`, ie not even higher kinds. This would mean that some existing programs would need a kind signature. {{{ data T a b where MkT :: a b -> T a b }}} would need signatures, thus {{{ data T (a : * -> *) b where MkT :: a b -> T a b or data T :: (* -> *) -> * -> * where MkT :: a b -> T a b or data T :: (k -> *) -> k -> * where MkT :: a b -> T a b }}} But it would enforce good practice (put those kind signatures in! And I suppose that this new behaviour could be enabled by `-XPolyKinds`. -- Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6049#comment:4> 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