Why doesn't TypeApplications allow partially applied type synonyms to be used

Question

I did some search and thought that LiberalTypeSynonyms would allow it. It would allow to use partially applied type synonyms as argument to Type in some cases.

{-# LANGUAGE LiberalTypeSynonyms #-}

type Value a = ExceptT [a] Identity a
type Apply m a = m a
run1 :: Apply Value a -> IO ()
run1 e = undefined 

But the following does not work in TypeApplications, why and is it possible to make it compiled?

{-# LANGUAGE LiberalTypeSynonyms #-}
{-# LANGUAGE TypeApplications #-}

type Value a = ExceptT [a] Identity a

run :: m Int -> IO ()
run e = undefined 

main :: IO ()
main = do
    print "begin"
    let a = run @Value 
    print "end"

The above code does not compile due to the error

    • The type synonym ‘Value’ should have 1 argument, but has been given none
    • In the expression: run @Value
      In an equation for ‘a’: a = run @Value
      In the expression:
        do print "begin"
           let a = run @Value
           print "end"
   |
30 |     let a = run @Value 

Answer 1

This doesn't have much to do with -XTypeApplications. Haskell generally doesn't allow type synonyms to be used without completely applied arguments. All that -XLiberalTypeSynonyms does is circumventing this in case it's possible to inline an entire expression – e.g. if you have

{-# LANGUAGE LiberalTypeSynonyms #-}

type IntApplied f = f Int
type List a = [a]

foo :: IntApplied List
foo = [1,2,3]

In this case, the type synonyms can just be substituted right there and then to foo :: [Int], before any type checking or instance resolution happens. It's like something a simple macro processor could do.

But in your case you're trying to pass an incomplete type synonym to something else as-is. run can't know whether or not the type variable it receives can be “inlined” this way, but it would in general need to be able to match on this variable, and that's just not possible on general type-level functions (as you can define with type synonyms/families), it's only possible on type constructors.

See https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0242-unsaturated-type-families.rst for how Haskell is moving forwards in this subject.