Andreas Abel

This is the Twelf approach to name picking, which I think works well in practice and is more principled than our current heuristics.

> 🤔 I also ask myself if choosing a signature of the form `A → List A → List A` vs. another one of the form `(x : A) →...

Agda dev meeting 2025-04-16: We could mine the `variable` declarations for name suggestions _now_ without introducing a new pragma. E.g. we could construct a map from concrete type names to...

@mpickering wrote: > [ ] Remove v1-commands Relevant issue collections include: - https://github.com/haskell/cabal/issues?q=label%3A%22re%3A+v1-install%22 - https://github.com/haskell/cabal/issues?q=label%3A%22re%3A+v1-vs-v2%22 On the danger of repeating myself: I first want to see feature completeness of v2...

The problem seems to be that `s` gets the Fomega-type `forall A -> STUFF -> A -> A` which looks it `s` was parametric in `A`. But it is not,...

Or with no indexed types at all: ```agda {-# OPTIONS --type-based-termination #-} {-# OPTIONS --no-syntax-based-termination #-} {-# OPTIONS --no-size-preservation #-} open import Agda.Primitive open import Agda.Builtin.Nat data ⊥ : Set...

Fixing `B`: ```agda -- Being logical equivalent to Nat data NAT (A : Set) : Set where mk : (A → Nat) → (Nat → A) → NAT A id...

> ```agda > bad (suc n) _ = bad (const 100 n) (yes 99) > ``` This looks more like a fixable bug than a conceptual problem, does it? Should...

I am afraid we cannot merge the tbt PR and this issue does not apply to master, so, closing as unresolved.

> (Also tries to sneak in `ImportQualifiedPost` so can't be merged until we drop ghc-8.8) So, wait for #7908 - #7908