Agda (2) has a similar feature called holes. Very similar to Haskell’s `nothing` and Scala’s `???`. The difference is that because of the dependently typedness the compiler can sometimes even fill in the code for you based on symbols in scope.
Haskell has also had typed holes for several major versions now. Any underscore or name beginning with an underscore (to include values and types, unsure about kinds) gets an informative error message describing the type of the name, e.g.:
Found hole `_' with type f (Free f b)
and relevant bindings, if applicable:
Relevant bindings include
>>= :: Free f a -> (a -> Free f b) -> Free f b
(bound at holes.hs:28:3)
f :: f (Free f a) (bound at holes.hs:29:8)
g :: a -> Free f b (bound at holes.hs:29:14)
In the first argument of `Free', namely `_'
Very useful for working your way out of a situation where the specific incantation to get to the right type isn't obvious.
