[GHC] #11620: RFC: Type-class type signatures (:: Constraint)

[GHC]

#11620: RFC: Type-class type signatures (:: Constraint)
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.1
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 I actually ran into this problem in a different context, where the problem
 was not just cosmetic.

 Short version: we should devise a syntax where a user can give a full kind
 signature for a class while binding type variables appropriately. I'm not
 sure what this syntax would be.

 Long version: I had this type:

 {{{#!hs
 data TypeRep (a :: k) where ...
 }}}

 I needed an existential wrapper around this type, something like

 {{{#!hs
 data TypeRepX1 where
   TypeRepX1 :: forall k (a :: k). TypeRep a -> TypeRepX1
 }}}

 But that turned out not to work for me, because it imposes no constraint
 at all on `k` or `a`. So I wanted a version of `TypeRepX` that is
 parameterized by a constraint that will be applied to `a`. If the
 existential `a` is still to be kind-polymorphic, then we have to make the
 constraint kind-polymorphic, too:

 {{{#!hs
 data TypeRepX :: (forall k. k -> Constraint) -> Type where
   TypeRepX :: forall (c :: forall k1. k1 -> Constraint) k (a :: k).
               c a => TypeRep a -> TypeRepX c
 }}}

 (Sadly, I need to put the kind on `c` explicitly, because GHC won't infer
 kinds with `forall`s, lest things become impredicative. But it's not so
 bad, really, to put the signature on.)

 This actually all works quite well, to my great delight when I first tried
 it.

 Then, I wanted to use the constraint `((~~) Bool)`. That is, I wanted to
 insist that the type `a` is in fact `Bool`. I used heterogeneous equality
 so that it would all be kind-polymorphic. However, note that

 {{{#!hs
 (~~) :: forall k1 k2. k1 -> k2 -> Constraint`
 }}}

 and thus that

 {{{#!hs
 (~~) Bool :: k2 -> Constraint
 }}}

 for some `k2`. That is, the original `forall` is too far to the left. As
 you will see in the "Practical type inference" paper, the kind of `(~~)`
 is too specific; it should really be `forall k1. k1 -> forall k2. k2 ->
 Constraint`. But we have no way of requesting such a kind without being
 able to specify the full kind signature of a class. (In the case of
 `(~~)`, GHC could just do this by fiat. But it would be unsporting for me
 to do this for `(~~)` without letting you do it for your constraints.)

 Bottom line: it would increase the expressiveness of Haskell to be able to
 specify a full kind.

 But what about syntax?? I'm a bit stuck there.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11620#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler