[Agda] reexport from record

[Serge D. Mechveliani]

People, 
I have a strange behavior of a record export with `public'.
The record is like this:

-------------------------------------------------------------
record Foo c l {upMon : UpMonoid c l} :  Set _
  where
  upMonoid = upMon
  ...
  setoid      = DecSetoid.setoid decSetoid
  Carrier : Set c
  Carrier = Setoid.Carrier setoid
  _~_     = Setoid._\~~_ setoid       -- (math symbol replaced)

  ~equiv : IsEquivalence {A = Carrier} _~_
  ~equiv = Setoid.isEquivalence setoid 

  open IsEquivalence ~equiv public renaming 
                           (sym to ~sym; refl to ~refl; trans to ~trans)
  field foo : Foo' 
  ...
--------------------------------------------------------------

I set `public' because the goal is to re-export  ~sym, ~refl, ~trans
from Foo with renaming, in order to apply things like
                                                      Foo.~sym r

Another way to reexport it is to set   ~sym = IsEquivalence.sym ~equiv 
                                       ...
instead of `open'.
But for my code, the checker reports of "unsolved metas" - until I 
add signature for each of   ~sym, ~refl, ~trans.
So, I have decided that  "open - public - renaming"  is shorter and 
nicer. 

Without `public', it is type checked, but  Б┬╪sym  is not exported.
And inserting `public' leads to the report
(in Agda-2.3.2 MAlonzo)
----------------------------------
Not a valid let-declaration
when scope checking
let open
      IsEquivalence ~equiv
        public renaming (sym to ~sym; refl to ~refl; trans to ~trans)
in (foo : Bool) -> Set
-----------------------------------

Is it an error in the checker?
How to fix my program?

The code fragment  with math symbols  is attached here as  t.agda.zip 

Thanks,

------
Sergei 
-------------- next part --------------
A non-text attachment was scrubbed...
Name: t.agda.zip
Type: application/zip
Size: 385 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20130220/96017248/t.agda.zip