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

Page last modified on July 11, 2007, at 10:27 PM

Powered by
PmWiki