[Agda] Coinductive records and separate files in Agda

[William Harrison]

Hi-

    I’m not able to separate the definition of a coinductive record type
from definitions using that type. I’ve attached two files giving a minimal
example of the issue. I’m trying to determine if I’m doing something wrong
or if I’ve discovered a bug/feature.

The first file (Records1.agda) gives the usual definition of a stream using
coinductive record syntax and a non-coinductive record; respectively, these
are Stream and Derp. I can define within Record1 particular Streams (e.g.,
zeros below):

record Stream {ℓ} (A : Set ℓ) : Set ℓ where
  coinductive
  field headStr : A
        tailStr : Stream A
open Stream; S = Stream

zeros : Stream ℕ
headStr zeros = 0
tailStr zeros = zeros

record Derp (A B : Set) : Set where
  field
    fld1 : A
    fld2 : B

In the second file (Records2.agda), I load Records1 (hiding zeros):

open import Records1 hiding (zeros)

-- Use of non-coinductive record in this file works fine:
foo : Derp ℕ ℕ
foo = record { fld1 = 0 ; fld2 = 1 }

-- The identical zeros definition generates an odd error:
zeros : Stream ℕ
headStr zeros = 0
tailStr zeros = zeros

That error is:

<local-file-path>/Records2.agda:12,1-14
Could not parse the left-hand side headStr zeros
Operators used in the grammar:
  None
when scope checking the left-hand side headStr zeros in the
definition of zeros

Am I doing something wrong here? Is there some way to separate coinductive
record type declarations and particular values of those types in distinct
files? If it matters, I’m using Agda 2.6.0.1, although I’ve seen this same
behavior in earlier versions of Agda.

Thanks,
Bill
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200116/abfb31de/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Records1.agda
Type: application/octet-stream
Size: 322 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200116/abfb31de/attachment.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Records2.agda
Type: application/octet-stream
Size: 564 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200116/abfb31de/attachment-0001.obj>