Jesper Cockx

Amazing work @lawcho ! If you (or anyone else) are planning to address this (which would be extremely welcome), may I suggest to break things up into separate PRs, for...

I'm not sure why exactly the change is needed but if there's a good reason then I don't mind it either (assuming the `make install-deps` only needs to be done...

This concerns developer experience so it doesn't really make sense to put it on a specific milestone.

Of course, changing such a long-standing call to `instantiateFull` reveals warts where we rely implicitly on terms being fully instantiated. There are two in the `Succeed` test suite: - The...

Related: https://github.com/agda/agda/issues/3094 (except here we are not only calling `instantiateFull` but also `reduce`)

This concerns developer experience so it doesn't really make sense to put it on a specific milestone.

Seems to be some bad interaction between generalization and sort inference. Debug output with `-v tc.sort:60`: ``` sortOf Issue6916.GeneralizeTel sortOfE a = {A = A₁ : Set} → Set hd...

Running the test with `-v tc:50 -v tc.sig.param:90` the first suspicious part of the output is this: ``` checkApplication hd = extract args = f ? e = extract (f...

This PR has conflicts with current `master`. Otherwise, it seems like a good change.

This is not a regression, so it can wait until the next release.