Opened 6 years ago

Closed 17 months ago

#4466 closed feature request (duplicate)

Add extension for type application

Reported by: igloo Owned by:
Priority: low Milestone: 8.0.1
Component: Compiler Version: 6.12.3
Keywords: Cc: wren@…, sweirich@…, mail@…, hamidhasan14@…, jstolarek
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #5296 Differential Rev(s):
Wiki Page:


In we discussed adding an extension for explicit type application.

The main stumbling block is syntax.

For example, we would like to be able to write something to the effect of

(Just @ Char) 'a'

and also to be able to pattern match types, e.g.

f ((Just @ t) x) = (Right @ String @ t) x

For a more useful example:

data T where
    MkT :: forall a. a -> (a -> Int) -> T

f (MkT @ a x g) = g (x::a)

Possible suggested syntaxes to make something of type

Maybe (forall a. a->a)


Just @ (forall a. a->a) id    (@ has another meaning in patterns)
Just[forall a. a->a] id       (pvs, opal, HasCASL with paramterized modules; conflicts with Haskell list syntax)
Just {forall a. a->a} id      (Agda)
#Just (forall a. a->a) id
@Just (forall a. a->a) id     (coq)

In the last 2 cases we would presumably have something like

Just :: forall a . a -> Maybe a
Just :: Char -> Maybe Char
#Just :: /\ a . a -> Maybe a
#Just Char :: Char -> Maybe Char

and similarly

#map :: /\ a b . (a -> b) -> [a] -> [b]

Change History (13)

comment:1 Changed 6 years ago by igloo

Milestone: 7.2.1

comment:2 Changed 6 years ago by igloo

See also #5296.

comment:3 Changed 5 years ago by igloo

Priority: normallow

comment:4 Changed 5 years ago by WrenThornton

Cc: wren@… added

comment:5 Changed 4 years ago by igloo


comment:6 Changed 4 years ago by sweirich

Cc: sweirich@… added

comment:7 Changed 4 years ago by kosmikus

Cc: mail@… added

comment:8 Changed 4 years ago by Hamidhasan

Cc: hamidhasan14@… added
difficulty: Unknown

comment:9 Changed 3 years ago by jstolarek

Cc: jan.stolarek@… added

comment:10 Changed 3 years ago by thoughtpolice


Moving to 7.10.1.

comment:11 Changed 2 years ago by thoughtpolice


Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.

comment:12 Changed 18 months ago by thoughtpolice


Milestone renamed

comment:13 Changed 17 months ago by jstolarek

Cc: jstolarek added; jan.stolarek@… removed
Resolution: duplicate
Status: newclosed

Clearly this has been duplicated by #5296 but since all the discussion is happening there I will close this ticket.

Note: See TracTickets for help on using tickets.