Holes in GHC

Andres Löh andres.loeh at googlemail.com
Mon Feb 13 09:35:08 CET 2012

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.


More information about the Glasgow-haskell-users mailing list