[Agda] message of parameterized

[Serge D. Mechveliani]

On Fri, Sep 07, 2012 at 09:43:22AM +0200, Andreas Abel wrote:
> Hello Serge,
>
> On 06.09.12 3:35 PM, Serge D. Mechveliani wrote:
>> I have two suggestions for the compiler and one note.
>>
>> 1. If a function  foo  is imported from a  parameterized module  Foo,
>>     and the compiler reports something about the _arguments_ for  foo,
>>     then it has sense to add to the report:
>>     "For any occasion: mind that the module  Foo  has parameters".
[..]
>> So, one probably needs to write  Commutative _==_ _+_
>> in this situation rather than    Commutative _+_
>>
>> A programmer sees in the library sources
>>               `Commutative : Op2 A -> Set _',   `Commutative _+_', ...,


> At this point, the programmer should wonder about a seemingly unbound  
> identifier `A' in the type signature of Commutative and a go looking for  
> its origin.  Then he would finally arive at the module header.

This looks reasonable. I have missed this. 


>> 2. A minor suggestion:
>>     a code piece in a message will be easier to read if it is surrounded
>>     either with a pair quotes or extra blanks:
>>
>>    checking that the expression plus has type Rel Nat _5 foo foo ...
>>    -->
>>    checking that the expression `plus' has type `Rel Nat _5' foo foo ...
>
> We cannot used quotation marks since they are allowed in identifiers.
>
> Maybe a different color would be best.


Color would help. Probably it has sense to also surround it with an 
extra pair of blanks.

Thanks,

------
Sergei