Is there a known example of a set $S$ of Diophantine equations such that
- $S$ is computable;
- it is a theorem that every equation in $S$ has (at most) finitely many solutions;
- the function that maps an element of $S$ to its set of solutions is uncomputable?
There are some famous finiteness theorems in number theory whose proofs are ineffective; e.g., Faltings's theorem that a curve of genus at least 2 has at most finitely many rational points, but in the examples I can think of, there is no proof that an algorithm does not exist—we just don't know of one.
By the way, although I said "Diophantine equations"—implying integer solutions—I'd be satisfied with an example where we're considering solutions in some other ring with a countably infinite number of elements (e.g., $\mathbb{Q}$).