The following code is accepted:
module _ where
open import Agda.Builtin.Equality
module M (A : Set₁) where
opaque
B : Set₁
B = A
module N (A : Set₁) where
open M A public
open N Set
opaque
unfolding B
_ : B ≡ Set
_ = refl
However, if I replace the local modules with modules in separate files (in a certain way), then Agda rejects the code:
module M (A : Set₁) where opaque B : Set₁ B = A
module N (A : Set₁) where open import M A public
module _ where open import Agda.Builtin.Equality open import N Set opaque unfolding B _ : B ≡ Set _ = refl
———— Error —————————————————————————————————————————————————
[…]/Bug.agda:11,7-11
B != Set of type Set₁
when checking that the expression refl has type B ≡ Set
———— Warning(s) ————————————————————————————————————————————
[…]/Bug.agda:8,13-14
warning: -W[no]UnfoldTransparentName
The name B, mentioned by an unfolding clause, does not belong to an
opaque block. This has no effect.
I can make the code work again by referring to the underlying definition of B instead of the reexported one:
module _ where open import Agda.Builtin.Equality import M open import N Set opaque unfolding M.B _ : B ≡ Set _ = refl
I don't think Agda should care if the code is in one or multiple files.
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