How does topological sorting of kind variables really work?
eir at cis.upenn.edu
Wed Apr 13 20:20:45 UTC 2016
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.
More information about the ghc-devs