[Agda] overlapping _∷_, []

[James Wood]

Note that record field names can also overlap if they are applied
directly to a record value. The theory behind this is in bidirectional
type checking, and how a term having its type checked (rather than
inferred) may be ambiguous without the information from the type. The
same mechanism allows λ to be reused for dimension abstraction in
cubical Agda (because it is a constructor).

In short, overloading is fine in the following cases:

- Everything being overloaded is a constructor, and there is an obvious
type to check the resulting construction against.
- Everything being overloaded is a field, and there is an obvious record
type that the field is destructing.

Outside of these cases, overloading fails.

You might notice also that the agda2-infer-type command will usually
fail to infer the type of a construction of which the head is an
overloaded constructor. This is because Agda really wants to check the
construction, rather than inferring a type for it. It just happens that
when the constructor is not overloaded, it's easier to make progress,
because that gives just enough to check the construction against.

Regards,
James

On 22/12/2019 20:11, Orestis Melkonian wrote:
> Constructor names can overlap; the right one will be chosen on usage
> depending on the expected type.
> Note that other kind of names cannot overlap (e.g. definition names,
> etc..).
> 
> Cheers,
> --OM
> 
> On 22-12-19 20:05, mechvel at scico.botik.ru wrote:
>> People,
>>
>> how does this occur that Data.List.Relation.Unary.All.Properties
>> open-imports
>>              _∷_, []
>>
>> both from Data.List  and from  Data.List.Relation.Unary.All
>> ?
>> Are these constructor names so special that they are overloaded?
>>
>> Regards,
>>
>> ------
>> Sergei
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda