This isn't right really, it's specifically to do with the synonym and the synonym alone:

data Const a b = Const a
data IdentityF f a = IdentityF (f a)

ok :: IdentityF (Const Int) Unit
ok = IdentityF (Const 5)

type A = Const

alsoOk :: IdentityF (A Int) Unit
alsoOk = IdentityF (Const 5)

type B a = Const a

alsoAlsoOk :: IdentityF (B Int) Unit
alsoAlsoOk = IdentityF (Const 5)

type X a b = Const a b

error :: IdentityF (X Int) Unit
error = IdentityF (Const 5)

Allowing partially applied type synonyms basically turns them into type level functions (an example here: https://stackoverflow.com/a/4923883), which sounds cool, but then it's not possible to check their equality in general.

You say that this error is related to the type synonym alone.

So this error has nothing to do with how it's replaced with its underlying type? But it's related to the underlying type somehow, too, no?

If the desugaring pass sees IdentityF (X Int) Unit, how would it know if the type synonym is partially applied? It would need to look at its underlying type, no?

Type synonyms seem benign and great... until you start looking at how to explain their interplay with data types. The problem seems to be a conflict with the syntax (what it appears to be) and the semantics (what it means). It looks like it can be used to do whatever type trickery you'd like, like you can with data types, but it's actually a trap.

To make a light metaphor, data : Pikachu :: type : Mimikyu: https://www.mymbuzz.com/wp-content/uploads/sites/2/2018/02/Detective-Pikachu-3DS-with-Mimikyu.jpg
It's a water-type! Mimikyu, electric attack! What? You can't do electric attacks? :)

I find this error to be absolutely unexplainable, which is so terribly frustrating. :(

I've looked at this error long enough and decided that it's unexplainable, sadly. The best docs I can come up with is to just not try to explain it and just give a code example of why it happens, and how to fix it.

I'll update.

So this error has nothing to do with how it's replaced with its underlying type? But it's related to the underlying type somehow, too, no?

No, take a look at the example - A, B, and X are all synonyms for exactly the same thing, they only differ in their defined arity, I did that to illustrate the issue is not to do with the result after expanding the synonym, but the way the synonym itself is used.

You can't explain this restriction in terms of some other part of the type system, because it's specific to synonyms. Synonyms need to exist with their own treatment in the type system as if they were somehow an alias for existing constructions you wouldn't be able to say things like type X a = a. newtype and data can be talked about interchangeably because newtype is just a restriction of data with guarantees about its runtime representation, there are no additional capabilities.

There are some good arguments for not having synonyms at all, but there are also some extremely tedious consequences of that approach. 😄

The why of the restriction is what I mentioned about them becoming functions if partial application is allowed, so having undecidable equality in general. Which makes typechecking undecidable (although there are probably ways that can happen now via fundeps, etc. but not with types alone).

@garyb Oh! I see it now! I stared at your code snippet for ~20 minutes without getting any meaning from it. Your persistence wasn't for naught. I tried to explain it in my latest commit here.

In my explanation, there is still a thing which seems inconsistent. I'm fine with it, but I'm sure such an inconsistency will frustrate others.

To properly use a type alias having type parameters, you must apply it to a type parameter at every location in the program...

and

A type synonym can be partially applied in the context of a type synonym, however.

A type synonym can be partially applied in the context of a type synonym, however.

Hmm, interesting! That's probably not intentional.

aliase -> alias