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 <ghc-devs@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@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