scopedSort and kind variable left-biasing

[Ryan Scott]

Ah, I read over this part [1] of the ScopedSort specification too quickly:

    * If variable v at the cursor is depended on by any earlier variable w,
      move v immediately before the leftmost such w.

I glossed over the "immediately" part, so I was under the impression that
as long as v appeared *somewhere* to the left of the leftmost w, then
everything was up to spec. But no, v can appear in one (and only one) place.

I was also looking in Note [ScopedSort], not the users' guide. Now that I
look at the users' guide, it specifically carves out an exception for
variables that appear in kind annotations [2]:

    - If the type signature includes any kind annotations (either on
variable
      binders or as annotations on types), any variables used in kind
      annotations come before any variables never used in kind annotations.
      This rule is not recursive: if there is an annotation within an
annotation,
      then the variables used therein are on equal footing. Examples::

        f :: Proxy (a :: k) -> Proxy (b :: j) -> ()
          -- as if f :: forall k j a b. ...

        g :: Proxy (b :: j) -> Proxy (a :: (Proxy :: (k -> Type) -> Type)
Proxy) -> ()
          -- as if g :: forall j k b a. ...
          -- NB: k is in a kind annotation within a kind annotation

I can see the appeal behind dropping this exception, both from a
specification and an implementation point of view. It'll require a massive
breaking change, alas, but it just might be worth it. Unfortunately, the
proposal for merging type and kind variables in `forall`s [3] makes no
mention of this detail—I wonder if it is worth its own proposal.

Ryan S.
-----
[1]
https://gitlab.haskell.org/ghc/ghc/blob/5c1f268e2744fab2d36e64c163858995451d7095/compiler/types/Type.hs#L2110-2111
[2]
https://gitlab.haskell.org/ghc/ghc/blob/5c1f268e2744fab2d36e64c163858995451d7095/docs/users_guide/glasgow_exts.rst#L10815-10826
[3]
https://github.com/ghc-proposals/ghc-proposals/blob/c3142c4a6f6abb90e53c2cac22b285991d0d0b3f/proposals/0024-no-kind-vars.rst

On Thu, Feb 14, 2019 at 2:04 PM Richard Eisenberg <rae at cs.brynmawr.edu>
wrote:

>
>
> > On Feb 14, 2019, at 10:34 AM, Ryan Scott <ryan.gl.scott at gmail.com>
> wrote:
> >
> >  the answer [j,a,k,b]! Strictly speaking, this answer meets the
> specification of ScopedSort,
>
> I wish to point out that the specification of ScopedSort is very tight: it
> says exactly what we should get, given an input. This is important, because
> the behavior of ScopedSort is user-visible and must be stable. Another way
> of saying this: if we got [j,k,a,b], that would be wrong. Arguably, GHC's
> behavior w.r.t. type and kind variables is wrong because of its habit of
> putting kind variables first.
>
> Once we treat kind and type variables identically, I want to just rely on
> ScopedSort. That is, GHC should infer the order [j,a,k,b]. While I
> understand the aesthetic appeal of moving k before a, I think it's simpler
> and more uniform just to use ScopedSort. No exceptions!
>
> Richard
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20190214/6ccee34d/attachment.html>