Allow visible type application in patterns

EDIT: Though this ticket predates the proposal, it is a good place to track its development: https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0126-type-applications-in-patterns.rst

Constructors (and pattern synonyms) when treated as expressions may be applied to types:

{-# LANGUAGE TypeApplications #-}

Nothing     :: Maybe a
Nothing @() :: Maybe ()

pattern Pair :: a -> a -> (a, a)
pattern Pair x y = (x, y)

Pair      :: a   -> a   -> (a, a)
Pair @Int :: Int -> Int -> (Int, Int)

But using them in patterns won't parse:

-- parse error in pattern: @Int
maybeToList :: Maybe Int -> [Int]
maybeToList (Nothing @Int) = []
maybeToList (Just @Int x)  = [x]

-- parse error in pattern: @Int
add :: (Int, Int) -> Int
add (Pair @Int x y) = x + y

Trac metadata

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

mentioned in issue #8583

changed weight to 5

added Tfeature request Trac import TypeApplications labels

mentioned in issue #11351 (closed)

Relevant note on ⟦Lexing type applications⟧

mentioned in issue #11385 (closed)

This should make the code in Richard's comment compile:

headOfList :: forall a. [a] -> Maybe a
headOfList (Nil  @[] @a)     = Nothing @a
headOfList (Cons @[] @a x _) = Just x

The rest of his comment applies to, this is not for dynamically branching on types although that could certainly be added as a feature!

doubleWhenInt :: forall a. Typeable a => a -> a
doubleWhenInt a =
  case eqT @Int @a of
    Just Refl -> a + a
    Nothing   -> a

-- Becomes…
doubleWhenInt :: forall a. Typeable a => a -> a
doubleWhenInt @Int n = n + n
doubleWhenInt @_   a = a

mentioned in issue #11387

Yes, this is a good idea. It would give a much nicer way to bind (particularly existential) type variables than the current ScopedTypeVariables hack. I think typecase should be treated separately though, and with lower priority (cf. #11387).

mentioned in issue #11441

While commenting on #11441, what about lambdas?

-- Should work, given proposal.
id :: forall a. a -> a
id @a x = x

-- Also.
id :: forall a. a -> a
id (@ a) (x :: a) = x

-- What about this?
id :: forall a. a -> a
id = \ (@ a) (x :: a) -> x

-- Or this
id :: b -> b
id = \ (@ a) (x :: a) -> x

Same question extends to LambdaCase.

Yes. I think all of these should work, modulo parsing. (I'm worried about (@ a) instead of @a. Would need to test to be sure.)

mentioned in issue #11638 (closed)

mentioned in issue #11671 (closed)

mentioned in issue #11992 (closed)

mentioned in issue #12001

mentioned in issue #12018 (closed)

mentioned in issue #12025 (closed)

See ticket:11638#comment:116813 for some detailed thoughts about design challenges here.