Typed holes `(??)` like Merlin with OCaml

[dc-mak]

It does work, but two issues:

1. [Error] Unbound value ?? - maybe use a different message (e.g. Warning/Error: Unimplemented hole)
2. refmt incorrectly formats it like this

Typed-holes are ridiculously useful for statically-typed programming (Agda, Idris) - would be great to shine some light on this feature - instead of/as well as gradually buildng types, we can gradually build terms :-)

[d4hines]

I would love to see this kind of feature. For inspiration, definitely check out https://hazel.org/, which contributes the idea that there can be a well-defined semantic for incomplete programs both at type checking (inferring the type of the hole), and at runtime (i.e incomplete programs can still run! But they give incomplete results).