[Agda] Problem with ``open'' in ``record'' before ``field''

[kahl at cas.mcmaster.ca]

I tried to use the ``open'' trick I found in the standard library
(working with the current development version)
to re-export material from nested records,
but encountered a class of situations where it does not work:
If there is another ``field'' after the ``open'',
I get a ``Not a valid let declaration when scope checking'' message.
(Artificial example below. With the ``open'', it fails no matter whether
 ``fun'' is moved before the second ``field'' or not.
)

The modules page in the reference manual does not help with this,
and the records page does not even clearly document
the possibility to have anything besides fields in a record
(see ``General Syntax'' there).

Again, I can work around this, but it is tedious ---
is this restriction intentional?


Wolfram

---


{-# OPTIONS --universe-polymorphism #-}

module BiSetoid where

open import Level

open import Relation.Binary.Core
open import Relation.Binary using ( Setoid ; module Setoid  )


record BiSetoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  field
    setoid : Setoid c ℓ₁
  
  open Setoid setoid public -- in the presence of the field below, this does not work.

  -- Carrier = Setoid.Carrier setoid -- this works

  field
    _≐_ : REL Carrier ℓ₂
    isEq2 : IsEquivalence _≐_

  fun : Set _
  fun = Carrier → Carrier