Well, Haskell got it from Agda [1], but Agda is even farther in the direction of Haskell than Haskell relative to mainstream programming languages, and beyond the "currently practical" language horizon.

[1]: https://wiki.haskell.org/GHC/Typed_holes

Typed holes are quite a different thing than deferred type errors. Does Agda actually have something like the latter? (Results seem negative from the tiny bit of searching I've just done, but that's awfully low confidence...)

Whoops, you're right! I was too hasty.

Eclipse does a similar thing with Java. It will replace methods that don't compile with a stub that throws an exception with the compilation error.

But is that transparent or they pollute the source code?

It's completely transparent, done only in the compiled class files. The signature of the method remains exactly the same, just the body is replaced.