Explain where adding type hints can help the inference system in static typing chapter

[ss2165]

For python users asking for type hints on functions seems to be natural, but hinting elsewhere (e.g. choosing generics, specifying array sizes) to help the type inference engine is unintuitive. Explain this with examples, and if possible add hints to errors to suggest adding type hints.

[CalMacCQ]

What would be such an example of this?

[ss2165]

from guppylang import guppy
from guppylang.std.quantum import measure, qubit
from guppylang.std.option import nothing


@guppy
def foo() -> None:
    opts = array(nothing() for _ in range(4))

    for q in opts:
        measure(q.unwrap())


foo.check()

Fails with

Error: Cannot infer type (at <In[2]>:8:17)
  | 
6 | @guppy
7 | def foo() -> None:
8 |     opts = array(nothing() for _ in range(4))
  |                  ^^^^^^^^^ Cannot infer type variables in expression of type
  |                            `Option[?T]`

Guppy compilation failed due to 1 previous error

Annotating with nothing[qubit]() fixes it.