10.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.
([anonymous]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 tactic 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) := byn:Nat⊢ ?m.2 n
  induction nzero⊢ ?m.2 0succn✝:Nata✝:?m.2 n✝⊢ ?m.2 (n✝ + 1)
  next =>⊢ ?m.2 0 rflAll goals completed! 🐙
  next n' ih =>n':Natih:?m.2 n✝⊢ ?m.2 (n✝ + 1)
    simp only [HAdd.hAdd, Add.add, Nat.add] at *n':Natih:0 ≍ n'⊢ 0 ≍ n'.succ
    rewrite [Invalid rewrite argument: Expected an equality or iff proof or definition name, but `ih` is a proof of
  0 ≍ n'ih]n':Natih:0 ≍ n'⊢ 0 ≍ n'.succ
    rfl

Invalid rewrite argument: Expected an equality or iff proof or definition name, but `ih` is a proof of
  0 ≍ n'

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 byAll goals completed! 🐙
  induction nzero⊢ 0 + 0 = 0succn✝:Nata✝:0 + n✝ = n✝⊢ 0 + (n✝ + 1) = n✝ + 1
  next =>⊢ 0 + 0 = 0 rflAll goals completed! 🐙
  next n' ih =>n':Natih:0 + n✝ = n✝⊢ 0 + (n✝ + 1) = n✝ + 1
    simp only [HAdd.hAdd, Add.add, Nat.add] at *n':Natih:Nat.add 0 n' = n'⊢ (Nat.add 0 n').succ = n'.succ
    rewrite [ih]n':Natih:Nat.add 0 n' = n'⊢ n'.succ = n'.succ
    rflAll goals completed! 🐙

Live ↪

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
  Pure ?m.12

Note: Lean will not try to resolve this typeclass instance problem because the type argument to `Pure` is a metavariable. This argument must be fully determined before Lean will try to resolve the typeclass.

Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.return 5

typeclass instance problem is stuck
  Pure ?m.12

Note: Lean will not try to resolve this typeclass instance problem because the type argument to `Pure` is a metavariable. This argument must be fully determined before Lean will try to resolve the typeclass.

Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.

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

Live ↪