#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 goldfire): Replying to [comment:2 simonpj]:
There is clearly a bug here. But it's a bug hiding a design question.
I agree with that statement, but disagree in the particulars. And I think that Note is wrong. Consider this: {{{ foo :: (Proxy a -> ()) -> () foo = undefined bar :: (forall a. Proxy a -> ()) -> () bar = undefined quux :: (forall (a :: k). Proxy a -> ()) -> () quux = undefined }}} With `-fprint-explicit-kinds -fprint-explicit-foralls`: {{{ *Scratch> :t foo foo :: forall (k :: BOX) (a :: k). (Proxy k a -> ()) -> () *Scratch> :t bar bar :: forall (k :: BOX). (forall (a :: k). Proxy k a -> ()) -> () *Scratch> :t quux quux :: (forall (k :: BOX) (a :: k). Proxy k a -> ()) -> () }}} With no explicit quantification, `foo`'s kind and type variables are quantified at the top-level. With `a` explicitly quantified in `bar`, `a` is not top-level, but `a`'s kind `k` is top-level. In `quux`, because `k` is explicit mentioned first in the scope of an inner quantification, it is quantified there, too. I find this design a little strange, but in the absence of explicit kind quantification, I don't see a better option. Any of these possibilities make sense and a programmer might want any of them. (Note, we will have explicit kind quantification in GHC 8.0.) Let's get back to datatypes. There is a third possibility Simon omits, and it's actually the one that GHC uses. When we see {{{ data T = MkT (forall a f. f a -> Int) }}} GHC will infer {{{ data T3 = forall k. MkT (forall a f. f a -> Int) }}} which indeed has an existential kind. The good news is that it's easy to work around this problem: just say {{{ data T = MkT (forall (a :: k) f. f a -> Int) }}} and you'll get `T2`, which has no existential kinds. Note that your first declaration, without polykinds, also has no existential variables. It has higher-rank variables, but not existential ones. As for the "could not deduce" error, I think it might be accurate, but I'm not sure. For example, consider {{{ type family F :: Constraint x1 :: (forall b. F => Proxy b -> Int) -> () x1 = undefined x2 :: (forall b. Proxy b -> Int) -> () x2 = undefined }}} `x2` compiles fine. `x1` does not, with a "could not deduce" error much like the one above. Note that `F` is just some unknown constraint, much like `Ctx2`. My guess is that GHC is more timid about unifying under the scope of an equality constraint in `x1`. In `x2`, where the constraint is obviously not an equality, everything is fine. So, error messages could perhaps be improved (can't they always?) but I don't think GHC is wrong here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10995#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler