G. Allais

I don't know about fixed size, @laMudri's original motivation to use `Fin n -> a` rather than `Vec n a` was that (together with a better definition of decidable equality)...

In Collie (declarative hierarchical command line interface library for Idris2) we have a similar story because we found that we needed two kinds of smart constructors depending on whether we...

I don't know if Wikipedia got edited in the meantime or something but [connex](https://en.wikipedia.org/wiki/Connected_relation) now makes the following distinction: * connex: `∀ {x y} → x ≢ y → x...

The problem I can see with these definitions is that we would now have two (essentially the same on propositional equality) distinct notions of injectivity and we would need to...

It looks to me like [`applyFlagsToTCWarnings`](https://github.com/agda/agda/blob/be89d4a8b264dd2719cb8c601a2c7f45a95ba220/src/full/Agda/TypeChecking/Errors.hs#L233) is completely ignoring the `WarningMode`.

Another source of problems: when we are checking the main interface we ignore the flags: https://github.com/agda/agda/blob/master/src/full/Agda/Interaction/Imports.hs#L817 Simply changing `IgnoreFlags` to `RespectFlags` there leads to an internal error in [`Serialize.Instances.Internal`](https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/Serialise/Instances/Internal.hs#L128) when...

Got it (I think)! In `TypeChecking.Warnings`, [we classify](https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/Warnings.hs#L106) `CoverageNoExactSplit` as an `ErrorWarning`. These kind of warnings [cannot be bypassed by a user-set flag](https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/Warnings.hs#L47). I think it is a mistake to...

At the moment `Werror` sets a boolean telling Agda we want all warnings to be turned into errors. I suppose we could have a more fine-grained approach and offer `-E(no)Flag`...

Right. These warnings are [filtered out after the fact](https://github.com/agda/agda/blob/2b1fe5621af463217d190b60003b9229f0317bb9/src/full/Agda/Interaction/Imports.hs#L943) if the unifier manages to find a solution despite inversion failing. One way to handle that would be to: * not...

I wonder where we should put these transformers. In the #1841 overhaul I ended up having submodules `ReaderT` & `Reader` in `Effect.Monad.Reader` because both define `functor`, `applicative`, etc. As a...