[Agda] difficult "unsolved metas"

[Serge D. Mechveliani]

People,
I am stuck with a program that forms sub-DSet -- something similar to
sub-DecSetoid, defined by a membership predicate.

Agda-2.3.2 MAlonzo (lib-0.7)  
reports of "unsolved metas" for the last line of the code.
So far, I do not find, how to fix the code.

The program uses the type constructor  ->c  for congruent maps, 
imported from  Function.Equality  (and renamed to  ->c).

"unsolved metas" is reported exactly for the line of  "cong = eCong"
in the final fragment of
  ...
  eTo : sub-Setoid ->c baseSetoid
  eTo = record{ _($)_ = fromSub     -- : subCarrier -> baseCarrier 
              ; cong  = eCong  }
        where
        eCong : _=s_ =[ fromSub ]=> _\equiv_ 
        eCong {x} {y} x-=s-y  = ...

This record is required by  Function.Equality._->_,
and eCong needs to express that  fromSub  preserves the equivalence
with respect to  _=s_  on subCarrier  and  _\equiv_ on  baseCarrier
-- which part must be most trivial in this case. 

The report preserves independently on whether the implementation for 
eCong  is given or it is postulated as  
                         postulate eCong : _=s_ =[ fromSub ]=> _\equiv_ 

The code is still simplified as contrived, and does not exactly serve
the initial need of sub-DSet (`Injection' is skipped, and other parts),
because I needed to reduce the example.

This precise code (about 170 lines) is 

     attached to this letter as     Main.agda.zip

-- 2 Kb archive. 
(Is a 2 Kb attachement large to send to this list?,
for I could alternatively put it to a public domain).

Can you, please, help with solving these "unsolved metas" ?

Thanks,

------
Sergei

-------------- next part --------------
A non-text attachment was scrubbed...
Name: Main.agda.zip
Type: application/zip
Size: 2114 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20130207/2f372358/Main.agda.zip