Hi Richard,

Many thanks for the hints!

I can see two ways to proceed:

i) First determine the kinds of all the data types, classes, and type synonyms.  Then perform a second pass over each type or class to determine the kinds of type variables (in class methods) that are not type class parameters.

This won't work.

class C a where

  meth :: a b -> b Int

You have to know the kind of local b to learn the kind of class-variable a. So you have to do it all at once.

I was doing it all at once -- but I wasn't sure how to export the information about 'b' from the procedure.  (After you record the kinds of the typecons like C, I believe the different typecons in the recursive group become separable.)

I presume (in retrospect) that GHC modifies the declaration to record the kind of b, and then re-walks the declaration to substitute kind variables later?

iii) Represent kinds with modifiable variables.  Substitution can be implemented by modifying kind variables in-place.  This is (I think) called "zonking" in the GHC sources.

I don't really see the difference between (ii) and (iii). Maybe (ii) records the kinds in a table somewhere, while (iii) records them "in" the kind variables themselves, but that's not so different, I think.

Yeah, that is a good point.  That clarified for me what GHC is doing.

This solves a small mystery for me, since I previously thought that zonking was just replacing remaining kind variables with '*'.  And indeed this seems to be an example of zonking, but not what zonking is (I think).

We can imagine that, instead of mutation, we build a substitution mapping unification variables to types (or kinds). This would be stored just as a simple mapping or dictionary structure. No mutation. As we learn about a unification variable, we just add to the mapping. If we did this, zonking would be the act of applying the substitution, replacing known unification variables with their values. It just so happens that GHC builds a mapping by using mutable cells in memory, but that's just an implementation detail: zonking is still just applying the substitution.

OK, that makes sense.  I'll start with the mapping approach, and then consider optimizing things later.

Zonking does not replace anything with *. Well, functions that have "zonk" in their name may do this. But it is not really logically part of the zonking operation. If you like, you can pretend that, after zonking a program, we take a separate pass replacing any yet-unfilled kind-level unification variables with *. Sometimes, this is called "zapping" in GHC, I believe.

Yes, I was definitely confusing zonking and zapping.  (Wow, lots of fun names here!)

Zonking is a bit laborious to implement, but not painful. Laborious, because it requires a full pass over the AST. Not painful, because all it's trying to do is replace type/kind variables with substitutions: each individual piece of the puzzle is quite simple.

But if that is a difficulty on the right road, I will just go for it. 

-BenRI