Holes in GHC

[Thijs Alkemade]

On Sun, Feb 12, 2012 at 2:55 PM, Andres Löh <andres.loeh at googlemail.com> wrote:
> 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

Hi Andres,

Thanks for your feedback. Showing everything in scope that matches or
can match the type of a hole is certainly something I am interested
in, but I'm afraid it's out of the scope of this project. I think
finding the types of the holes is a good first step that should make
this feature easier to implement later.

Best regards,
Thijs Alkemade