Enabling TypeHoles by default

[Mateusz Kowalczyk]

On 13/01/14 21:30, Daniil Frumin wrote:
> On ghc-dev Dominique Devriese has actually proposed changing TypeHoles
> to TypedHoles or to something similar, because "TypeHoles" sounds like
> you can have holes in types, just like in your example.
> 
> But what error message do you want to get if you have a hole in your
> type? GHC won't be able to tell you much
> 

Indeed I have seen the ghc-devs post. Using Hole instead of stating a
type is useful for me to me for two things:

* Causing type errors for type of the expression, for example to
specialise part of the signature and see what GHC infers for the rest of it

* Easily checking types of the expressions I'm working on inside of the
function. Sometimes one might lose track of types inside a larger
expression and it is useful to cause a type error with a hole on one of
the sub-expressions to see where we're at. GHCi doesn't provide a way to
check type of subexpressions, only top-level definitions so this is
particularly useful.

While the second problem can be mitigated in simple situations where we
have a single symbol expression such as

foo :: Integer -> Integer
foo x y = x + _y

the ‘_’ does not work for larger expressions. For example, the following

foo :: Integer -> Integer
foo x y = x + _(y + 3)

does not work as it actually gets translated to

foo :: Integer -. Integer
foo x y = x + _ (y + 3)

and rather than get the type of (y + 3), we get the type of the function
which takes that expression. Close but not quite. With _ for types I
could do

x + (y + 3 :: _)

as opposed to

data Hole
x + (y + 3 :: Hole)

It'd be great if I could spare myself defining Hole *and* get all the
information about bindings that _ provides.

-- 
Mateusz K.