Typed hole support is enabled with the option
-fwarn-typed-holes
, which is enabled by default.
The goal of the typed holes warning is not to change the type system, but to help with writing Haskell code. Type holes can be used to obtain extra information from the type checker, which might otherwise be hard to get. Normally, the type checker is used to decide if a module is well typed or not. Using GHCi, users can inspect the (inferred) type signatures of all top-level bindings. However, determining the type of a single term is still hard. Yet while writing code, it could be helpful to know the type of the term you're about to write.
This extension allows special placeholders, written with a leading underscore (e.g. "_
",
"_foo
", "_bar
"), to be used as an expression.
During compilation these holes will generate an error message describing what type is expected there,
information about the origin of any free type variables, and a list of local bindings
that might help fill the hole with actual code.
Holes work together well with deferring type errors to runtime:
with -fdefer-type-errors
, the error from a hole is also deferred, effctively making the hole
typecheck just like undefined
, but with the added benefit that it will show its warning message
if it gets evaluated. This way, other parts of the code can still be executed and tested.
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 type holes can be used to find common type variables between expressions. For example:
sum :: [Int] -> Int sum xx = 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 Failed, modules loaded: none.
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.