typed holes (with subterms) for shrinking

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. 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).

The MR also contains some independent improvements to the shrinking strategy; in particular convenient shrinking for products, which I hope to possibly upstream in QCheck directly.

cc @omartino, @fpottier. This is something that I discussed with @omartino (I didn't know when we could implement it), and I would be interested in a high-level opinion from François; in particular I think the (hinted) relation to typed error slicing may be interesting.

(I think that the relation is that we may be computing a minimal slice while shrinking (I'm not sure how to check it), but in an inefficient way as we retype each new term completely from scratch. It is completely fine in practice. I don't know how to do this more incrementally if we wanted to, given that we shrink terms starting from the leaves, instead of typing a partial term that gets more and more complete. Maybe we should try to complete a partial tree from the root to the leaves...)

changed the description

For a concrete example of improved shrinking, I injected a bug in the application rule. Before this MR, our shrinked counter-example is

fun x0 ->
  fun x1 -> x0 (let (x2, x3) = x1 in fun x4 -> (fun x5 -> x3) x3)

with typed holes (and some improvements to shrinking)

...[] (fun x5 -> ...[])

where ...[] is the syntax for holes without subterms.

This looks good to me. I am not sure about the relation with minimal type error slicing. Does "minimal type error slicing" mean "keep only the constraints that participate in an error", or does it mean "keep only the AST nodes that participate in an error", or something else?

There is an explicit connection between these two notions in Haack and Wells paper ("Type error slicing in implicitly typed higher-order languages", 2004): from a set-of-locations obtained from a minimal-set-of-constraints, they show how to determine a program-with-holes that is ill-typed, and minimal in the sense that any programs with more holes is well-typed.

(For the record: Olivier and myself thought of introducing typed holes (without subterms/arguments) during a discussion about shrinking. When I asked around if holes had been used for shrinking before, Neelakantan Krishnaswami pointed to their use in the Haack and Wells. This inspired me to add subterm arguments to our holes as well.)

mentioned in commit e6953c62

merged