20070711-1

The following definition type checks:

module MutualScopeBug where

-- mutual
  data Nat : Set where
    z : Nat
    s : Nat -> Nat

  data Nat' : Nat -> Set where
    z' : Nat' z
    s' : forall {n} -> Nat' n -> Nat' (s n)

  test : Nat' z -> Nat' z
  test z' = z'

However if I uncomment mutual then I get the following error message:

Not in scope:
  z at /Users/jmc/MutualScopeBug.agda:12,15-16
when scope checking Nat' z

This is because constructors are not in scope in type signatures in the mutual block in which they are defined. The workaround is to define a synonym:

 module MutualScopeBug where

 mutual
   data Nat : Set where
     z : Nat
     s : Nat -> Nat

   data Nat' : Nat -> Set where
     z' : Nat' z
     s' : forall {n} -> Nat' n -> Nat' (s n)

   z1 : Nat
   z1 = z

   test : Nat' z1 -> Nat' z1
   test z' = z'

I think that the reason for not having the constructors in scope is to allow mentioning functions defined further down in the mutual block (such as test) in the type signatures of the constructors. You would get a problem if z mentioned test in its type and test also mentioned z, for instance. Having to define a synonym is awkward, though, and I would prefer a more convenient way to handle this situation. I suggest that you add a feature request. /NAD