#12045: Visible kind application -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Iceland_jack Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: | TypeApplications TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): ​Phab:D2216 Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): [research.microsoft.com/en-us/um/...f/promotion-tldi12-sub.pdf Giving Haskell a Promotion]: {{{#!hs data Mu :: forall k. ((k -> Type) -> (k -> Type)) -> (k -> Type) where Roll :: f (Mu f) a -> Mu f a data VecF :: Type -> (Nat -> Type) -> (Nat -> Type) where VFNil :: VecF a f Zero VFCons :: a -> f n -> VecF a f (Succ n) }}} Applying `type Vec a n = Mu (VecF a) n` instantiates `k` to `Nat` in `Mu`, so this should work: {{{
:kind Mu Mu :: ((k -> Type) -> k -> Type) -> k -> Type
:kind Mu @Nat Mu @Nat :: ((Nat -> Type) -> Nat -> Type) -> Nat -> Type
:kind forall a. Mu @Nat (VecF a) forall a. Mu @Nat (VecF a) :: Nat -> Type }}}
-- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12045#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler