Lucas Escot
Lucas Escot
When defining an unboxed record, one gets to define new instances for type classes on the Agda side. Those instances never get compiled, and code that uses instances over boxed...
We currently rely on `haskell-src-exts`. It doesn't support all modern Haskell syntax, is barely maintained and only offers a String pretty-printer. We may be interested in using this library instead:...
Not being able to use the [rewrite construct](https://agda.readthedocs.io/en/v2.6.4.1/language/with-abstraction.html#with-rewrite) is proving to be extremely annoying. Related: #40, #255.
Wonder if we could support `with` syntax for matching on _views_ specifically. https://arxiv.org/pdf/2301.02194.pdf
Using those can prove to be annoying on the Agda side: https://github.com/agda/agda2hs/blob/15314cd3fbc505ead13e48257194afd5ca171672/lib/Haskell/Prim.agda#L38 We may want to make it dependent too, so long as we annotate with erasure properly.
[See `\cases`](https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/lambda_case.html) supported since GHC `9.4.1`.
**WIP** Wanted to add support for the following `Singleton` datatype: ```agda data Singleton (a : Set) : @0 a → Set where MkSingl : ∀ x → Singleton a x...
Defining an alias to a strictly-positive functor as opaque prevents it from being seen as strictly-positive. Is this intended behavior? ```agda module opaquepos where open import Agda.Builtin.List opaque MyList :...
We should enable the `existing-class` pragma for postulated type classes: ```agda postulate MyShow : Set -> Set myshow : {{ MyShow a }} -> a -> String {-# COMPILE MyShow...