[Ur] using mapX

[Adam Chlipala]

On 10/02/2013 06:28 AM, Sergey Mironov wrote:
> 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
>    

The [ident] above indicates the type-level identity function, which 
doesn't mesh with the type you chose for [r], and which explains why the 
compiler expects [x] to have type [t].  Instead of [ident], you should 
write [fn _ => xml ctx [] []] again.

By the way, you'll probably find use of this function easier if you 
change the kind of [t] to [{Unit}].  Since you're ignoring the types 
stored inside [t] at present, type inference won't be able to 
reconstruct them uniquely from context.