Should (~) be homogeneous or heterogeneous?

[Richard Eisenberg]

On Nov 24, 2015, at 7:54 AM, Simon Peyton Jones <simonpj at microsoft.com> wrote:

> 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?
> 

All tyvars mentioned in superclass constraints must be introduced in the class head. Your version violates this constraint.


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

Suppose I then say

> instance C ('KP :: KProxy Bool)

GHC needs to prove ('KP :: KProxy Bool) ~ ('KP :: KProxy Any) and it has a hard time doing so.

In any case, I've now seen enough very weird gotchas around heterogeneous ~ to convince me to keep it homogeneous, and to introduce ~~. If you want (~~), you'll need to import it from Data.Type.Equality -- it won't have magical scope like (~) does.

Thanks for the feedback.

Richard

> 
> 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
>