For things like this, I recommend using thedebug functions inTypeChecker.Monad, specifically for thisdebugSubstitution, 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 thatkindOfTypeSynonym callskindsOfAll, which is wrapped inwithFreshSubstitution.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 ofkindsOfAll 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 callinferTypeSynonym 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 synonymswithout explicit kind signatures, this should be a fresh unification variable.kindsOfAll sets this up usingexistingSignatureOrFreshKind.inferTypeSynonym will unify against whatever is in the environment.

ThecheckEscapedSkolems 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 thatcheckTypeQuantification is likely necessary. The purpose of this check is to make sure there are no unknowns leftoverafter generalization. This can happen when you have a closed kind application. A term-level analog islength [], wherelength 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 thatcheckVisibleTypeQuantification 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 theLinter 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.