#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
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
