Nils Anders Danielsson
Nils Anders Danielsson
> That did work for the cubical library, but it seems my changes made thing extremely slow: Were these changes part of the changes that you committed?
The bug fix breaks code and seems to have caused a massive performance regression. Furthermore the error is not that Agda accepts too much code, but that Agda rejects too...
> I will prepare a PR that rolls back the change without losing all of the work I did on refactoring and improving the old code. Thanks.
At the moment we do not compile Cubical Agda code properly: for some code we generate calls to `error` (or something like that), and for some code we generate code...
If subtyping is removed for `@0` (#5427), then no coercions would be necessary.
Subtyping has now (hopefully) been removed for `@0`.
The following problem might be related: ```agda postulate _≡_ : {A : Set} → A → A → Set refl : (A : Set) (x : A) → x ≡...
A type `A` is modal for the erasure modality if `λ x → [ x ] : A → Erased A` is an equivalence. I'm not aware of a name...
Now that Agda can serialise meta-variables (#5731) it might make sense to revisit this idea.
One idea is to treat instantiated meta-variables like (simple) function definitions. We already have (or should have) code that ensures that, for a definition like `f (suc n) = f...