Holes in GHC

Andres Löh andres.loeh at googlemail.com
Sun Feb 12 14:55:40 CET 2012

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


More information about the Glasgow-haskell-users mailing list