Ерунда "не в поле зрения" ошибки

Question

Иногда Агда выдает мне бессмысленные ошибки «Не в рамках», оставляя меня не знающим, что делать. Вот пример:

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))

Агда говорит, что true, не находится в области видимости; обратите внимание на ,. Странно, но часто полезно, что Agda рассматривает большинство последовательностей символов без пробелов как одиночные токены.