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 _______________________________________________ Glasgow-haskell-users mailing list [email protected] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
