Jesper Cockx

I keep getting frustrated by this problem when working with erasure. Looking into the code a bit, it seems this problem might be caused by the fix of https://github.com/agda/agda/issues/4480 by...

I've made another attempt at fixing this but I'm blocked on #5837, without this issue being fixed you get hard errors too often when eta-expansion could still help. Given that...

I have a working fix of this at https://github.com/jespercockx/agda/commit/59244ca9bc11d56a422f2da1b78307052e21b57c, but currently it is still a bit crude in that it makes liberal use of `catchError` and eta-expands things even when...

I'm afraid I've lost steam working on this issue. My current WIP can be found on https://github.com/jespercockx/agda/tree/Issue5703, but it doesn't yet pass the test suite. The whole thing is a...

Now that we have `--level-universe`, we have a clear path to make this work (at least when this flag is enabled): we just need to remember the shape of the...

I'd like to take a critical look at all uses of `instantiateFull` after the release of 2.6.3, so I'm assigning this to myself.

That seems like a good plan on first sight. These definitions could perhaps in some (but not all) ways be treated as INLINE functions, e.g. for the positivity and termination...

Note that elements of `Prop` are in a sense easier to recognize than other definitional singleton types, since you only have to look at their sort. You cannot have a...

> Do you think it would be feasible to support both variants without too much code duplication or complication? You recently changed the occurs check so that it handles definitional...

Hi @jul1u5, it's great to see that you are working on this issue! I think your approach of creating a function for each instantiated metavariable is interesting and it is...