  In some sense, we have a non-wellfounded definition, which is as problematic as a contradiction (a proposition equivalent to its negation). One important theorem, the normalisation theorem, says that this cannot happen with simple types: if we have \(M:A\) then \(M\) is normalisable in a strong way (any sequence of reductions starting from \(M\) terminates).