In dependent types, Type : Type results in inconsistency (Girard's or Hurken's paradox).
Are there examples of universe inconsistency (where assuming Type : Type would result something that is false) showing up "accidentally" when not deliberately trying to prove it (when proving unrelated things)?
This is a hard question to answer, in part because it's unclear what it means to get something "by accident". Regularly, though, people run into the Universe Inconsistency error of Coq, as some quick googling will show (e.g. here). This certainly sometimes happens by accident, sometimes in the attempt at showing inconsistencies or testing the limits of the prover.
One of the big sources of universe inconsistencies unsurprisingly comes from trying to formalize category theory in Coq, as is mentioned in this article by Gross, Chlipala and Spivak.
In most cases, it's hard to tell whether the inconsistency comes from an actually inconsistent statement, or just a limitation of the proof checker, which sometimes has counter-intuitive restrictions on universes, particularly in the allowed parameters for inductive types. This is actually a somewhat tricky subject (see the official definition and Chlipala's more accessible discussion).
