Holes in GHC

[Brent Yorgey]

On Sun, Feb 12, 2012 at 02:55:40PM +0100, Andres Löh 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.

Being able to see the available context is indeed a big advantage, but
even just seeing the type of the hole is really helpful -- I would
certainly use this feature if it were available in Haskell.  And we
have to start somewhere, don't we?  There is certainly no reason we
can't later *add* ways of extracting information about the context of
a hole.

> as others have indicated, it can relatively easily be simulated
> already.

I don't think this is true.  The wiki page includes a discussion of
the current methods for "simulating" holes and their (substantial)
disadvantages.  In order to be useful it seems to me that it must be
possible to

  (1) obtain the inferred type of a hole
  (2) while still allowing the enclosing module to type check.

As far as I know, none of the existing solutions satisfy (2).

-Brent