7.14. Typed Holes

Typed holes are a feature of GHC that allows special placeholders written with a leading underscore (e.g., "_", "_foo", "_bar"), to be used as expressions. During compilation these holes will generate an error message that describes which type is expected at the hole's location, information about the origin of any free type variables, and a list of local bindings that might help fill the hole with actual code. Typed holes are always enabled in GHC.

The goal of typed holes is to help with writing Haskell code rather than to change the type system. Typed holes can be used to obtain extra information from the type checker, which might otherwise be hard to get. Normally, using GHCi, users can inspect the (inferred) type signatures of all top-level bindings. However, this method is less convenient with terms that are not defined on top-level or inside complex expressions. Holes allow the user to check the type of the term they are about to write.

To run and test a piece of code containing holes, use the -fdefer-typed-holes flag. This flag defers errors produced by typed holes and converts them into warnings. The result is that typed hole errors are converted into warnings (controlled by -fwarn-typed-holes). The result is that a hole will behave like undefined, but with the added benefits that it shows a warning at compile time and will show another warning message if it gets evaluated. This behaviour follows that of the -fdefer-type-errors option, which implies -fdefer-typed-holes. See Section 7.16, “Deferring type errors to runtime”.

For example, compiling the following module with GHC:

f :: a -> a
f x = _

will fail with the following error:

hole.hs:2:7:
    Found hole `_' with type: a
    Where: `a' is a rigid type variable bound by
               the type signature for f :: a -> a at hole.hs:1:6
    Relevant bindings include
      f :: a -> a (bound at hole.hs:2:1)
      x :: a (bound at hole.hs:2:3)
    In the expression: _
    In an equation for `f': f x = _

Multiple typed holes can be used to find common type variables between expressions. For example:

sum :: [Int] -> Int
sum xs = foldr _f _z xs

Shows:

holes.hs:2:15:
    Found hole `_f' with type: Int -> Int -> Int
    In the first argument of `foldr', namely `_'
    In the expression: foldr _a _b _c
    In an equation for `sum': sum x = foldr _a _b _c

holes.hs:2:17:
    Found hole `_z' with type: Int
    In the second argument of `foldr', namely `_'
    In the expression: foldr _a _b _c
    In an equation for `sum': sum x = foldr _a _b _c

Unbound identifiers with the same name are never unified, even within the same function, but always printed individually. For example:

cons = _x : _x

results in the following errors:

unbound.hs:1:8:
    Found hole '_x' with type: a
    Where: `a' is a rigid type variable bound by
               the inferred type of cons :: [a] at unbound.hs:1:1
    Relevant bindings include cons :: [a] (bound at unbound.hs:1:1)
    In the first argument of `(:)', namely `_x'
    In the expression: _x : _x
    In an equation for `cons': cons = _x : _x

unbound.hs:1:13:
    Found hole '_x' with type: [a]
    Arising from: an undeclared identifier `_x' at unbound.hs:1:13-14
    Where: `a' is a rigid type variable bound by
               the inferred type of cons :: [a] at unbound.hs:1:1
    Relevant bindings include cons :: [a] (bound at unbound.hs:1:1)
    In the second argument of `(:)', namely `_x'
    In the expression: _x : _x
    In an equation for `cons': cons = _x : _x

This ensures that an unbound identifier is never reported with a too polymorphic type, like forall a. a, when used multiple times for types that can not be unified.