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