Typed holes are a feature of GHC that allows special placeholders written with
a leading underscore (e.g., "
_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
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
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.