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

[Simon Peyton-Jones]

Quite right -- a bug. Thank you.  I'll add it to the regression suite

Simon

|  -----Original Message-----
|  From: haskell-cafe-bounces at haskell.org [mailto:haskell-cafe-
|  bounces at 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 at haskell.org
|  http://www.haskell.org/mailman/listinfo/haskell-cafe