#15782: Visible type/kind applications in declaration of data/type constructors -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #12045 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by Iceland_jack: Old description:

Two "logical" placements of visible type / kind application, in the declaration of data and type constructors (from [https://phabricator.haskell.org/D5229#144558 Phab comment]).

{{{#!hs data Proxy :: forall k. k -> Type where MkProxy :: Proxy @k (a :: k)

-- can be written

data Proxy @k :: k -> Type where MkProxy @k :: Proxy @k (a :: k) }}}

&

{{{#!hs data Fin :: N -> Type where FinO :: Fin (S n) FinS :: Fin n -> Fin (S n)

-- can be written

data Fin :: N -> Type where FinO @n :: Fin (S n) FinS @n :: Fin n -> Fin (S n) }}}

New description: I'm making this ticket to keep track of this, I don't know if it's a good idea. Allow visible type/kind applications when declaring data/type constructors on the LHS of `::` (from [https://phabricator.haskell.org/D5229#144558 Phab comment]). {{{#!hs data Proxy :: forall k. k -> Type where MkProxy :: Proxy @k (a :: k) -- can be written data Proxy @k :: k -> Type where MkProxy @k :: Proxy @k (a :: k) }}} & {{{#!hs data Fin :: N -> Type where FinO :: Fin (S n) FinS :: Fin n -> Fin (S n) -- can be written data Fin :: N -> Type where FinO @n :: Fin (S n) FinS @n :: Fin n -> Fin (S n) }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15782#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15782: Visible type/kind applications in declaration of data/type constructors -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #12045 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Consider also, declarations of type classes and synonyms {{{#!hs class (f a, g a) => (&) @k f g a instance (f a, g a) => (&) @k f g a -- on the VKA branch, only this works }}} {{{#!hs type Cat ob = ob -> ob -> Type class Category (ob :: Type) where type Hom @ob :: Cat ob id :: Hom @ob a a (.) :: Hom @ob b c -> Hom @ob a b -> Hom @ob a c }}} Now for an extreme example, but what about this {{{#!hs class Category @ob where type Hom @ob :: Cat ob id :: Hom @ob a a }}} where the type of `id` is `id :: forall (a :: ob). Category @ob => Hom a a`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15782#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler