Jesper Cockx

Ok thanks for investigating! I'll see if I can change the `__IMPOSSIBLE__` to a softer failure for now, so my work here does not have to be blocked on cubical...

That did work for the cubical library, but it seems my changes made thing extremely slow: ``` real 64m12,737s user 63m58,220s sys 0m5,516s ``` (this is w/o aggressive optimization but...

No, the version that I merged has much improved the performance wrt to the initial draft, there should hopefully not be a noticeable slowdown.

I agree that the current situation is not good. I will spend the last day at the Agda meeting tomorrow to see if I can find a fix to the...

After working unsuccessfully on finishing my fix yesterday, we had a discussion over dinner and I conceded that my change should be rolled back for now. I will prepare a...

Bumping this to 2.6.5, sadly.

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

Perhaps it would be useful to add a generic reachability analysis to the backend infrastructure of Agda? It could take a set of initial names as input and compute the...

I noticed that the Treeless syntax currently does not preserve any of the `ArgInfo`. If we do not erase arguments marked with `@0` entirely from the Treeless syntax, then we...

I noticed that if one makes `A` and `F` into module parameters instead, you get unsolved constraints in both cases. This makes even less sense to me, since module parameters...