[Agda] Re: Poll: Mixfix and parametrized modules --- which behavior would you expect

[Darin Morrison]

Hi,

I am currently making heavy use of parametrized modules with infix fields for an important research project. Basically I am following the schema described by Thorsten, although with a few other tricks here and there depending on specific use cases.

In my examples at least, I am quite certain the implicit parameter cannot always be inferred. In fact, in most cases it cannot be because the parameter is itself another record (maybe also parametrized) containing several functions. I suppose this ends up leading to higher order unification problems.

I don't think a change in semantics is currently warranted, especially if it would lead to a lot of code breakage for those already dealing with this problem, but I could certainly imagine some sort of changes to help with pretty printing.

What about some sort of pragma the pretty printer would be aware of that lets you specify an alternative syntax for a field when using a module unopened?

Cheers,
Darin