[Agda] Changing import lists turns constructors into variables

[Nils Anders Danielsson]

Hi,

Consider the following module:

 module M where
 open import A -- Brings A, a₁ and a₂ into scope.
 open import B -- Brings B, b₁ and b₂ into scope.

 f : A → B
 f a₁ = b₁
 f a₂ = b₂

Assume now that someone adds a definition B to module A. This makes the
type signature of g ambiguous. One can fix this by changing the import
statements in M. By just adding minimal import lists one can be lead to
believe that the following fix is correct:

 module M′ where
 open import A using (A)
 open import B using (B; b₁; b₂)

 f : A → B
 f a₁ = b₁
 f a₂ = b₂

However, while the code in M′ type checks, it is not equivalent to the
one in M, because a₁ and a₂ are now treated as variables (the
constructors are not in scope).

When Ulf and I discussed the lexical syntax of Agda the possibility of
this problem was raised, but we never did anything about it. However, I
was recently bitten by this problem. What should we do about it? Some
ideas:

1) Leave things as they are. We can devise conventions to avoid this
   problem. Maybe it is enough to be aware of it.

2) Make variables and constructors lexically distinguishable. In Haskell
   constructors start with an upper-case letter. We can mark variable
   patterns using some reserved character or word:

    id : {A : Set} → A → A
    id &x = x

3) Always bring constructors into scope together with the corresponding
   data type.

4) Thorsten noted that this particular instance of the problem could
   have been avoided if Agda had warned about unreachable patterns.

I'm leaning towards 4). Hopefully it is easy to change the coverage
checker so that it complains if only a proper subset of the clauses is
needed to reach full coverage. Ulf?

-- 
/NAD


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.