[Ur] Folds on lists of xbody

[Adam Chlipala]

The issue here is that in Ur/Web, HTML fragments in general are allowed 
to bind form fields and refer to form fields that were bound earlier.  
The type of [join] reflects the fact that the 2nd argument may refer to 
fields defined in the first.  The error message below is talking about 
U82 as the "extra" fields bound by the first [join] argument.  If we 
specify that type parameter as the empty record, then the problem goes away.

So here's an easy way to make that specification:
     val f = List.foldl (join : xbody -> xbody -> xbody) <xml/> e

On 05/27/2013 08:45 PM, Istvan Chung wrote:
> I am attempting to use List.foldl to join a list xbody:
>
>     val a : xbody =<xml><p>Hello</p></xml>
>     val b : xbody =<xml><p>World!</p></xml>
>     val c = join a b
>     val d = (join b (join a<xml/>))
>     val e : list xbody = (a :: b :: [])
>     (* All ok up to here... *)
>     val f = List.foldl join<xml/>  e
>
> Which causes Ur/Web to give the (opaque to me) error message:
>
>      Unification failure
>      Expression:
>      join [<UNIF:U80::{Unit}>] [<UNIF:U81::{Type}>] [<UNIF:U82::{Type}>]
>       [<UNIF:U83::{Type}>]
>        Have con:
>      (xml<UNIF:U80::{Unit}>  <UNIF:U81::{Type}>  <UNIF:U82::{Type}>) ->
>       (xml<UNIF:U80::{Unit}>  (<UNIF:U81::{Type}>  ++<UNIF:U82::{Type}>)
>         <UNIF:U83::{Type}>) ->
>        xml<UNIF:U80::{Unit}>  <UNIF:U81::{Type}>
>         (<UNIF:U82::{Type}>  ++<UNIF:U83::{Type}>)
>        Need con:
>      (xml<UNIF:U80::{Unit}>  <UNIF:U81::{Type}>  <UNIF:U82::{Type}>) ->
>       (xml<UNIF:U80::{Unit}>  (<UNIF:U81::{Type}>  ++<UNIF:U82::{Type}>)
>         <UNIF:U83::{Type}>) ->
>        xml<UNIF:U80::{Unit}>  (<UNIF:U81::{Type}>  ++<UNIF:U82::{Type}>)
>         <UNIF:U83::{Type}>
>      Constructor occurs check failed
>      Have:<UNIF:U81::{Type}>
>      Need:<UNIF:U81::{Type}>  ++<UNIF:U82::{Type}>
>
> Why does this happen, and why does no such error occur for expression
> [d], which seems to perform the same set of joins?
>