Different behavior between type application and type annotation.

Consider this code:

{-# LANGUAGE FlexibleInstances, TypeApplications #-}

module Bug where

class Foo t where
  foo_ :: (IO () -> IO ()) -> t

instance (Show a, Foo t) => Foo (a -> t) where
  foo_ k a = foo_ (\continue -> k (print a >> continue))

instance Foo (IO ()) where
  foo_ k = k (return ())

foo :: Foo t => t
foo = foo_ id

bar = foo () (Just "bar") [()] :: IO ()

baz = foo @(IO ()) () (Just "baz") [()]

bar is accepted by GHC while baz is rejected:

    * Couldn't match expected type `() -> Maybe [Char] -> [()] -> t'
                  with actual type `IO ()'
    * The function `foo' is applied to four arguments,
      but its type `IO ()' has none
      In the expression: foo @(IO ()) () (Just "baz") [()]
      In an equation for `baz': baz = foo @(IO ()) () (Just "baz") [()]
    * Relevant bindings include baz :: t (bound at bug.hs:19:1)
   |
19 | baz = foo @(IO ()) () (Just "baz") [()]
   |       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Why so?

Trac metadata

Trac field	Value
Version	8.2.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture