Idris 支持 General Recursion，那它的 typechecking 會不會死循環？

眾所周知在 CoC 的框架體系內，Type 和 Term 完全等同，因而 typechecking 的關鍵步驟——Unification——需要真的去展開某些 Term。如果不限制遞歸的話就可能會導致 typechecking 不終止。

那 Idris 對於它是怎麼處理的？

當然可以死循環。total functional programming 語言的 termination checker 都是基於非常 naive 的語法特徵去匹配的（Idris 的文檔太缺了，參考 Agda wiki 上的說法：http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Totality），但並不是所有 total 的函數都滿足 primitive/structural recursion 的語法特徵。

所以無論 Agda 和 Idris 都提供了「大爺我覺得這函數 total，編譯器給我閉嘴」的功能。Agda 有個 TERMINATING pragma（見Termination Checking），Idris 有個 assert_total 函數（見Theorem Proving - Idris 0.99 documentation）。你用這功能堵上編譯器的嘴，寫個 diverging 的函數，讓類型檢查器空轉是完全 ok 的。

有可選的 totality checker，如果檢查不過的話，在類型檢查的時候是不會規約的

non-total definitions aren』t reduced when type checking because they are not well-defined for all possible inputs.

在 Types and Functions 最底下

01 類型檢測不會死循環，這是在語言類型系統設計之初就設定好的，你要了解詳具體情況可以看一下直覺主義類型系統（覺得會死循環不妨舉個例子）。但是類型推導有可能。具體到idris，當然也不會陷入死循環，但類型標註不明時它會提示讓你明確標註類型

02 General Recursion 和你問的問題沒關係呀，幾乎所有流行的fp語言都是General Recursion，類型檢測的演算法和性質與限定total的是一樣的