[Ur] using mapX

[Adam Chlipala]

On 10/02/2013 08:41 AM, Adam Chlipala wrote:
> 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.

Oh, and to make that more concrete, if I replace [{Type}] with [{Unit}], 
then your example works with one small type annotation to guide the 
choice of [ctx]:
     val all : xbody = xmlify { A = <xml><p>blabla</p></xml> , B = 
<xml><p>zzz</p></xml> }

Without that change, undetermined unification variables remain.