#10114: Kind mismatches with AnyK in rank-2 types -------------------------------------+------------------------------------- Reporter: cam | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by simonpj): Some notes for myself (work in progress). At the moment, for type `T` above we get {{{ -- Without PolyKinds type T = forall (f :: AnyK -> *) (a :: AnyK). f a -- With PolyKinds type T k = forall (f :: AnyK -> k) (a :: AnyK). f a }}} Trouble is that we are not generalising over the kind of `a`. I think we want: {{{ -- Without PolyKinds type T = forall (f :: * -> *) (a :: *). f a -- With PolyKinds type T k1 k2 = forall (f :: k1 -> k2) (a :: k1). f a }}} But note the strange kind of `T` in `PolyKinds` case: `T :: forall k1 k2. k2`. I'm pretty sure we do NOT want to kind-generalise "inside", thus: {{{ type T = forall k1 k2 (f :: k1->k2) (a::k1). f a }}} Reasons: * see `Note [Kind generalisation]` in `TcHsType` * what kind would `T` have? `T :: k2` ??? * more operationally, kind foralls must be implicitly instantiated, during kind inference using only `T`'s kind -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10114#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler