How does topological sorting of kind variables really work?

[Richard Eisenberg]

On Apr 13, 2016, at 5:17 AM, Simon Peyton Jones <simonpj at microsoft.com> wrote:

> I thought that inferred foralls are Invisible binders (see Note [TyBinders and VisibilityFlags]); and you can't use visible type application for Invisible binders.  

No. See that Note. A binder is Invisible only when it is completely unmentioned in the source. The implicitly-bound kind variables Ryan uses are meant to be Specified.

> 
> I thought that was because it's hard to specify the order of inferred type variable, just as Ryan says.

Once the user has written something, then we have a left-to-right ordering to guide us.

> 
> So /is/ inference meant to give a reliable ordering?  If so why?  

We had decided that a signature `f :: a -> a` meant that `a` is specified. It seemed silly if `data P (a :: k)` did not mean that `k` is specified, too.

Another confounding detail here: the `:type` command now fully instantiates a type and then regeneralizes. So any output of `:type` can't be relied upon to get the variable ordering correct. For simple functions, you can use `:info`. But for data constructors, for example, GHC currently provides no way to see which variables are specified, and what order they appear in. See #11376.

It is my intent that any variables mentioned by the user appear in a predictable order in types. That does not seem to be the case here, so this is a bug.

Richard