#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: | -------------------------------------+------------------------------------- Changes (by thomie): * cc: goldfire (added) * component: Compiler => Compiler (Type checker) * related: => #10715 Comment: HEAD also compiles your first example without errors. Your second example results in the error messages below. The `pprTrace "RAE1"` is from 2f9809efdbc11fee445dbe3d5c555433ec3c5e6a (#10715). {{{ $ ghc-7.11.20151019 Test.hs [1 of 1] Compiling Test ( Test.hs, Test.o ) RAE1 [W] cobox_apw :: k0_apq[tau:3] ~ k_apn[sk] (CNonCanonical) k0_apq[tau:3] k_apn[sk] False Test.hs:10:22: error: Couldn't match kind ‘k0’ with ‘k’ ‘k0’ is untouchable inside the constraints: Ctx2 c a b bound by the type of the constructor ‘P1’: Ctx2 c a b => Proxy b -> Int at Test.hs:10:22 ‘k’ is a rigid type variable bound by the type of the constructor ‘P1’: (forall (b :: k). Ctx2 c a b => Proxy b -> Int) -> Proxy1 c a at Test.hs:10:22 Expected type: Proxy b -> Int Actual type: Proxy b -> Int In the ambiguity check for the type of the constructor ‘P1’: P1 :: forall c a (k :: BOX). (forall (b :: k). Ctx2 c a b => Proxy b -> Int) -> Proxy1 c a To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the definition of data constructor ‘P1’ In the newtype declaration for ‘Proxy1’ Test.hs:10:22: error: Could not deduce: Ctx2 c a b from the context: Ctx2 c a b bound by the type of the constructor ‘P1’: Ctx2 c a b => Proxy b -> Int at Test.hs:10:22 In the ambiguity check for the type of the constructor ‘P1’: P1 :: forall c a (k :: BOX). (forall (b :: k). Ctx2 c a b => Proxy b -> Int) -> Proxy1 c a To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the definition of data constructor ‘P1’ In the newtype declaration for ‘Proxy1’ Test.hs:10:22: error: A newtype constructor cannot have existential type variables P1 :: forall c a (k :: BOX). (forall (b :: k). Ctx2 c a b => Proxy b -> Int) -> Proxy1 c a In the definition of data constructor ‘P1’ In the newtype declaration for ‘Proxy1’ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10995#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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