Wrap record accessors in an implicit namespace

[david-christiansen]

When elaborating a record

record A where
  MkA : (arg : Int) -> A

the elaborator should wrap an implicit namespace A around the accessors. This would allow them to be more easily overloaded and disambiguated.

I'll try to do this when I get a minute. The ticket is just to remember.

[david-christiansen]

Hmm, should constructors be in an implicit namespace as well? It would seem that this would avoid having to wrap separate list-like datatypes in namespaces, and at the same time give an easy and predictable way to disambiguate them (List.Nil vs Vect.Nil).

This is less good for operator names, though. Perhaps it should only happen to non-infix-named datatypes.

What do you think, @edwinb?

[andy-morris]

Apropos of this: should we have syntax for qualified operators? I guess x M.+ y (or M.+ x y à la SML) is a bit gross looking, but possibly better than nothing?

Either way, I agree that constructor namespaces'd be nice. At least they'd be useful for a lot of cases.

[david-christiansen]

The syntax is like Prelude.Classes.(+).

[andy-morris]

Oh, right. Never mind then. (That looks nicer too!)

[david-christiansen]

@edwinb: any objections to my wrapping constructors in an implicit namespace, with the same name as the family?

[Melvar]

I believe this has been implemented for accessors. If constructors should be done, perhaps the issue title should be changed. Note that it is possible to define constructors with additional namespacing explicitly.

[ahmadsalim]

I think this would still be nice to have.