Type synonym impossible to fully apply in type application

[LiamGoodacre]

Description

Possible kind inference funkiness going on with synonyms in type applications.

Using the same type expression in an annotation vs a type application works differently.

To Reproduce

try purescript

module Main where
import Prelude
import Type.Proxy (Proxy(..))

-- `i` will be determined when `x` is concrete
type F :: forall i . Row i -> Row i
type F x = ()

-- type checks; `i ~ Type`
y :: Proxy (F (() :: Row Type))
y = Proxy

-- fails:
--   Type synonym Main.F is partially applied.
--   Type synonyms must be applied to all of their type arguments.
z :: Proxy (F (() :: Row Type))
z = Proxy @(F (() :: Row Type))

type G = F (() :: Row Type)
-- also works
g :: Proxy G
g = Proxy @G

Expected behavior

z would also pass type checking.

PureScript version

0.15.13

[rhendric]

Interestingly, this works:

z :: Proxy (F (() :: Row Type))
z = Proxy @(() :: Row Type)

Definitely a bug somewhere.

[natefaubion]

-- `i` will be determined when `x` is concrete
type F :: forall i . Row i -> Row i
type F x = ()

type Z :: forall i . Row i -> Row i
type Z x = ()

-- fails:
--   Type synonym Main.Z is partially applied.
--   Type synonyms must be applied to all of their type arguments.
z :: Proxy (F (() :: Row Type))
z = Proxy @(Z (() :: Row Type))

Since the failure is in the type-application, my guess is that there is a kind-checker elaboration rule missing for type applications.