#10995: Existentials in newtypes -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #10715 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Ahh... There is clearly a bug here. But it's a bug hiding a design question. If you see this: {{{ data T = MkT (forall a f. f a -> Int) }}} which of these two would you expect to get? {{{ data T1 @k = MkT (forall (a::k) (f::k->*). f a -> Int ) data T2 = MkT (forall k. forall (a::k) (f::k->*). f a -> Int) }}} That is, where should the kind be quantified? A similar choice arises for ordinary function type signatures; see this comment in `TcHsType`: {{{ Note [Kind generalisation] ~~~~~~~~~~~~~~~~~~~~~~~~~~ We do kind generalisation only at the outer level of a type signature. For example, consider T :: forall k. k -> * f :: (forall a. T a -> Int) -> Int When kind-checking f's type signature we generalise the kind at the outermost level, thus: f1 :: forall k. (forall (a:k). T k a -> Int) -> Int -- YES! and *not* at the inner forall: f2 :: (forall k. forall (a:k). T k a -> Int) -> Int -- NO! Reason: same as for HM inference on value level declarations, we want to infer the most general type. The f2 type signature would be *less applicable* than f1, because it requires a more polymorphic argument. }}} On this basis, to be consistent, we should go for `T1` not `T2`. (Which raises the question of how you could get `T2` or `f2` if you wanted them.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10995#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler