For things like this, I recommend using the debug functions in TypeChecker.Monad, specifically for this debugSubstitution, which will print out all the unification variables with either their kinds (if unsolved) or solutions (if solved). In this particular case, the substitution environment before kind checking that synonym is:

?2 = t4
?3 = t4
?4 :: Type

So the particular unification variable in the error definitely exists. The reason for the error is that kindOfTypeSynonym calls kindsOfAll, which is wrapped in withFreshSubstitution. withFreshSubstitution sets up an empty substitution environment. You want this for top-level declarations, but clearly not in this case. Your intuition is correct, in that we need to extract some of the logic into something appropriate for local synonyms.

The apparent complexity of kindsOfAll comes from dealing with recursive type-level binding groups, which is not possible in a local context like this since we disallow recursive type synonyms altogether. Recursive binding groups need to be generalized correctly so that all the kind-polymorphism can be threaded around between them. We don't want to do any of that for local type synonyms. For the most part, you can just call call inferTypeSynonym directly. This will infer the kind of the body, and elaborate the rhs with kind applications. There is some setup though that's done, and a few post-inference checks to account for.

inferTypeSynonym assumes that there is a kind for the type synonym in the environment. For type synonyms without explicit kind signatures, this should be a fresh unification variable. kindsOfAll sets this up using existingSignatureOrFreshKind. inferTypeSynonym will unify against whatever is in the environment.

The checkEscapedSkolems check is necessary, and it should already account for types in scope, so I think no changes are necessary here. This just ensures that there are no skolems left over that don't also have an appropriate entry in the type environment. I'm not positive that the main typechecker puts skolems in the type environment though, so that may need some validation.

I don't think that checkTypeQuantification is likely necessary. The purpose of this check is to make sure there are no unknowns leftover after generalization. This can happen when you have a closed kind application. A term-level analog is length [], where length must be instantiated with the type of [], which can be anything. At the kind-level this would be left as an unbound unification variable. I don't believe this would be observable for local type synonyms.

I'm going to guess that checkVisibleTypeQuantification is unnecessary. We don't currently support visible quantification. In top-level contexts however it's possible to require this through generalization. Since we are not generalizing local type synonyms, we can probably elide this check.

@natefaubion Thank you so much! That was immensely useful.

There are likely a few more edge cases that I haven't yet tested and fixed, but this is now mostly functional.

We need to support local synonyms in the shadowing lint for both:

• type synonyms shadowing other type level names
• type variables in type synonyms shadowing other type variables.

For the first case: ShadowedName, or a new error constructor?

If the types work out, I say reuse it, otherwise a new one.

Warnings have been added! Most of them were not put in the Linter module proper, since quantifier type variables aren't associated with value declarations until the type checking phase. In theory I imagine this could be changed, but the existing type variable shadowing warning lives in the type checker so that's where I put the new warnings that use the same information. I hope that's reasonable.