Has anyone on here implemented typed holes for any system of any kind?
There is a Shen implementation for elisp, which might the task easier compared with other platforms that have Shen ports.
Is Shen's flexibility (I have the impression that Shen can be used to implement arbitray type systems -- but this may be wrong) an obstacle to implementation of typed holes when compared to something like Idris?
The existence of proof general (although I don't know enough to use it for anything non-trivial) makes me optimistic about this question.
You were maybe too optimistic about this question. Nobody ever answered and it's kind of sad.
I've never tried Shen. Mark Tarver is the author of The Bipolar Lisp Programmer http://www.marktarver.com/bipolar.html