Quite right -- a bug. Thank you. I'll add it to the regression suite Simon | -----Original Message----- | From: haskell-cafe-bounces@haskell.org [mailto:haskell-cafe- | bounces@haskell.org] On Behalf Of Stefan Holdermans | Sent: 17 October 2012 21:45 | To: Haskell Cafe | Cc: José Pedro Magalhães | Subject: [Haskell-cafe] Erroneous interaction between DataKinds and | ExistentialQuantification? | | I am almost sure this is a known issue, but I noticed some erroneous (?) | interaction between datatype promotion and existential quantification. Consider | the following program: | | {-# LANGUAGE DataKinds #-} | {-# LANGUAGE ExistentialQuantification #-} | {-# LANGUAGE GADTs #-} | {-# LANGUAGE KindSignatures #-} | | module Test where | | data K = forall a. T a -- promotion gives 'T :: * -> K | | data G :: K -> * where | D :: G (T []) -- kind error! | | I would expect the type checker to reject it, but GHC (version 7.6.1) compiles it | happily. Is this indeed a (known) bug? | | On a related note: is there a way to promote a type that involves an existential | type variable of a kind other than *? | | Thanks, | | Stefan | _______________________________________________ | Haskell-Cafe mailing list | Haskell-Cafe@haskell.org | http://www.haskell.org/mailman/listinfo/haskell-cafe