[Agda] constructor/definition taxonomy in compiler internals/syntax highlighting

[Noam Zeilberger]

I've been playing with the compiler source code and noticed something
that seemed a bit strange to me, in the compiler's internal taxonomy.
Not sure whether obscure details of the compiler source are off-topic
for this list, but in any case it also shows up in syntax highlighting
(SH).  So, the compiler (and the SH) maintains a distinction between
names denoting constructors and names denoting definitions (e.g.,
DefinedName vs ConstructorName in Agda.Syntax.Scope.Monad, and green
vs blue highlighting in the SH).  My question is, how come type
*constructors* are treated as definitions?  SH aside, is there a
reason why the current taxonomy is important for the language's
semantics, or at least simplifies the compiler design?  I ask because
I'm trying to write a new compiler module, where I think treating type
constructor names as ConstructorName's would make more sense.

Noam