[Haskell-cafe] Erroneous interaction between DataKinds and ExistentialQuantification?

[Stefan Holdermans]

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