scopedSort and kind variable left-biasing
ryan.gl.scott at gmail.com
Thu Feb 14 19:32:15 UTC 2019
Ah, I read over this part  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 :
- If the type signature includes any kind annotations (either on
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
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  makes no
mention of this detail—I wonder if it is worth its own proposal.
On Thu, Feb 14, 2019 at 2:04 PM Richard Eisenberg <rae at cs.brynmawr.edu>
> > On Feb 14, 2019, at 10:34 AM, Ryan Scott <ryan.gl.scott at gmail.com>
> > 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!
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the ghc-devs