Could you please add some passing and failing tests where a top-level declaration does not have a type signature but there is a local type synonym used in its definition? I feel like it would be good to test that, e.g., the inferred type for the top level declaration does not mention the local synonym in such cases.

(although you might want to wait until we've made a decision on whether to move forward with this, sorry)

I added tests as requested (see failing/LocalTypeSynonyms5 and 6, and the end of passing/LocalTypeSynonyms); not sure they cover everything you had in mind though. Mind taking a look? (The build is failing for the same reason master is; I don't see any new hlint complaints in this PR.)

Yeah, that's what I was imagining. Thanks! Also could I request that you not force-push, since it makes it a bit harder to review? We can save commit rewriting for when we're ready to merge.

Oh, of course! Sorry for the trouble.

No worries! 🙂

Do we need to support standalone kind signatures for polykinds?

Probably! I can easily add some tests that copy what the type synonym parts of the StandaloneTypeSignatures tests do, only in an inner scope; but I think there are probably more interesting things to test around using and/or shadowing kinds from the outer scope. I'm not very comfortable with polykinds yet; do you have any particularly tricky things to exercise in mind?

The primary issues I'm thinking about are:

• We generalize the kinds of type-level declarations. Type-level declarations are all top-level, and so they have the same generalization strategy as top-level value declarations. It's not clear to me that local type synonyms should be generalized, since we don't otherwise generalize local value declarations.
• We warn on generalization of type-level declarations like we warn on generalization of value declarations. If we are hoisting and generalizing local declarations, what do these warnings look like?

These issues are part of what make me hesitant to implement this as a desugaring step.

I could be missing something here, but is generalization a concern for type synonyms? Since there can't be cycles in type synonyms, eventually all type synonym expansions will bottom out in some type made of top level data, from which kinds can be inferred. Any parameters to type synonyms that aren't included in this final expansion are not only generalizable, they're completely irrelevant, right? There's no point in having them at all: type synonyms can't be partially applied, and everything else in the language that uses types such as instance resolution depends on the expansion, not the synonym form. So generalizing makes no difference; unused type synonym parameters at any scope, top-level or not, could be errors and I don't think any real programs would be affected. Is that right?

I should clarify, I don't think there's necessarily an implementation problem with generalizing, it's more about expectations around where and how we generalize in PureScript, and if we want a consistent rule-set for generalization, and how warnings and such around it are exposed to the user.

An example to test for right now would be defining a local type LocalApp a = f a synonym where f is bound in the current scope. How does the compiler treat that and warn?

An example to test for right now would be defining a local type LocalApp a = f a synonym where f is bound in the current scope. How does the compiler treat that and warn?

Ah, thank you, I think I see the problem now. We're talking about generalization of the type parameters that get added from the local scope. Prior to polykinds, these all had definite kinds at the forall site, either explicitly stated or implicitly Type. But now they can generalize, and the compiler warns about that, and is that right?

On reflection, this seems like a specification question rather than a question about this particular implementation (although, even in the absence of a right thing, this implementation is clearly doing a wrong thing by issuing a warning about type local$1$1$LocalApp). I propose moving this conversation over to #3708.

I'm closing this in favor of #3897, as I'm now reasonably convinced that getting kind signatures and the desired generalization behavior right with desugaring is more trouble than not. There are very probably still issues to work out with #3897 but for now it certainly looks like the more practical path forward (assuming of course that the maintainers ultimately decide the feature is desirable at all).