Holes in GHC

[Andres Löh]

Hi Thijs.

Sorry if this has been discussed before.

In my opinion, the main advantage of Agda goals is not that the type
of the hole itself is shown, but that you get information about all
the locally defined identifiers and their types in the context of the
hole. Your page doesn't seem to discuss this at all. Without that
extra info, I don't see much purpose in the feature, though, because
as others have indicated, it can relatively easily be simulated
already.

Cheers,
  Andres