I am confused by certain constructions regarding fundamental groups. The word problem for finitely presented groups is known to be undecidable. However, it is also known how to construct, given a finitely-presented group, a finite simplicial complex (of dimension 2) with that group as its $\pi_1$. Given two words in the finitely-presented group, they correspond to two loops $l_1, l_2$ in the complex, and we can check whether their composition $l_2^{-1}\circ l_1$ is the zero loop by simply checking whether it lifts to a closed path in the universal cover of the complex.
Now, it is true that the universal cover will not in general be a finite complex, but this is not a problem since you can simply construct enough patches of the universal cover until you get to the endpoint of the loop $l_2^{-1}\circ l_1$, and check whether that endpoint is the same as the point you started from. That is, if the loop $l_2^{-1}\circ l_1$ is given by a finite sequence of edges in the complex, then go along the edges in order and construct patches from the universal cover one by one, until you get to the final edge of $l_2^{-1}\circ l_1$, and check the endpoint. What is the problem with this argument?