Skip to content

The types-in-terms syntax (forall, ->, =>)

In accordance with GHC Proposal #281, the syntax of expressions must be extended with several constructs that previously could only occur at the type level:

  • Function arrows: a -> b
  • Multiplicity-polymorphic function arrows: a %m -> b (under -XLinearTypes)
  • Constraint arrows: a => b
  • Universal quantification: forall a. b
  • Visible universal quantification: forall a -> b

The purpose of the new syntax is to be used in required type arguments (via T2T). Using it in a free-standing expression is an error.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information