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
[email protected]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Reply via email to