Hi Brent.
as others have indicated, it can relatively easily be simulated already.
I don't think this is true. The wiki page includes a discussion of the current methods for "simulating" holes and their (substantial) disadvantages. In order to be useful it seems to me that it must be possible to
(1) obtain the inferred type of a hole (2) while still allowing the enclosing module to type check.
As far as I know, none of the existing solutions satisfy (2).
You are right, and I want to apologize if I sounded overly negative. I think I was a bit disappointed to see the feature being sold as "Agda goals" where in fact a major aspect of Agda goals wasn't even being discussed. I agree now, however, that adding the feature in a limited form is still quite useful. Cheers, Andres