id	summary	reporter	owner	description	type	status	priority	milestone	component	version	resolution	keywords	cc	os	architecture	failure	difficulty	testcase	blockedby	blocking	related
6049	Kind variable generalization error in GADTs	goldfire		"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."	bug	closed	normal		Compiler (Type checker)	7.5	fixed	PolyKinds	dimitris@… dreixel sweirich@…	Unknown/Multiple	Unknown/Multiple	GHC rejects valid program	Unknown	polykinds/T6049