Should (~) be homogeneous or heterogeneous?
Simon Peyton Jones
simonpj at microsoft.com
Tue Nov 24 12:54:43 UTC 2015
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"?
| -----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.
| ghc-devs mailing list
| ghc-devs at haskell.org
More information about the ghc-devs