Ah, I somehow forgot all about FreeKiTyVars. It turns out that the `freeKiTyVarsAllVars` function [1] is exactly what drives this behavior: freeKiTyVarsAllVars :: FreeKiTyVars -> [Located RdrName] freeKiTyVarsAllVars (FKTV { fktv_kis = kvs, fktv_tys = tvs }) = kvs ++ tvs That's about as straightforward as it gets. Thanks! Ryan S. ----- [1] https://gitlab.haskell.org/ghc/ghc/blob/5c1f268e2744fab2d36e64c163858995451d... On Thu, Feb 14, 2019 at 12:46 PM Simon Peyton Jones wrote:

See Note [Kind and type-variable binders] in RnTypes, and Note [Ordering of implicit variables].

And the data type FreeKiTyVars.

But NB: that in https://gitlab.haskell.org/ghc/ghc/merge_requests/361, I argue that with this patch we can sweep all this away.

If we did, we’d probably end up with [j,a,k,b].

Perhaps that’s an ergonomic reason for retaining the current rather cumbersome code. (Maybe it could be simplified.)

Simon

*From:* ghc-devs *On Behalf Of *Ryan Scott *Sent:* 14 February 2019 15:35 *To:* ghc-devs@haskell.org *Subject:* scopedSort and kind variable left-biasing

Consider this function:

f :: Proxy (a :: j) -> Proxy (b :: k)

If you just collect the free type variables of `f`'s type in left-to-right order, you'd be left with [a,j,b,k]. But the type of `f` is not `forall (a :: j) j (b :: k) k. Proxy a -> Proxy b`, as that would be ill scoped. `j` must come before `a`, since `j` appears in `a`'s kind, and similarly, `k` must come before `b`.

Fortunately, GHC is quite smart about sorting free variables such that they respect dependency order. If you ask GHCi what the type of `f` is (with -fprint-explicit-foralls enabled), it will tell you this:

λ> :type +v f f :: forall j k (a :: j) (b :: k). Proxy a -> Proxy b

As expected, `j` appears before `a`, and `k` appears before `b`.

In a different context, I've been trying to implement a type variable sorting algorithm similar to the one that GHC is using. My previous understanding was that the entirely of this sorting algorithm was implemented in `Type.scopedSort`. To test my understanding, I decided to write a program using the GHC API which directly uses `scopedSort` on the example above:

main :: IO () main = do let tv :: String -> Int -> Type -> TyVar tv n uniq ty = mkTyVar (mkSystemName (mkUniqueGrimily uniq) (mkTyVarOcc n)) ty j = tv "j" 0 liftedTypeKind a = tv "a" 1 (TyVarTy j) k = tv "k" 2 liftedTypeKind b = tv "b" 3 (TyVarTy k) sorted = scopedSort [a, j, b, k] putStrLn $ showSDocUnsafe $ ppr sorted

To my surprise, however, running this program does /not/ give the answer [j,k,a,b], like what :type reported:

λ> main [j_0, a_1, k_2, b_3]

Instead, it gives the answer [j,a,k,b]! Strictly speaking, this answer meets the specification of ScopedSort, since it respects dependency order and preserves the left-to-right ordering of variables that don't depend on each other (i.e., `j` appears to the left of `k`, and `a` appears to the left of `b`). But it's noticeably different that what :type reports. The order that :type reports, [j,k,a,b], appears to bias kind variables to the left such that all kind variables (`j` and `k`) appear before any type variables (`a` and `b`).

From what I can tell, scopedSort isn't the full story here. That is, something else appears to be left-biasing the kind variables. My question is: which part of GHC is doing this left-biasing?

Ryan S.

Yes -- sweep it away!

On Feb 14, 2019, at 5:30 PM, Simon Peyton Jones via ghc-devs wrote:

What do you (or anyone else) think about sweeping all that stuff away? See my comments on https://gitlab.haskell.org/ghc/ghc/merge_requests/361 https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Fghc%2Fghc%2Fmerge_requests%2F361&data=02%7C01%7Csimonpj%40microsoft.com%7Cfc2d7f5498a34d68153008d692aaa9ae%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636857659024990967&sdata=H7euZSJmjiP%2BNE8KD9WD7TeeuHGFvuHzBAGLebPIMPM%3D&reserved=0

Simon

From: Ryan Scott Sent: 14 February 2019 18:31 To: Simon Peyton Jones Cc: ghc-devs@haskell.org Subject: Re: scopedSort and kind variable left-biasing

Ah, I somehow forgot all about FreeKiTyVars. It turns out that the `freeKiTyVarsAllVars` function [1] is exactly what drives this behavior:

freeKiTyVarsAllVars :: FreeKiTyVars -> [Located RdrName] freeKiTyVarsAllVars (FKTV { fktv_kis = kvs, fktv_tys = tvs }) = kvs ++ tvs

That's about as straightforward as it gets. Thanks!

Ryan S. ----- [1] https://gitlab.haskell.org/ghc/ghc/blob/5c1f268e2744fab2d36e64c163858995451d... https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Fghc%2Fghc%2Fblob%2F5c1f268e2744fab2d36e64c163858995451d7095%2Fcompiler%2Frename%2FRnTypes.hs%23L1604-1605&data=02%7C01%7Csimonpj%40microsoft.com%7Cfc2d7f5498a34d68153008d692aaa9ae%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636857659024990967&sdata=QaWLPwctKWcuIFJFdPAqBhJzA99%2FFtsftSuuAstHVEQ%3D&reserved=0

On Thu, Feb 14, 2019 at 12:46 PM Simon Peyton Jones mailto:simonpj@microsoft.com> wrote: See Note [Kind and type-variable binders] in RnTypes, and Note [Ordering of implicit variables]. And the data type FreeKiTyVars.

But NB: that in https://gitlab.haskell.org/ghc/ghc/merge_requests/361 https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Fghc%2Fghc%2Fmerge_requests%2F361&data=02%7C01%7Csimonpj%40microsoft.com%7Cfc2d7f5498a34d68153008d692aaa9ae%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636857659024990967&sdata=H7euZSJmjiP%2BNE8KD9WD7TeeuHGFvuHzBAGLebPIMPM%3D&reserved=0, I argue that with this patch we can sweep all this away.

If we did, we’d probably end up with [j,a,k,b].

Perhaps that’s an ergonomic reason for retaining the current rather cumbersome code. (Maybe it could be simplified.)

Simon

From: ghc-devs mailto:ghc-devs-bounces@haskell.org> On Behalf Of Ryan Scott Sent: 14 February 2019 15:35 To: ghc-devs@haskell.org mailto:ghc-devs@haskell.org Subject: scopedSort and kind variable left-biasing

Consider this function:

f :: Proxy (a :: j) -> Proxy (b :: k)

If you just collect the free type variables of `f`'s type in left-to-right order, you'd be left with [a,j,b,k]. But the type of `f` is not `forall (a :: j) j (b :: k) k. Proxy a -> Proxy b`, as that would be ill scoped. `j` must come before `a`, since `j` appears in `a`'s kind, and similarly, `k` must come before `b`.

Fortunately, GHC is quite smart about sorting free variables such that they respect dependency order. If you ask GHCi what the type of `f` is (with -fprint-explicit-foralls enabled), it will tell you this:

λ> :type +v f f :: forall j k (a :: j) (b :: k). Proxy a -> Proxy b

As expected, `j` appears before `a`, and `k` appears before `b`.

In a different context, I've been trying to implement a type variable sorting algorithm similar to the one that GHC is using. My previous understanding was that the entirely of this sorting algorithm was implemented in `Type.scopedSort`. To test my understanding, I decided to write a program using the GHC API which directly uses `scopedSort` on the example above:

main :: IO () main = do let tv :: String -> Int -> Type -> TyVar tv n uniq ty = mkTyVar (mkSystemName (mkUniqueGrimily uniq) (mkTyVarOcc n)) ty j = tv "j" 0 liftedTypeKind a = tv "a" 1 (TyVarTy j) k = tv "k" 2 liftedTypeKind b = tv "b" 3 (TyVarTy k) sorted = scopedSort [a, j, b, k] putStrLn $ showSDocUnsafe $ ppr sorted

To my surprise, however, running this program does /not/ give the answer [j,k,a,b], like what :type reported:

λ> main [j_0, a_1, k_2, b_3]

Instead, it gives the answer [j,a,k,b]! Strictly speaking, this answer meets the specification of ScopedSort, since it respects dependency order and preserves the left-to-right ordering of variables that don't depend on each other (i.e., `j` appears to the left of `k`, and `a` appears to the left of `b`). But it's noticeably different that what :type reports. The order that :type reports, [j,k,a,b], appears to bias kind variables to the left such that all kind variables (`j` and `k`) appear before any type variables (`a` and `b`).

From what I can tell, scopedSort isn't the full story here. That is, something else appears to be left-biasing the kind variables. My question is: which part of GHC is doing this left-biasing?

Ryan S.

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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/5c1f268e2744fab2d36e64c163858995451d... [2] https://gitlab.haskell.org/ghc/ghc/blob/5c1f268e2744fab2d36e64c163858995451d... [3] https://github.com/ghc-proposals/ghc-proposals/blob/c3142c4a6f6abb90e53c2cac... On Thu, Feb 14, 2019 at 2:04 PM Richard Eisenberg wrote:

...

On Feb 14, 2019, at 10:34 AM, Ryan Scott 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

| 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! I agree. And then we can dispose entirely of the FreeKiTyVars stuff in RnTypes. Vlad: doing so would fit very neatly into https://gitlab.haskell.org/ghc/ghc/merge_requests/361 Simon | -----Original Message----- | From: ghc-devs On Behalf Of Richard | Eisenberg | Sent: 14 February 2019 19:04 | To: Ryan Scott | Cc: ghc-devs@haskell.org | Subject: Re: scopedSort and kind variable left-biasing | | | | > On Feb 14, 2019, at 10:34 AM, Ryan Scott 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 | _______________________________________________ | ghc-devs mailing list | ghc-devs@haskell.org | https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.haske | ll.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc- | devs&data=02%7C01%7Csimonpj%40microsoft.com%7Cfe4658679a9d474f232e08d69 | 2af3ab0%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636857678634719246& | ;sdata=XhEw8LYBtqVxn%2BjpeHxus5%2FRTrUVlCU%2FRJrIYUsLpDY%3D&reserved=0