[GHC] #15782: Visible type/kind applications in declaration of data/type constructors
GHC
ghc-devs at haskell.org
Fri Oct 19 12:38:20 UTC 2018
#15782: Visible type/kind applications in declaration of data/type constructors
-------------------------------------+-------------------------------------
Reporter: Iceland_jack | Owner: (none)
Type: feature | Status: new
request |
Priority: normal | Milestone:
Component: Compiler | Version: 8.6.1
Keywords: | Operating System: Unknown/Multiple
TypeApplications |
Architecture: | Type of failure: None/Unknown
Unknown/Multiple |
Test Case: | Blocked By:
Blocking: | Related Tickets: #12045
Differential Rev(s): | Wiki Page:
-------------------------------------+-------------------------------------
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)
}}}
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15782>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
More information about the ghc-tickets
mailing list