"Found hole"

Edward Kmett ekmett at gmail.com
Tue Jan 20 23:49:08 UTC 2015

FWIW- you can think of a 'hole' as a "not in scope" error with a ton of
useful information about the type such a term would have to have in order
to go in the location you referenced it.

This promotes a very useful style of type-driven development that is common
in Agda, where you write out your program and then leave holes that start
with _'s to fill in later.

Since no new programs are accepted or rejected, GHC turned on "holes"
support by default. Users have historically faked this style with
ImplicitParams by labeling their holes ?foo, but that approach doesn't give
any information on what local stuff could be used to plug the hole.

The only thing that changed is the nature of the error message, which
carefully track what variables are in scope, how they are instantiated, and
what type the missing term is used at.

Since libraries like lens were already making heavy use of the _'d
namespace this only happens if the name isn't already in use. This is why
you can define _'d things just fine. The main thing that happened is if you
typo the name of a lens, well, your error messages got even worse. ;)


On Tue, Jan 20, 2015 at 1:36 PM, Volker Wysk <verteiler at volker-wysk.de>

> Hello!
> What is a "hole"?
> This program fails to compile:
> main = _exit 0
> I get this error message:
> ex.hs:1:8:
>     Found hole ‘_exit’ with type: t
>     Where: ‘t’ is a rigid type variable bound by
>                the inferred type of main :: t at ex.hs:1:1
>     Relevant bindings include main :: t (bound at ex.hs:1:1)
>     In the expression: _exit
>     In an equation for ‘main’: main = _exit
> When I replace "_exit" with "foo", it produces a "not in scope" error, as
> expected. What is special about "_exit"? It doesn't occur in the Haskell
> Hierarchical Libraries.
> Bye
> Volker
> _______________________________________________
> 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/20150120/f97ffe34/attachment.html>

More information about the Glasgow-haskell-users mailing list