Nonsense "Not in scope" errors

user_1031791 0
Viewed 1011

Sometimes Agda gives me nonsense "Not in scope" errors, leaving me not knowing what to do. Here is an example:

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

This one complains true is not in scope. This is even weirder considering x = In (true, tt) works fine. Why this happens?

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,
agda
1 Answers

A whitespace is missing. Correctly:

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

Agda says true, is not in scope; note the ,. It's weird, but often useful, that Agda considers most space-free character sequences as single tokens.

user_10682320
Related