Typed holes are quite a different thing than deferred type errors. Does Agda actually have something like the latter? (Results seem negative from the tiny bit of searching I've just done, but that's awfully low confidence...)