[Agda] Possibly infinite/exponential compilation time by just calling a certain function

[Nils Anders Danielsson]

On 2017-06-13 14:41, Jan Bracker wrote:
> I like using module arguments, because they are very useful when all
> of the definitions work with the same input. But this experience
> discourages me from using them somewhat, because there apparently seem
> to be some issues with them in the compiler.

The special case that I mentioned only works when terms (including all
inferred implicit arguments) are syntactically identical. This is a
brittle condition.

> Should I file a bug report about this?

If my guesses are correct, then I wouldn't call this a bug. However, I
have not verified that they are correct.

> (If so, where? On GitHub?)

Yes.

-- 
/NAD