For contractibility defined as $\text{isContr}(A) :\equiv \Sigma_{a:A} \Pi_{x:A} (a=x)$,
(cf. page 124 of the HoTT book), the intuitive idea is that every point $x$ is the same point as $a$.
The way you are reading the definition is common, and says:
"there is an $a$ such that for each $x$ there is a path from $a$ to $x$"
I completely agree, this sounds like path-connected-ness. However we get this reading by mixing our interpretations of types. Here we forget the topological data in the $\Sigma$ and $\Pi$ types (by reducing them to mere quantifiers) but we remember the topological data in the identity type!
If you want to use the quantifier lingo, stick to it. Then the sentence says
"there is an $a$ such that for each $x$, $a=x$"
which DOES sound like contractibility.
Alternatively, if you want to use topological intuition, you have to remember what $\Sigma$ and $\Pi$ types mean -- there's a naturality condition in how we pick our paths. With path-connected-ness we can pick each path separately, however we need to. However, because of naturality, we are saying there is some uniform way to find a path from any point $x$ to $a$ -- that's exactly what it means to have a deformation retract to $a$.
In this interpretation, $\text{isContr}(A)$ is the type of pairs $(a,r)$ where $a$ is a point in $A$ and $r$ is a deformation retract to $a$, which also sounds like a good definition for contractibility.
There's a very good discussion of exactly this mistake (which everyone makes, by the way) here, as well as good background reading motivating why the definitions are what they are.
If a blind appeal to naturality isn't satisfying, by the way, I encourage you to actually prove the associated theorem. It isn't very difficult, and it's what finally convinced me that $\text{isContr}$ was correct:
If $(a,r) : \text{isContr}(A)$, then $r$ is (judgementally) equal to the type $\text{const}_a \sim \text{id}_A$. That is, $r$ witnesses the constant function at $a$ is homotopic to the identity function on $A$, and so it is actually a deformation retract, as claimed.
Hope this helped ^_^
Edit:
I realize I've left out part of your question, so let me try to remedy that now.
Why not take $\text{intuitiveContr}(A) = \Pi_{x:A} \Pi_{\alpha : x=x} (\alpha = \text{refl}_x)$ as a definition? Leaving aside the fact that it admits the empty type as contractible (which is easily fixed), what bad can really come of it?
The more pressing reason to not take $\text{intuitiveContr}(A)$ as a definition is that it doesn't capture contractibility. Instead, it captures the notion of Simply Connected (cf. this article).
$\text{intuitiveContr}$ insists that all loops can be contracted to refl, but it says nothing about higher homotopy. The 2-sphere, for instance, satisfies $\text{intuitiveContr}$, but is not contractible. Even though there is no 1-dimensional obstruction to contractibility (i.e. every loop contracts to a point), there is a 2-dimensional obstruction to contractibility (the sphere is not filled in with a ball). Unfortunately, $\text{intuitiveContr}(A)$ misses this.
Part of the magic of $\text{isContr}$ is that it avoids this problem. One can prove (using function extensionality) that $\text{isContr}(A) \to \text{isContr}(\text{isContr}(A))$, and using this we can inductively show that homotopy vanishes in all dimensions.
Said another way, it is an easy exercise to show that contractible types are equivalent to $\textbf{1}$, the singleton type (also on page 124 of the HoTT book), so it is the right definition.
Best Answer
I think the answer to your question (existentially reformulated) is "yes", but not for the reason you probably think. In fact as soon as you have $p_1:x=y$ and $p_2:p_1={\rm refl}$, it must be that $x\equiv y$. The reason is that equality is "homogeneous": it only makes sense to talk about whether $x=y$ once you know that $x$ and $y$ have the same type (hence why we sometimes write $x=_A y$). So in particular, it only makes sense to talk about $p_2:p_1={\rm refl}$ once you know that $p_1$ and ${\rm refl}$ have the same type. But $p_1$ has type $x=y$ and ${\rm refl}_x$ (say) has type $x=x$, while terms have unique types (modulo subtleties like subtyping and universe cumulativity) so it must be that the types $x=y$ and $x=x$ are (judgmentally) equal, $(x=y)\equiv (x=x)$. Finally, type constructors are (judgmentally) injective, so for instance $(a=b) \equiv (c=d)$ can only happen if $a\equiv c$ and $b\equiv d$; hence in this case we must have $y\equiv x$.
The reason I say that this is probably not what you're thinking about is that it's basically syntactic trickery, due to the way that the syntax is usually formulated and the fairly finicky properties (like unique types and injectivity of type formers) that it usually has. Moreover, these properties are "admissible" rather than "derivable", which means that the above argument is not a proof inside HoTT (or more precisely a "derivation"), rather it is a meta-argument about derivability: whenever you can derive $p_1:x=y$ and $p_2:p_1={\rm refl}$ it must also be the case that you can derive $x\equiv y$.
Here's an example that I think may be more along the lines you have in mind which shows that the answer to the question you probably meant to ask is "no". Suppose $A$ is a contractible type, so that for any $x,y:A$ we have $x=y$. In fact, if $A$ is contractible then the type $x=y$ is also contractible. Thus, for $x,y:A$ we have some $p_1:x=y$, and for any $q_1:x=y$ we have $p_2:p_1=q_1$; and for any $q_2:p_1=q_1$ we have $p_3:p_2=q_2$; and so on. But this doesn't imply $x\equiv y$. For instance, we could take $A = \sum_{b:S^1} (b={\rm base})$; then $A$ is contractible, but the two points $({\rm base},{\rm refl})$ and $({\rm base},{\rm loop})$ of $A$ are not judgmentally equal, since if they were then we would have ${\rm refl} \equiv {\rm loop}$ which cannot be true. (Note that any proof of "judgmental inequality" must also be a meta-argument that "judgmental equality is not derivable", since the formal system of type theory does not allow derivations of judgmental inequality.)