Should (~) be homogeneous or heterogeneous?

[Simon Peyton Jones]

In your example, why do you get KP Any?  Why don't you get

class forall k1 k2 kproxy).
     (kproxy :: KProxy k1 ~ 'KP :: KProxy k2) => C kproxy where ...

That may be over-polymorphic, but it'll work ok won't it?

More generally, why does (2) lead to "trouble"?

Simon

|  -----Original Message-----
|  From: ghc-devs [mailto:ghc-devs-bounces at haskell.org] On Behalf Of
|  Richard Eisenberg
|  Sent: 22 November 2015 19:00
|  To: ghc-devs Devs <ghc-devs at haskell.org>
|  Subject: Should (~) be homogeneous or heterogeneous?
|  
|  Hi devs,
|  
|  I'm desperately working toward getting kind equalities in before the
|  feature freeze. It's coming along nicely. But I have a user-facing
|  issue to work out.
|  
|  * Should (~), as written in user code, require the kinds of its
|  arguments to be equal?
|  
|  Another way of asking the same question is: Should the kind of (~) be
|  1. forall k. k -> k -> Constraint    (HEAD)
|  2. forall k1 k2. k1 -> k2 -> Constraint   (my branch, at the moment)
|  
|  Choice #2 is strictly more powerful and cannot be expressed in terms
|  of #1. But #1 is perhaps more intuitive for programmers, who might
|  expect inference to conclude that the two kinds are the same.
|  
|  Here is an example of where the difference matters:
|  
|  > data KProxy k = KP
|  > class kproxy ~ 'KP => C (kproxy :: KProxy k)
|  
|  We can see that the kind of the type variable kproxy should be (KProxy
|  k). But we still have to infer the kind of the occurrence of 'KP on
|  the left. HEAD sees the kind of kproxy and infers that 'KP should have
|  kind (KProxy k). My branch, on the other hand, doesn't have any reason
|  to constrain the kind of 'KP, and so it gets (KProxy Any), which
|  quickly causes trouble.
|  
|  The fix is easy: add a kind signature.
|  
|  I see two ways forward, corresponding to the choices for the kind of
|  (~) above:
|  
|  1. Make (~) homogeneous and introduce a new constraint (~~) that is
|  like (~) but heterogeneous. We resign ourselves to explaining the
|  technical, subtle difference between (~) and (~~) into perpetuity.
|  
|  2. Make (~) heterogeneous. Some people will have to add kind
|  annotations to their code to port from GHC 7.10 to GHC 8.0. But these
|  kind annotations will be fully backward-compatible, and won't require
|  CPP, or warnings, or any other bother. We may have to explain why kind
|  inference around (~) is weaker than it was before.
|  
|  
|  I'm (clearly?) leaning toward #2. But I'd like feedback.
|  
|  Thoughts?
|  
|  Thanks!
|  Richard
|  _______________________________________________
|  ghc-devs mailing list
|  ghc-devs at haskell.org
|  https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fmail.h
|  askell.org%2fcgi-bin%2fmailman%2flistinfo%2fghc-
|  devs&data=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7c95ca36eba6074ac
|  feefb08d2f36f2700%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=0w0B9q7
|  SJpXzf4UJokFZejYBhiIeASO0bfaJSDVRrJU%3d