I don't know if you saw my idea for unlifted types that ties into the work-in-progress on improved impredicativity support, but it relies on the (transient) subtyping constraints being heterogeneous. So it'd need: !a <~ a even though `!a :: Unlifted` and `a :: *`. I don't think this has any direct bearing on ~, because <~ disappears pretty early, I think, and the `<~ turns into ~` rule could be conditioned on the arguments to <~ having homogeneous kinds. Now that I think about it, I'm unsure which direction this supports. The check on `<~ into ~` actually makes sense, because `!a <~ a` should only be satisfied by an 'identity' function `!a -> a`, because the opposite `a -> !a` isn't appropriate, and thus we shouldn't simply have `!a ~ a`. One could still do the check, though, even if ~ is heterogeneous itself. -- Dan On Sun, Nov 22, 2015 at 2:00 PM, Richard Eisenberg wrote:

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

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@haskell.org] On Behalf Of | Richard Eisenberg | Sent: 22 November 2015 19:00 | To: ghc-devs Devs | 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@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