Re: Holes in GHC

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