无意义的“不在范围内”错误

Question

有时 Agda 会给我一些无意义的“不在范围内”错误，让我不知道该怎么做。下面是一个例子：

open import Data.Product
open import Data.Bool
open import Data.Unit

postulate
  ?    : (Set ? Set) ? Set
  In   : {F : Set ? Set} ? F (? F) ? ? F
  unIn : {F : Set ? Set} ? ? F ? F (? F)

NatT : Set
NatT = ? ? x -> ? Bool (? { true -> ?; false -> x })

x : NatT
x = In (false , In (true, tt))

这个抱怨true不在范围内。考虑到x = In (true, tt)工作正常，这更奇怪。为什么会发生这种情况？

Not in scope:
  true, at /Users/v/agda/mu.agda:14,21-26
    (did you mean
       'Bool.true' or
       'Data.Bool.Bool.true' or
       'Data.Bool.true' or
       'true'?)
when scope checking true,

Answer 1

缺少空格。正确：

x = In (false , In (true , tt))

Agda 说不true,在范围内；请注意,. Agda 将大多数无空格字符序列视为单个标记，这很奇怪，但通常很有用。