<div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div>Ah, I read over this part [1] of the ScopedSort specification too quickly:</div><div><br></div><div> * If variable v at the cursor is depended on by any earlier variable w,<br> move v immediately before the leftmost such w.</div><div><br></div><div>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.</div><div><br></div><div>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]:</div><div><br></div><div> - If the type signature includes any kind annotations (either on variable<br> binders or as annotations on types), any variables used in kind<br> annotations come before any variables never used in kind annotations.<br> This rule is not recursive: if there is an annotation within an annotation,<br> then the variables used therein are on equal footing. Examples::<br> <br> f :: Proxy (a :: k) -> Proxy (b :: j) -> ()<br> -- as if f :: forall k j a b. ...<br> <br> g :: Proxy (b :: j) -> Proxy (a :: (Proxy :: (k -> Type) -> Type) Proxy) -> ()<br> -- as if g :: forall j k b a. ...<br> -- NB: k is in a kind annotation within a kind annotation</div><div><br></div><div>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.<br></div><div><br></div><div>Ryan S.</div><div>-----</div><div>[1] <a href="https://gitlab.haskell.org/ghc/ghc/blob/5c1f268e2744fab2d36e64c163858995451d7095/compiler/types/Type.hs#L2110-2111">https://gitlab.haskell.org/ghc/ghc/blob/5c1f268e2744fab2d36e64c163858995451d7095/compiler/types/Type.hs#L2110-2111</a></div><div>[2] <a href="https://gitlab.haskell.org/ghc/ghc/blob/5c1f268e2744fab2d36e64c163858995451d7095/docs/users_guide/glasgow_exts.rst#L10815-10826">https://gitlab.haskell.org/ghc/ghc/blob/5c1f268e2744fab2d36e64c163858995451d7095/docs/users_guide/glasgow_exts.rst#L10815-10826</a></div><div>[3] <a href="https://github.com/ghc-proposals/ghc-proposals/blob/c3142c4a6f6abb90e53c2cac22b285991d0d0b3f/proposals/0024-no-kind-vars.rst">https://github.com/ghc-proposals/ghc-proposals/blob/c3142c4a6f6abb90e53c2cac22b285991d0d0b3f/proposals/0024-no-kind-vars.rst</a><br></div></div></div></div></div></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Feb 14, 2019 at 2:04 PM Richard Eisenberg <<a href="mailto:rae@cs.brynmawr.edu">rae@cs.brynmawr.edu</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><br>
<br>
> On Feb 14, 2019, at 10:34 AM, Ryan Scott <<a href="mailto:ryan.gl.scott@gmail.com" target="_blank">ryan.gl.scott@gmail.com</a>> wrote:<br>
> <br>
> the answer [j,a,k,b]! Strictly speaking, this answer meets the specification of ScopedSort,<br>
<br>
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.<br>
<br>
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!<br>
<br>
Richard</blockquote></div>