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.
-----