#7347: Existential data constructors should not be promoted
---------------------------------+------------------------------------------
Reporter: simonpj | Owner:
Type: bug | Status: merge
Priority: normal | Milestone:
Component: Compiler | Version: 7.6.1
Keywords: | Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: None/Unknown
Difficulty: Unknown | Testcase: polykinds/T7347
Blockedby: | Blocking:
Related: |
---------------------------------+------------------------------------------
Comment(by simonpj):
What if I declare `Ex` like this?
{{{
data KEx :: * where
MkKEx :: forall (a::k). Proxy a -> KEx
}}}
Now the kind variable `k` as well as the type variable `a` is
existentially quantified, and NOW we will have to worry about existential
escape, notwithstanding your comment about "no phase separation". Indeed
I can't give a kind to `UnKEx`:
{{{
type family UnKEx :: KEx -> ???
}}}
So maybe what saves us here is that type families have user-specified kind
signatures, and that in turn means we don't need to check for existential
escape.
So I think I agree with your point, but I don't know how urgent/important
it is, nor how hard it would be to implement. At its easiest it might
mean just removing a restriction, but I'm not certain.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7347#comment:12>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
