Holes in GHC

[Andres Löh]

Hi Brent.

>> 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).

You are right, and I want to apologize if I sounded overly negative. I
think I was a bit disappointed to see the feature being sold as "Agda
goals" where in fact a major aspect of Agda goals wasn't even being
discussed. I agree now, however, that adding the feature in a limited
form is still quite useful.

Cheers,
  Andres