[Ur] using mapX

[Sergey Mironov]

Hi

I've got trouble applying mapX (declared in top.urs). I want to
translate a record filled with xml fields into one xml like this

val all = xmlify { A = <xml><p>blabla</p></xml> , B = <xml><p>zzz</p></xml> }

I know that potential problem is the order of visiting fields, but for
now Its ok to have any of <xml>{r.A}{r.B}</xml> or
<xml>{r.B}{r.A}</xml>

I attempted to declare xmlify like that:

fun xmlify
  [ctx ::: {Unit}]
  [t ::: {Type}]
  (fl : folder (map (fn _ => xml ctx [] []) t))
  (r : record (map (fn _ => xml ctx [] []) t))
     : xml ctx [] [] =
    @mapX [ident] [ctx]
      (fn [nm ::_] [t ::_] [r ::_] [[nm]~r] x => x)
        fl r

Unfortunately, the compiler errors with

dev:[grwlf at greyblade:~/proj/urdesign]$ urweb -dbms sqlite Test
/home/grwlf/proj/urdesign/Test.ur:117:6: (to 117:51) Unification failure
Expression:
fn nm :: Name => fn t :: Type => fn r :: {Type} => fn x : t => x
  Have con:
nm :: Name -> t :: Type -> r :: {Type} -> [[nm = ()] ~ r] => t -> t
  Need con:
nm :: Name ->
 t :: Type ->
  rest :: {Type} -> [[nm = ()] ~ rest] => t -> xml ctx ([]) ([])
Incompatible constructors
Have:  t
Need:  xml ctx ([]) ([])

Looks like it doesn't think that all the fields of r (the input of
xmlify) are really xmls, despite the fact that r's type is (map
(fn_=>xml ctx [] []) t) . Am I correct in this conclusion? Can I
bypass it?

Regards,
Sergey