In the context of constructive type theory, a term inhabiting some type is said to be in canonical form if it is explicitly built up using the constructors of that type.
Particularly, the only constructor of the identity type of $A$ is $\text{refl }: \Pi x. \text{id}_A \text{ } x \text{ } x$, so
Question 1: What is a canonical term of $\text{Id}_A(x,y)$ if $x$ is not jugdmentally identical to $y$?
Apparently there cannot be such a canonical term, for neither $\text{refl } x$ nor $\text{refl } y$ type check. Does this mean that the identity type of $A$ does not have a canonical form in general? That is, that $\text{Id}_A(x,y)$ only has a canonical form in the particular case where $x$ is judgmentally equal to $y$?
But in this case how propositional equality differs in practice from judgmental equality then – except for the fact that the former occurs as a type and the other as a judgment?
Question 2: What is a closed term of $\text{Id}_A(x,y)$? Are there two closed terms $p, q$ of $\text{Id}_A(x,y)$ such that $p$ and $q$ are not judgmental equal?