5.10. Type Ascription

Type ascriptions explicitly annotate terms with their types. They are a way to provide Lean with the expected type for a term. This type must be definitionally equal to the type that is expected based on the term's context. Type ascriptions are useful for more than just documenting a program:

  • There may not be sufficient information in the program text to derive a type for a term. Ascriptions are one way to provide the type.

  • An inferred type may not be the one that was desired for a term.

  • The expected type of a term is used to drive the insertion of coercions, and ascriptions are one way to control where coercions are inserted.

syntaxPostfix Type Ascriptions

Type ascriptions must be surrounded by parentheses. They indicate that the first term's type is the second term.

term ::= ...
    | Type ascription notation: `(0 : Int)` instructs Lean to process `0` as a value of type `Int`.
An empty type ascription `(e :)` elaborates `e` without the expected type.
This is occasionally useful when Lean's heuristics for filling arguments from the expected type
do not yield the right result.
(term : term)

In cases where the term that requires a type ascription is long, such as a tactic proof or a Lean.Parser.Term.do : termdo block, the postfix type ascription with its mandatory parentheses can be difficult to read. Additionally, for both proofs and Lean.Parser.Term.do : termdo blocks, the term's type is essential to its interpretation. In these cases, the prefix versions can be easier to read.

syntaxPrefix Type Ascriptions
term ::= ...
    | show term from term

When the term in the body of Lean.Parser.Term.show : termshow is a proof, the keyword Lean.Parser.Term.show : termfrom may be omitted.

term ::= ...
    | show term by A sequence of tactics in brackets, or a delimiter-free indented sequence of tactics.
Delimiter-free indentation is determined by the *first* tactic of the sequence. tacticSeq
Ascribing Statements to Proofs

This example is unable to execute the tactic proof because the desired proposition is not known. As part of running the earlier tactics, the proposition is automatically refined to be one that the tactics could prove. However, their default cases fill it out incorrectly, leading to a proof that fails.

example (n : Nat) := n:Nat⊢ HEq 0 n ⊢ HEq 0 0n✝:Nata✝:HEq 0 n✝⊢ HEq 0 (n✝ + 1) next ⊢ HEq 0 0 All goals completed! 🐙 next n' ih n':Natih:HEq 0 n'⊢ HEq 0 (n' + 1) n':Natih:HEq 0 n'⊢ HEq 0 n'.succ rewrite [n':Natih:HEq 0 n'⊢ HEq 0 n'.succ] rfl 
tactic 'rewrite' failed, equality or iff proof expected
  HEq 0 n'
n' : Nat
ih : HEq 0 n'
⊢ HEq 0 n'.succ

A prefix type ascription with Lean.Parser.Term.show : termshow can be used to provide the proposition being proved. This can be useful in syntactic contexts where adding it as a local definition would be inconvenient.

example (n : Nat) := show 0 + n = n by ⊢ 0 + 0 = 0n✝:Nata✝:0 + n✝ = n✝⊢ 0 + (n✝ + 1) = n✝ + 1 next ⊢ 0 + 0 = 0 All goals completed! 🐙 next n' ih n':Natih:0 + n' = n'⊢ 0 + (n' + 1) = n' + 1 n':Natih:Nat.add 0 n' = n'⊢ (Nat.add 0 n').succ = n'.succ rewrite [n':Natih:Nat.add 0 n' = n'⊢ n'.succ = n'.succ] All goals completed! 🐙
Ascribing Types to Lean.Parser.Term.do : termdo Blocks

This example lacks sufficient type information to synthesize the Pure instance.

example := do typeclass instance problem is stuck, it is often due to metavariables Pure ?m.75return 5 
typeclass instance problem is stuck, it is often due to metavariables
  Pure ?m.75

A prefix type ascription with Lean.Parser.Term.show : termshow, together with a hole, can be used to indicate the monad. The default OfNat _ 5 instance provides enough type information to fill the hole with Nat.

example := show StateM String _ from do return 5