Remove more holes automatically

[brprice]

We don't (even after hackworthltd/vonnegut#175) remove holes such as
{? Succ ?} Zero
because we don't have enough information to see if the hole is "finishable" at the point we handle the hole. In general, if a hole is in a synthesis position, we don't know where else downstream it is being referred to, so we dare not change its type.

I don't know how to do better here!

I also don't know how common this situation is in practice, so have no idea if this should be high priority or not.

[brprice]

One approach is to remove the hole regardless, and then make downstream insert holes if they break. Consider
{? 1 ?} True which would stay as it is: we remove the hole when considering synthesising a type for it, but then when considering the App node, we re-add the hole as we need an arrow type. Now consider {? ? :: Nat -> Nat ?} True which would change to (? :: Nat -> Nat) {? True ?} as we remove the hole but then we require that Nat \ni True, which is false so we add a hole there. This "jumping holes" seems like bad UX to me.

[dhess]

What's the status of this issue wrt the new smart holes implementation?

[brprice]

What's the status of this issue wrt the new smart holes implementation?

Essentially unchanged. We attempt to remove holes, but the implementation is somewhat ad-hoc and should be improved to both be more general and more intuitive.

Some particular issues we currently have

• the "change this empty hole into a non-empty hole" ? ~> {? ? ?} action is broken, since we automatically elide this non-empty hole again
• some "obviously pointless" hole/annotations are not elided, e.g. foo : ∀a:*.? ; foo = {? ? : ∀a:*.? ?} where we have "the same annotation" twice

However, I still don't know how to remove all(/most) "pointless" things whilst not making it awkward to intentionally create something like foo : Bool ; foo = {? ? : Int ?}, which can be useful when trying to work out how to complete your program. To create this one probably wants to go via foo : Bool ; foo = {? ? : ? ?}, which is a "pointless" hole/annotation.

Perhaps we need to rethink the decision to operate only on the AST, and instead track whether holes were automatically created?

[georgefst]

It would be great if we could reach a point where the manual FinishHole action is never actually necessary. I figured this should be possible, since a naive implementation would just be to perform a post-TC pass of auto-applying the action wherever it's available.

However, while tring to work out exactly when the action is offered in the first place (the Succ example in OP is invalid now with saturated-constructors), I've just noticed that we sometimes offer it in expressions where it has no effect, e.g. {? singleton @_ _ ?} : Bool where singleton : ∀a. a -> List a. This seems odd.

[brprice]

It would be great if we could reach a point where the manual FinishHole action is never actually necessary. I figured this should be possible, since a naive implementation would just be to perform a post-TC pass of auto-applying the action wherever it's available.

I agree (modulo one concern). The issue here is how to do it efficiently, and potentially how to choose which subset of holes to finish if there are conflicts (I haven't thought about whether this is possible).

My one concern here is that there may be holes that the student wants to keep around for some reason -- perhaps it contains a type-correct term but it is semantically wrong. This however is somewhat orthogonal, and maybe should be dealt with by adding a flag on holes "student-defined"/"automatically-created".

However, while tring to work out exactly when the action is offered in the first place (the Succ example in OP is invalid now with saturated-constructors), I've just noticed that we sometimes offer it in expressions where it has no effect, e.g. {? singleton @_ _ ?} : Bool where singleton : ∀a. a -> List a. This seems odd.

Yes, we simply offer it at any hole. I have not thought about how to detect whether it is a sensible action efficiently.