Lucas Escot
Lucas Escot
Related: agda/agda#7253
This is a known issue. See #85 and the current workaround introduced in #103. That is, to get explicit foralls you need to introduce an anonymous module with implicit `Set`...
I think figuring out when to throw an error for this is probably only slightly less difficult than automatically inserting the explicit `forall`s, so hopefully by then we won't need...
Iirc I have a stale branch where this is the behavior you mention: all `forall`s are made explicit. Maybe I can find this stale branch and put it under a...
Related PR: #332
I agree that the positivity checker should _probably_ not know this by default, and positivity information should ideally be expressed intentionally in the type of opaque definitions with polarity annotations....
> The use case is worth keeping in mind: Even though the computational parts of the data type do not depend on the type class, the (erased) invariants can only...
Wait, now that I think about it we already have the following pragma: ```agda {-# COMPILE AGDA2HS IsEra existing-class #-} ``` used extensively in the prelude to avoid compiling the...
> Unfortunately, it does not appear to work on postulate. Right, the culprit here seems to be this line: https://github.com/agda/agda2hs/blob/0412c42844b94d4d687d8bba3a29e7e815c93a2b/src/Agda2Hs/Compile/Utils.hs#L170 Where we require `Record`s for class candidates. I think it...
Linking agda/agda#5541, because if there is support for it upstream any backend would be able to preserve comments attached to definitions.