#8090: MetaKinds - PolyKinds generalization -------------------------------------+------------------------------------ Reporter: wvv | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by wvv): 1) This is a part of lambda-cube. {{{ Agda Haskell Set0 a::* Set1 a::k <<==>> a :: (k :: *) Set2 a :: (k2 :: (k :: *)) ... }}} 2) rankNkinds is essential to work with rank(N-1)kinds: classes and (G)ADTs. We already have a lot of rank2kinds(PolyKinds), so we already need to have rank3kinds. Developers said they did new Typeable in GHC 7.8, but it is impossible to write {{{ data Foo (a::(b::k)->*) deriving Typeable }}} new Typeable = Typeable2kinds; but Foo is a part of Typeable3kinds 3) I think for several years max rank kind = 7 is enough (Bill Gates said "640K ought to be enough for anybody") -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8090#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler