Dependent types prevent infinite loops at compile time because if you have nonterminating terms, your types are unsound as a logic (you can derive true and false properties altogether)

That's because theorem proving with dependent types is based on the idea that you can prove something by providing a proof object that is a witness that what you want to prove is true. But a nonterminating function can fake it: you can write a function that promises a proof that something is true, while it never returns (so it never has to build a proof object). That way you can prove that false things are "true".