事实上，存在编译错误。这agda可执行文件发现错误并将该信息传递给agda-mode在 Emacs 中，它会进行语法突出显示，让您知道存在错误。我们可以看看如果我们使用会发生什么agda直接地。这是我正在使用的文件：
module C1 where
open import Data.Nat
loop : ℕ → ℕ
loop 0 = 0
loop x = loop x
现在，我们调用agda -i../lib-0.7/src -i. C1.agda（不要介意-i参数，它们只是让可执行文件知道在哪里寻找标准库），我们得到错误：
Termination checking failed for the following functions:
loop
Problematic calls:
loop x
(at D:\Agda\tc\C1.agda:7,10-14)
这确实是编译错误。此类错误使我们无法import从其他模块中获取此模块或编译它。例如，如果我们将这些行添加到上面的文件中：
open import IO
main = run (putStrLn "")
并使用编译模块C-c C-x C-c, agda-mode抱怨：
You can only compile modules without unsolved metavariables
or termination checking problems.
其他类型的编译错误包括类型检查问题：
module C2 where
open import Data.Bool
open import Data.Nat
type-error : ℕ → Bool
type-error n = n
__________________________
D:\Agda\tc\C2.agda:7,16-17
ℕ !=< Bool of type Set
when checking that the expression n has type Bool
阳性检查失败：
module C3 where
data Positivity : Set where
bad : (Positivity → Positivity) → Positivity
__________________________
D:\Agda\tc\C3.agda:3,6-16
Positivity is not strictly positive, because it occurs to the left
of an arrow in the type of the constructor bad in the definition of
Positivity.
或未解决的元变量：
module C4 where
open import Data.Nat
meta : ∀ {a} → ℕ
meta = 0
__________________________
Unsolved metas at the following locations:
D:\Agda\tc\C4.agda:5,11-12
现在，您正确地注意到有些错误是“死胡同”，而其他错误则让您继续编写程序。这是因为有些错误比其他错误更严重。例如，如果您得到未解决的元变量，很可能您只需填写缺失的信息即可，一切都会好起来的。
至于挂起编译器：检查或编译模块不应导致agda循环。让我们尝试强制类型检查器循环。我们将在模块中添加更多内容C1:
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
refl : x ≡ x
test : loop 1 ≡ 1
test = refl
现在，检查一下refl是该类型的正确表达，agda必须评估loop 1。然而，由于终止检查失败，agda不会展开loop（并最终陷入无限循环）。
然而，C-c C-n真正的力量agda尝试评估表达式（你基本上告诉它“我知道我在做什么”），所以很自然地你会进入无限循环。
顺便说一句，你可以使agda如果禁用终止检查，则循环：
{-# NO_TERMINATION_CHECK #-}
loop : ℕ → ℕ
loop 0 = 0
loop x = loop x
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
refl : x ≡ x
test : loop 1 ≡ 1
test = refl
最终结果是：
stack overflow
经验法则：如果你能做到agda通过检查（或编译）模块而不使用任何编译器编译指示来循环，那么这确实是一个错误，应该在错误跟踪器。话虽这么说，如果您愿意使用编译器编译指示，则有几种方法可以制作非终止程序。我们已经看到了{-# NO_TERMINATION_CHECK #-}，这里还有一些其他方法：
{-# OPTIONS --no-positivity-check #-}
module Boom where
data Bad (A : Set) : Set where
bad : (Bad A → A) → Bad A
unBad : {A : Set} → Bad A → Bad A → A
unBad (bad f) = f
fix : {A : Set} → (A → A) → A
fix f = (λ x → f (unBad x x)) (bad λ x → f (unBad x x))
loop : {A : Set} → A
loop = fix λ x → x
这个依赖于一种不严格为正的数据类型。或者我们可以强制agda接受Set : Set（也就是说，类型Set is Set本身）并重建罗素悖论:
{-# OPTIONS --type-in-type #-}
module Boom where
open import Data.Empty
open import Data.Product
open import Relation.Binary.PropositionalEquality
data M : Set where
m : (I : Set) → (I → M) → M
_∈_ : M → M → Set
a ∈ m I f = Σ I λ i → a ≡ f i
_∉_ : M → M → Set
a ∉ b = (a ∈ b) → ⊥
-- Set of all sets that are not members of themselves.
R : M
R = m (Σ M λ a → a ∉ a) proj₁
-- If a set belongs to R, it does not contain itself.
lem₁ : ∀ {X} → X ∈ R → X ∉ X
lem₁ ((Y , Y∉Y) , refl) = Y∉Y
-- If a set does not contain itself, then it is in R.
lem₂ : ∀ {X} → X ∉ X → X ∈ R
lem₂ X∉X = (_ , X∉X) , refl
-- R does not contain itself.
lem₃ : R ∉ R
lem₃ R∈R = lem₁ R∈R R∈R
-- But R also contains itself - a paradox.
lem₄ : R ∈ R
lem₄ = lem₂ lem₃
loop : {A : Set} → A
loop = ⊥-elim (lem₃ lem₄)
(source）。我们还可以写出吉拉德悖论的一个变体，由 A.J.C. Hurkens 简化:
{-# OPTIONS --type-in-type #-}
module Boom where
⊥ = ∀ p → p
¬_ = λ A → A → ⊥
℘_ = λ A → A → Set
℘℘_ = λ A → ℘ ℘ A
U = (X : Set) → (℘℘ X → X) → ℘℘ X
τ : ℘℘ U → U
τ t = λ (X : Set) (f : ℘℘ X → X) (p : ℘ X) → t λ (x : U) → p (f (x X f))
σ : U → ℘℘ U
σ s = s U λ (t : ℘℘ U) → τ t
τσ : U → U
τσ x = τ (σ x)
Δ = λ (y : U) → ¬ (∀ (p : ℘ U) → σ y p → p (τσ y))
Ω = τ λ (p : ℘ U) → ∀ (x : U) → σ x p → p x
loop : (A : Set) → A
loop = (λ (₀ : ∀ (p : ℘ U) → (∀ (x : U) → σ x p → p x) → p Ω) →
(₀ Δ λ (x : U) (₂ : σ x Δ) (₃ : ∀ (p : ℘ U) → σ x p → p (τσ x)) →
(₃ Δ ₂ λ (p : ℘ U) → (₃ λ (y : U) → p (τσ y)))) λ (p : ℘ U) →
₀ λ (y : U) → p (τσ y)) λ (p : ℘ U) (₁ : ∀ (x : U) → σ x p → p x) →
₁ Ω λ (x : U) → ₁ (τσ x)
不过，这确实是一团糟。但它有一个很好的特性，即它只使用依赖函数。奇怪的是，它甚至没有通过类型检查并导致agda循环。分割整体loop术语一分为二有帮助。
