Andreas Abel

The problem is that this is unsafe, unless we make sure that we give correct custom compilations for __all__ involved abstract definitions. For instance, if we comment out the ```...

Thanks for fixing!

> I've installed [git-sizer](https://github.com/github/git-sizer/) I considered this, but don't have enough space to install a new PL.

@ice1000: Life paths are strange. I only became a type theorist because the class on TT I attended left me utterly confused...

@gallais @MatthewDaggitt I wouldn't like to censor this kind of metaphorical expression (I am fond of metaphors even of a such drastic kind). But I acknowledge the possibility of trigger....

`createInterfaceIsolated` is claiming in a comment "Every interface is treated in isolation.", but the imported rewrite rules are still active because the imported signature `isig` is preserved (via `addImportedThings`) when...

> Alternatively, we could just set the `-Werror` GHC option in the `cabal.project` file and not introduce a new flag at all? Indeed, good point. However, this requires us to...

Well, Hackage only accepts individual packages, defined by a `.cabal` file, and not package collections, as would be defined by a `cabal.project` or `stack.yaml` file. So these files do not...

GHC 9.0 has a type checking regression I hit here : https://github.com/agda/agda/actions/runs/14021462831/job/39253976578?pr=7756 On my Mac M4 I cannot install GHC 9.0 or lower without extra effort, as they require an...

Agda Hackathon 2024-10-16: With dependent matching one could possibly exploit the Fomega semantics of TBT: ```agda {-# OPTIONS --type-based-termination #-} open import Agda.Builtin.Equality open import Agda.Builtin.List data Rose (A :...