Are there problems without efficient algorithms, where existence theorems have proved such algorithms must exist? Are there problems in CS where no efficient algorithms are known, despite existence theorems proving such efficient algorithms must exist?

What are these problems called? Where can I find out more?
Sure, there are lots of examples, at least in the spirit of your question.

Often one gets such a result from the probabilistic method. For example, one paper that I like that runs into the problem is on reconstructing graphs in the additive model.  Here, the authors show that there exists a set of $O(dn)$ queries that will (optimally) learn the target graph.  Given this set, the algorithm is efficient.  However, they use the probabilistic method to show the existence of this small set (for each problem size) that will work on all inputs, but do not explicitly construct it.  So the best they can do is just a brute-force search through an exponential family of queries because they don't have an explicit construction.