Invalid type application [GHC-95781]

Type application can only be performed for specified type variables (see documentation on inferred vs. specified type variables). If a type variable is instead inferred, i.e. the type is not annotated or the type variable is marked as inferred with braces, performing a type application for the corresponding type variable leads to this error.

Examples

Type application with type variable marked as inferred

The type annotation forall {k} ... of C marks the type variable k as inferred with the surrounding braces. In the type application C @Type @Int Proxy, the type/kind argument @Type is therefore bound to a rather than k, causing the application to the second type argument @Int to throw an error.

Removing the braces around k allows C to be applied to both type arguments.

Error Message

InferredTypeVarApplication.hs:11:15: error: [GHC-95781]
    • Cannot apply expression of type ‘Proxy (*) -> T (*)’
      to a visible type argument ‘Int’
    • In the expression: C @Type @Int Proxy
      In an equation for ‘x’: x = C @Type @Int Proxy
      In the expression: let x = C @Type @Int Proxy in ()
   |
11 | bar = let x = C @Type @Int Proxy
   |               ^^^^^^^^^^^^^^^^^^
InferredTypeVarApplication.hs
Before
{-# LANGUAGE TypeApplications, RankNTypes, GADTs, PolyKinds #-}

module InferredTypeVarApplication where

import Data.Proxy
import Data.Kind

data T a where C :: forall {k} (a::k). Proxy a -> T a

bar :: ()
bar = let x = C @Type @Int Proxy
      in ()
After
{-# LANGUAGE TypeApplications, RankNTypes, GADTs, PolyKinds #-}

module InferredTypeVarApplication where

import Data.Proxy
import Data.Kind

data T a where C :: forall k (a::k). Proxy a -> T a

bar :: ()
bar = let x = C @Type @Int Proxy
      in ()
Type application with no type variable

The function plus is applied to the type argument Int, but its annotated type Int -> Int -> Int contains no type variable.

Error Message

TypeAppNoTypeVar.hs:8:5: error: [GHC-95781]
    • Cannot apply expression of type ‘Int -> Int -> Int’
      to a visible type argument ‘Int’
    • In the expression: plus @Int 5 7
      In an equation for ‘x’: x = plus @Int 5 7
  |
8 | x = plus @Int 5 7
  |     ^^^^^^^^^^^^^
TypeAppNoTypeVar.hs
Before
{-# LANGUAGE TypeApplications #-}

module TypeAppNoTypeVar where

plus :: Int -> Int -> Int
plus = (+)

x = plus @Int 5 7
After
{-# LANGUAGE TypeApplications #-}

module TypeAppNoTypeVar where

plus :: Int -> Int -> Int
plus = (+)

x = plus 5 7
Type application with non-annotated expression

The lambda expression (\x -> x) has no type annotation, thus the application to the type argument Int is forbidden. To fix the error, one can remove the type application or add a type annotation.

Error Message

TypeForTermArg.hs:5:10: error: [GHC-95781]
    • Cannot apply expression of type ‘p1 -> p1’
      to a visible type argument ‘Int’
    • In the expression: (\ x -> x) @Int 12
      In an equation for ‘lamApp’: lamApp = (\ x -> x) @Int 12
  |
5 | lamApp = (\x -> x) @Int 12
  |          ^^^^^^^^^^^^^^^^^
TypeForTermArg.hs
Before
{-# LANGUAGE TypeApplications, RankNTypes, PolyKinds #-}

module TypeForTermArg where

lamApp = (\x -> x) @Int 12
After
{-# LANGUAGE TypeApplications, RankNTypes, PolyKinds #-}

module TypeForTermArg where

lamApp1 = (\x -> x) 12
lamApp2 = ((\x -> x) :: forall a. a -> a) @Int 12