[Agda] Incompatibilities affecting ``Fresh Look''

[Andreas Abel]

On 12/15/10 6:13 PM, kahl at cas.mcmaster.ca wrote:
> I had not been fully aware of this (I remember reading it, but so far
> I have never felt tempted to seriously consider this possibility).
> Does anybody have a good use case for that?
> (I come from Haskell...)

Yes.  Since you can have many refinements of the same structures, like 
refining list to vectors, sorted lists, sorted vectors, etc., it is 
convenient to allow them to share the name for nil and cons.

Without overloading, we get nowwhere.  (Imagine a language where there 
are different verbs for eating bread, eating rolls, eating roll with 
butter, eating rolls with butter and jam...) ;-)

-- Andreas