Squash types correspond to judgmental truncation, not propositional truncation. In a type theory without a type for judgmental equality, there's non much of a way to make use of an inhabitant of a squash type; there's no way to write an eliminator into any type except another squash type. Relatedly, having squash types makes typechecking undecidable; having propositional truncation types does not result in this drawback.

Squash types correspond to judgmental truncation, not propositional truncation. In a type theory without a type for judgmental equality, there's non much of a way to make use of an inhabitant of a squash type; there's no way to write an eliminator into any type except another squash type. Relatedly, having squash types, as presented in the book you linked, makes typechecking undecidable; having propositional truncation types does not result in this drawback.

Why do squash types result in undecidable typechecking? Quoting the book you linked:

The first approach to representing the proposition is to consider the ‘squash’ type, defined in [C+86a] to be

$\|A\| ≡_{df} \{ t : \top\ \mid\ A \}$

which will be inhabited by the object $Triv$ if and only if there is some proof object $a : A$.

Now let $A$ be your favorite undecidable problem, and ask your typechecker to decide if $Triv$ has type $\|A\|$. By construction, it can't decide your problem, and thus can't typecheck $Triv : \|A\|$.

Note that this problem is specific to squash types with canonically named inhabitants. Agda has a form of judgmental truncation, which goes by the name "irrelevant arguments" or "irrelevant fields", without canonically named inhabitants. Agda maintains decidable typechecking, though I think it doesn't manage to throw away the proofs, and has to carry them around (perhaps only for technical implementation reasons). (This would be something to ask about on the Agda mailing list.) These suffer the drawback, mentioned above, of not being able to eliminate into any non-irrelevant types.