Nils Anders Danielsson

@andreasabel, what is your plan? If you want this to be fixed on the Emacs side, then I guess it makes sense to submit a patch, or at least a...

I think this works out of the box when a recent version of Emacs is used. @andreasabel, can you confirm?

A little more context: Back in 2010 @UlfNorell and I noticed that some Agda code that should be linear wasn't, and found a way to make the code faster. The...

> Cons of treating not-yet-defined functions as metavariables: > > * It makes Agda accept mutual definitions where in order to typecheck, each definition relies on the computational behaviour of...

Is this something that would be easy to implement? In that case I think we should perform this change now.

> * The internal checker had to be improved a bit, as we have to rely on it to check _again_ the types of constructor arguments with parameters and their...

> It's not strictly necessary to check the full type, we could also get away with a specialized function that traverses types in the telescope and only checked polarity annotations,...

Please add the flag `--polarity` to two lists in the user manual: https://github.com/agda/agda/blob/1c5a4e9e12a7bd66f22c3d5c0123654ea2dc0147/doc/user-manual/tools/command-line-options.rst?plain=1#L1106-L1108 https://github.com/agda/agda/blob/1c5a4e9e12a7bd66f22c3d5c0123654ea2dc0147/doc/user-manual/tools/command-line-options.rst?plain=1#L1145-L1147

If the problem with sized types is only that some meta-variables get eagerly instantiated to `∞`, then I think you can ignore that problem, the size solver is known to...

I suggest that you also change things so that the `POLARITY` pragmas can only be used if `--polarity` is used.