Andreas Abel

Agda picks the smallest solution, `i`, for the size meta, but this is incomplete, we need to take the variance into account.

Another case (lifted from #6002): ```agda {-# OPTIONS --sized-types #-} open import Agda.Builtin.Size record Thunk (F : Size → Set₁) i : Set₁ where coinductive field force : (j :...

See also https://github.com/andreasabel/agda-scope#rfc-agda-shadowing-rules.

See an example at #3350 where one would expect a positional argument to refer to an actually user-written argument, but a generalized implicit interferes.

> to defer generating the trX-trX clause? The question is, defer until _when_? You can defer the _production_ by having a new `Constraint` form that gets retried once the blocking...

The current error is: ``` An internal error has occurred. Please report this as a bug. Location of the error: __IMPOSSIBLE__, called at src/full/Agda/TypeChecking/EtaContract.hs:46:17 ``` https://github.com/agda/agda/blob/26c11b629cd60bc135ca87697cbf01ee03f094c6/src/full/Agda/TypeChecking/EtaContract.hs#L46 The new error is...

~~I think Ulf is right:~~ ``` $ cabal exec -- which agda .../bin/agda $ cabal list-bin agda .../dist-newstyle/build/x86_64-osx/ghc-9.2.2/Agda-2.6.3/build/agda/agda ``` ~~With `cabal exec` we get the _installed_ version of agda (if...

After all, @nad is right: ``` $ which agda-mode .../bin/agda-mode $ cabal exec -- which agda-mode .../dist-newstyle/build/x86_64-osx/ghc-9.2.2/Agda-2.6.3/build/agda-mode/agda-mode ``` My experiment ``` $ which agda .../bin/agda $ cabal exec -- which...

I still feel that programs whose behavior depends on the CWD should allow me to set it for them, but I do not see a pressing need in this case....

One could also relax the semantics of `--safe` to mean _safe if no open goals_. The the original meaning of `--safe` would be the new one in the absence of...