[Agda] message of parameterized

[Serge D. Mechveliani]

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".

Motivation
----------
Consider the code 
 plus : Op2 Nat
 plus = Data.Nat._+_
 CommPlus : Set _
 CommPlus = Algebra.FunctionProperties.Commutative plus

(under Agda-2.3.0.1, lib-0.6, 
 and for this letter I replace  
              Op\_2 with Op2,  \bn  with  Nat,  \equiv  with  _==_ 
).
The report is
 "Nat !=< (Set _5) of type Set
  when checking that the expression plus has type Rel Nat _5
 "
I have a bit more complex code, which I have reduced to this one, 
trying to debug the program.
why it needs  Rel Nat _5  instead of  Op2 Nat  ?
At this point I have been puzzling for 1 hour, intil dicovered 
(only by occasion!) that the module  Algebra.FunctionProperties  is 
parameterized.
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 _+_', ...,

and it is difficult to guess that there might be needed an additional
argument to insert.

Probably, parameterized modules are good. But they present a certain bug 
farm, so it has sense for the compiler to provide a help.

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 ...

3. A note on `view'.
   I nice TRW logical language  Maude  has a very different notion of
`view'
(it also has parameterized modules, and the fixity denotations like 
`_f__ :',  `if_then_else : ...'). 
As I recall, a view there is a module map produced by instantiating 
sorts for module parameters.

Regards,

------
Sergei