The usual proof that $K[X]$ is a PID goes by finding $p\in I$ of the lowest degree for a non-zero ideal $I$ of $K[X]$. Constructively, this amounts to testing $p\in I$ for all $p$ of degree $0$, then for all $p$ of degree $1$, and so on.
If $K$ is infinite, the set of all polynomials of a fixed degree $n\geq 0$ is infinite, so we can't just test them all. I suppose enumerating all elements of $K[X]$ won't help either.
Surely, since $I$ is constructively non-zero, it contains a non-zero $q$, and we can factorize $q$ into irreducibles, and find $p$ among them such that $p\in I$. While this proves that $p$ is an irreducible member of $I$, this doesn't prove that $p$ is a lowest degree member of $I$.
Is there a constructive proof that $K[X]$ is a PID?
I'm specifically interested in the following ideal. Let $K\subseteq L$ be an extension of fields, let $\alpha\in L$, and $I := \{p \mid p\in K[X]; p(\alpha)=0\}$. Then $I$ is an ideal. I guess that a proof would depend on how $L$ is described. I heard there are constructive encodings of algebraic numbers. Can they help here?