The following code is accepted by Agda 2.7.0.1, but not by a recent development version that includes the fix for issue #7797:
data D : Set where
record R (F : Set → Set) : Set₁ where
field
f : (A : Set) → F A
open R ⦃ … ⦄
postulate
F₁ F₂ : Set → Set
instance postulate
r₁ : R F₁
r₂ : R F₂
module M (_ : F₁ D) where
open M (f D)
If the last line is replaced by the following one, then the code is accepted:
open M (f ⦃ r = r₁ ⦄ D)
Is this change intended, or is this a bug?
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4