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
<details><summary>Trac metadata</summary>
| 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 | |
</details>
<!-- {"blocked_by":[],"summary":"Existential data constructors should not be promoted","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.6.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"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:\r\n{{{\r\n {-# LANGUAGE DataKinds #-}\r\n {-# LANGUAGE ExistentialQuantification #-}\r\n {-# LANGUAGE GADTs #-}\r\n {-# LANGUAGE KindSignatures #-}\r\n\r\n module Test where\r\n\r\n data K = forall a. T a -- promotion gives 'T :: * -> K \r\n\r\n data G :: K -> * where\r\n D :: G (T []) -- kind error!\r\n}}}\r\nI would expect the type checker to reject it, but GHC (version 7.6.1) compiles it happily","type_of_failure":"OtherFailure","blocking":[]} -->
issue