Existential data constructors should not be promoted

Stefan Holdermans reports: 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

Trac metadata

Trac field	Value
Version	7.6.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture