#7347: Existential data constructors should not be promoted
    Reporter:  simonpj           |       Owner:                  
        Type:  bug               |      Status:  new             
    Priority:  normal            |   Milestone:                  
   Component:  Compiler          |     Version:  7.6.1           
    Keywords:                    |          Os:  Unknown/Multiple
Architecture:  Unknown/Multiple  |     Failure:  None/Unknown    
  Difficulty:  Unknown           |    Testcase:                  
   Blockedby:                    |    Blocking:                  
     Related:                    |  

Comment(by simonpj):

 Well this
 type instance MkEx x = x
 should give an existential escape error, but it doesn't. Instead it
 somehow fixes the kind to *.

 You are arguing for this in general.  If we promote a data constructor,
 such as `Just`, whose type is
  Just :: forall a. a -> Maybe a
 then we get poly-kinded type constructor
  'Just :: forlal k. k -> 'Maybe k
 You are arguing for some different type-promotion rule for existentials.
 Maybe, but I have never thought about that and I don't know what the
 details would be.

 If you want something that isn't kind-polymorphic, you don't need an
 existential at all. Wha you want is something like
 data kind Ex = MkEx *
 a perfectly ordinary non-existential data type with an argument of kind
 `*`.  Now, as Pedro points out in his ICFP paper we don't have a way to
 say that, but that is quite a separate matter; existntials are a total red
 herring.  Maybe we should have
 data Ex = MkEx STAR
 where `STAR` is an uninhabited type whose promotion to the kind level is

Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7347#comment:6>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

Glasgow-haskell-bugs mailing list

Reply via email to