Wrong fixity applied for overloaded constructor

From andreas....@gmail.com on November 23, 2013 21:55:40

Having an overloaded constructor in scope with different fixity for its different instances bears trouble:

module A where

infixr 4 ,

record × (A B : Set) : Set where constructor , field fst : A snd : B

module B where

infixl 2 ,

data Ty : Set where

data Cxt : Set where ε : Cxt , : (Γ : Cxt) (a : Ty) → Cxt

open A open B

test : (Γ : Cxt) → Set₁ test ε = Set test (Γ , a) = {!Γ!} -- press C-c C-c here

Agda splits

test (ε , a) = ? test (Γ , a , a₁) = ?

but then cannot parse it

, is not a constructor of the datatype Ty when checking that the pattern a , a₁ has type Ty

In the current design of Agda, this cannot be made to work. Overloaded constructors with different fixity cannot be parsed before resolving the overloaded, which happens at type-checking. This shows that phase separation parsing/scope checking/type-checking is impossible for the current design.

Question: Why is the first fixity taken for , and not the second?

Answer: None should be taken, instead an error "fixity clash" should be raised (similar to when we use a name that is in scope from two different modules)!

Original issue: http://code.google.com/p/agda/issues/detail?id=978

UlfNorell / agda-test

Wrong fixity applied for overloaded constructor #978