Can be merged fast-forward. This implements the first step of the language consolidation plan (#1), by removes the concept of a "language variant" (with K/without K/whichever cubical). A lot of tests had to move, and, of course, this drops support for the stdlib. In passing I fixed two upstream bugs.
There's a performance regression in code like below (see test/Perf/UnifyLiteral), which now can't make use of the literalStrategy to deal with the reflexive unification problem (since the Deletion step is disabled); they fall back to doing 9999999999 Injectivity steps instead.
pathological:(e:9999999999≡9999999999)→Setpathologicalrefl=Nat
The solution will be to split the Deletion step into the general case that is only supported when splitting on an SSet (for which we can't, and don't need to, generate left inverses), and a specialized LitDeletion step (which we can support).
Can be merged fast-forward. This implements the first step of the language consolidation plan (#1), by removes the concept of a "language variant" (with K/without K/whichever cubical). A *lot* of tests had to move, and, of course, this drops support for the stdlib. In passing I fixed two upstream bugs.
---
There's a performance regression in code like below (see `test/Perf/UnifyLiteral`), which now can't make use of the `literalStrategy` to deal with the reflexive unification problem (since the `Deletion` step is disabled); they fall back to doing 9999999999 `Injectivity` steps instead.
```agda
pathological : (e : 9999999999 ≡ 9999999999) → Set
pathological refl = Nat
```
The solution will be to split the `Deletion` step into the general case that is only supported when splitting on an `SSet` (for which we can't, and don't need to, generate left inverses), and a specialized `LitDeletion` step (which we *can* support).