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

[kahl at cas.mcmaster.ca]

<<< Second attempt, now with Unicode-free Agda source >>>

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 : Set (suc zero) where
  field
    setoid : Setoid zero zero
  
  open Setoid setoid public -- in the presence of the field below, this does not work.

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

  field
    R : REL Carrier zero
    isEq2 : IsEquivalence R

  fun : Set _
  fun = Carrier -> Carrier