Typed holes

A subsection under Values, types and signatures: _ where the code is not
written yet, what the compiler says about it, and a _name as a named hole.

🤖 Generated with [ECA](https://eca.dev)

Co-Authored-By: eca-agent <git@eca.dev>

_01.Language-basics.sz

@@ -164,6 +164,27 @@ Everything at the toplevel needs a signature, even values. In a function body, n
 
 The example above is of course facile, but it matters more for generic functions with inlined traits. They are pinned to the first use, and any subsequent usage will raise an error. More on this in the trait section.
 
+@subsubsection{Typed holes}
+
+When you don't know what to write somewhere, write @code{_} there. That is a typed hole (not to be confused with the holes of string interpolation). A program with a typed hole does not compile. Instead the compiler tells you what type is wanted at that spot, and which bindings in scope have that type:
+
+@codeblock[#:lang "bjolang"]{
+(: lengths (-> (Vec string) (Vec int)))
+(defun (lengths names)
+  (vec-map _ names))
+}
+
+@codeblock[#:lang "text"]|{
+Hole at lengths.bjo:3:12: '_' stands for a value of type (-?-> string int).
+  Bindings in scope that fit: string-count, unhashable, count, eq-hash, length, structural-hash, and 2 more.
+}|
+
+@code{-?->} is a function that may or may not suspend, which is what @code{vec-map} accepts. More on that under Concurrency.
+
+The bindings closest to the hole are listed first: locals, then your own module's, then imported ones. A binding with a where clause is only listed if the clause holds. A name that starts with an underscore, like @code{_total}, is a hole too as long as nothing binds it, which is handy when you have several. If nothing around the hole decides its type, you get a @code{?a} and what it has to be able to do, like @code{(Displayed ?a)}. In the REPL, @code{(: _ string)} is a quick way to ask what in scope is a string.
+
+While a hole's type is still open, the other errors in the same definition are held back, since they are often caused by the hole. Once you fill it in, they show up.
+
 @subsubsection{Naming conventions}
 
 Bjolang follows scheme's naming conventiens. Predicates end with @code{?}. Mutating functions end with @code{!}. Conversions are written using @code{->}.