[GHC] #15782: Visible type/kind applications in declaration of data/type constructors

GHC ghc-devs at haskell.org
Sat Oct 20 17:31:46 UTC 2018


#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


More information about the ghc-tickets mailing list