Type inference for type abstractions in functions

Summary

GHC Proposal #448, section 5.2, subsection 4, bullet i, reads as follows:

In synthesis mode, when examining \ @a -> expr, we simply put a in scope as a fresh skolem variable (that is, not equal to any other type) and then check expr. (Presumably, expr uses a in a type signature.) When we infer that expr has type ty, the expression \ @a -> expr has type forall a. ty. Example: \ @a (x :: a) -> x infers the type forall a. a -> a. (For this example, we note that \ @a (x :: a) -> x is a short-hand for \ @a -> \ (x :: a) -> x.)

Furthermore, bullet iii reads:

In synthesis mode, when examining a function argument @a to a function f, we bring a into scope as a fresh skolem variable and check the remainder of the arguments and the right-hand side. In the type of f, we include a forall a. in the spot corresponding to the type variable argument.

So, per the proposal, TypeAbstractions should support type inference. However, at the moment, they don't:

ghci> f @a = 42 :: a
<interactive>:3:3: error: [GHC-14964]
    • Invisible type pattern a has no associated forall
    • In an equation for ‘f’: f @a = 42 :: a

Steps to reproduce

Try to compile this code:

{-# LANGUAGE TypeAbstractions #-}

module T25660 where

-- No signature:
f @a = 42 :: a

Expected behavior

The declaration of f is accepted with the inferred type f :: forall a. Num a => a.

Environment

• GHC version used: 9.12.1