What happens if we try to extract a witness but it actually does not exist from a term of existential type?
Any value. It depends upon which $t$ you are given. A term of type $\exists y.(\neg(0 = 0) \Rightarrow 0 = S(y))$ is a pair of an int $y$ and a function that takes a proof of $\neg(0=0)$ and gives you a proof of $0 = S(y)$. You can use a term of type $\neg(0 = 0)$ and type $0 = 0$ (from reflexivity) to derive a term of any type you want. This includes a term of type $0 = S(0)$, $0 = S(1)$, $\ldots$. So, you can make $y$ any integer you want.