現在我們關心一下第二個例子 loop（修改自 Certified Programming with Dependent Types）：
data Term abs : (Term → Term) → Term app : Term → Term → Term app (abs f) t = f t w : Term w = abs (λ x → app x x) loop : Term loop = app w w
loop 的計算永遠都不會結束，然而證明器用到的 dependent type theory 卻允許型別依賴 loop 這樣的值，因此就能寫出讓 type checker 無法停止的程式。換句話說，證明器仰賴的性質缺失。事實上 Term 跟 Bad 的問題就是違反了 strictly positive 的性質，或許也有人已經發現了兩者 constructor 型別的相似之處。接下來我們來看為什麼這樣的定義會製造出不一致邏輯。