The following code is accepted by Agda 2.7.0.1, but not by a recent development version:
data D : Set where
c : D
record R (M : Set → Set) : Set₁ where
field
f : {A : Set} → A → M A
open R ⦃ … ⦄
postulate
F : Set → Set
module M₁ (_ : Set₁) where
postulate instance
r : R F
open M₁ Set
module M₂ (A : Set) (_ : F A) where
open M₂ D (f c)
If the last line is replaced by the following one, then the code is accepted:
open M₂ D (f ⦃ r = M₁.r Set ⦄ c)
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