Here's a minimal reproducer:
module Test where
open import Agda.Builtin.Nat
record R : Set where
record S : Set where
field s : Nat
module X (r : R) (open R r) where
module A (Z : Set) where
open S public
module B (Z : Set) where
open A Z
t : S → Nat
t = s {_}
In the last line, note that s should not accept a hidden argument. However, this file type checks. If we put a hole there, we can see that s has the type {r = r₁ : R} → R.S _ → Nat instead of the expected S → Nat. Also, if the opening of R r is moved inside the module, s has the expected type in B. I tested this with with Agda versions 2.6.4 and 2.7.0.
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