
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.