Nils Anders Danielsson

Importing Agda.Primitive.Cubical without --cubical or --erased-cubical should fail

3

@jespercockx [reported](https://github.com/agda/agda/issues/3750#issuecomment-1266799994) that one can import `Agda.Primitive.Cubical` without enabling `--cubical` or `--erased-cubical`. That should not be possible. This fails: ```agda open import Agda.Builtin.Cubical.Glue ``` ``` Importing module Agda.Builtin.Cubical.Glue using the...

A variant of Cubical Agda that is consistent with UIP

20

I have a development where I use extensionality and the propositional truncation, some parts of the code use instances of univalence (introduced as assumptions), and some parts use instances of...

Use relative paths?

1

Currently Agda uses "canonical" absolute paths. This can lead to performance problems (#5673) and has at least in the past led to a bug report related to symbolic links (#4828)....

The computation `sourceToModule` is used in `generateAndPrintSyntaxInfo`, which is used repeatedly: https://github.com/agda/agda/blob/82b2b0fbea55c1716685d72cd8546b533d0f12dc/src/full/Agda/TypeChecking/Monad/Base.hs#L876-L883 For large developments this could have a non-trivial cost.

Agda is slow for a pattern variable with a large type

4

I was working on a proof and Agda became much slower when I replaced one variable in the left-hand side by a non-trivial pattern, even though I did not use...

Agda sometimes stores interface files in incorrect locations

1

Agda seems to use the location of a `.agda-lib` file, if any, even if `--no-libraries` is used: ``` $ (mkdir outer1 && cd outer1 && touch .agda-lib && mkdir inner...

Document ThingsInScope

1

A value of type `ThingsInScope a` is a map from names to lists of `a`'s: https://github.com/agda/agda/blob/3b9831fd6dfdfdfb46dc7d92e0becf9518cfe840/src/full/Agda/Syntax/Scope/Base.hs#L313 The following code, which uses `List.union`, suggests that the lists might represent sets: https://github.com/agda/agda/blob/3b9831fd6dfdfdfb46dc7d92e0becf9518cfe840/src/full/Agda/Syntax/Scope/Base.hs#L542-L543...

Internal errors due to use of runSpeculative

3

You can get an internal error if you use `runSpeculative m`, where `m` constructs and returns a fresh meta-variable but asks for the state to be reverted, if you then...

Cannot reduce type because variable is erased

1

A follow-up to issue #5734: ```agda open import Agda.Builtin.List open import Agda.Builtin.Reflection open import Agda.Builtin.Unit id : (@0 A : Set) → A → A id _ x = x...

Solving blocked terms loses the user-written code

17

Consider the following code: ```agda postulate A : Set F : Set → Set P : F A → Set id : F A → F A f : (x...