Are there problems without efficient algorithms, where existence theorems have proved such algorithms must exist?
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.