Why can't you (totally) apply a type synonym that has arguments using an other type synonym?

Question

We can define type synonyms with arguments and this works fine when used with actual types:

type MyType t = t String String

data Test a b = Test a b

f :: MyType Test
f = undefined

main = undefined

Compiling this results in no errors:

$ghc --make test.hs                                           
[1 of 1] Compiling Main             ( test.hs, test.o )                                          
Linking test ...   

However this doesn't work when Test is a type synonym:

type MyType t = t String String

data Test a b = Test a b

type Test' a b = Test a b

f :: MyType Test'
f = undefined

main = undefined

Which gives the following error:

$ghc --make test.hs
[1 of 1] Compiling Main             ( test.hs, test.o )

test.hs:7:6:
    Type synonym Test' should have 2 arguments, but has been given none
    In the type signature for `f': f :: MyType (Test')

What puzzles me is that Test' is being applied to two arguments, so why is GHC complaining that I didn't pass the arguments?

Shouldn't type synonym be completely transparent and impossible to distinguish from other kind of types?

Is there any way to achieve the expected behaviour?

Answer 1

According to the Haskell report type synonyms cannot be partially applied:

Type constructor symbols T introduced by type synonym declarations cannot be partially applied; it is a static error to use T without the full number of arguments.

In particular this is checked before expanding the type synonyms, this means that in the expression:

MyType Test'

The check is performed before expanding MyType and hence Test' results partially applied.

However, it is possible to achieve that behaviour using GHC LiberalTypeSynonyms extension. This extension treats type synonyms as macros, which are expanded without any check and afterwards the type checker will see whether the type synonym was partially applied.

^{Kind inference is still done before type synonym expansion.}

Note that type synonyms cannot be partially applied even in this case, i.e. something such as:

Test' Int

is still an error. However you now can use type synonyms to totally apply other type synonyms without receiving errors.

Allowing partial application of type synonyms would make type inference undecidible, so it's not possible to easily extend the type system in that direction.