A typed hole can have any type (it imposes no typing constraints on
the context around it), and its subterms can have any type (the hole
imposes no constraint on them).

This is the ultimate language construct to do type-preserving
shrinking. When shrinking it is important to be able to remove
subterms that do not participate to the error. Holes with no subterms
can be used to completely erase a term, as implemented in this
commeit.

Holes with subterms can be used to selectively erase parts of
a term (for example, the application "t u" can be rewritten into the
hole "...[t, u]", erasing only the application rule), but this is not
implemented yet in the present commit.