Holes in GHC

[Edward Kmett]

Not sure if I misparsed your response or not.

Its not just things that can or could match the type of the scope, but
basically anything introduced in local scopes around the hole, those can
have types that you can't talk about outside of a local context, due to
existentials that were opened, etc.

The usual agda idiom is to make the hole, then check to see what is
available that you can use to build towards filling it in, but those
locally introduced things may not have anything in common with the type of
the hole.

-Edward

On Mon, Feb 13, 2012 at 4:09 AM, Thijs Alkemade <thijsalkemade at gmail.com>wrote:

> 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
>
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20120218/b318bb1c/attachment.htm>