[Ur] Unification failure when duplicating result of a monadic XML generator

Tue Jul 22 08:32:36 EDT 2014

On 07/20/2014 05:52 AM, Sergey Mironov wrote:
> I've learned the situation a bit more, and now think that it is not a
> bug, but a feature of the typesystem. Basis.join's definition says
> that it's right fragment's type depends on it's left fragment's type:
> use2 should be equal to (use1 ++ bind1) :
> (from the manual:
>   val join : ctx ::: {Unit} → use 1 ::: {Type} → bind 1 ::: {Type} →
> bind 2 ::: {Type} → [use 1 ∼ bind 1 ] ⇒ [bind 1 ∼ bind 2 ] ⇒
>
>    (*left fragment *) xml ctx use 1 bind 1 →
>    (* right fragment *) xml ctx (use 1 ++ bind 1 ) bind 2 →
>    (* the result*) xml ctx use 1 (bind 1 ++ bind 2 )
> )
>
> I feel that it is the key to understanding of the problem.

Right.  I do believe your original code can be elaborated with type 
annotations into a type-correct program, but the Ur/Web type inference 
engine isn't smart enough to do it.  One minor issue is that the type of 
[main] was genuinely ambiguous, but adding a [: transaction page] 
annotation there resolves the ambiguity.

It turns out that turning the second [r] reference into a [useMore r] 
gets us to a type-inferrable program, but I think that's just a fluke.  
Basically, type inference for Ur/Web is undecidable, and we should be 
happy that this small change is enough to get everything to work. ;)

> But I still
> can't figure out the exact meaning of the second parameter of [xml]
> constructor, refered as 'use' above. What does it mean? Why we can't
> define a symmetrical join with signature like [ xml ctx use1 bind1 ->
> xml ctx use2 bind2 -> xml ctx (use1 ++ use2) (bind1 ++ bind2)] ?

The [use] parameter describes the environment of previously defined form 
fields, which determines the expected types of any <submit> handlers.  
Your alternative [join] operator doesn't quite make sense from that 
perspective.

> And the second question: Why doesn't compiler accept the join call
> which have empty use's and bind's? Shouldn't it figure out that [] ==
> [] ++ [] ?

Type inference is getting especially confused by your polymorphic type 
parameters for [inp] and [frm].  Removing them and hardcoding those type 
indices as [[]], I get a different error message about the occurs check 
failing, and it makes sense that it would fail. C'est la vie.  
Undecidable type inference, etc. ;)

> Regards,
> Sergey
>
> 2014-07-19 22:49 GMT+04:00 Sergey Mironov <grrwlf at gmail.com>:
>> Hi.
>>
>> Here is the issue I've faced recently. The code below failed to
>> compile with 'Unification failure' (full text is below the program).
>> Looks like a bug, please check!
>> Sorry if it is a duplicate, quick search shows no matches for such a
>> problem for me.
>>
>> Regards,
>> Sergey
>>
>> --
>>
>> fun mkrow [o ::: {Unit}] [inp ::: {Type}] [frm ::: {Type}] [o ~
>> [Table,Tr]] (x:xml (o++[Tr]) inp frm) :
>>    transaction (xml (o++[Table]) inp frm) =
>>      return <xml><tr>{x}</tr></xml>
>>
>> fun main {} =
>>    r <- mkrow (<xml><td>an item</td></xml>);
>>    return <xml>
>>      <head/>
>>      <body>
>>      <table>
>>        {r}
>>        {r} (* <--- LINE 26 *)
>>      </table>
>>      </body>
>>    </xml>
>>
>> --
>> The error message:
>>
>>
>> /home/grwlf/proj/urbugs/XML.ur:26:3: (to 27:8) Unification failure
>> Expression:
>> Basis.join [<UNIF:U232::{Unit}>] [<UNIF:U233::{Type}>] [[]]
>>   [<UNIF:U235::{Type}>]
>>   (Basis.cdata [<UNIF:U232::{Unit}>] [<UNIF:U233::{Type}>] "\n")
>>   (Basis.join [<UNIF:U232::{Unit}>] [<UNIF:U233::{Type}>] [[]]
>>     [<UNIF:U235::{Type}>]
>>     (Basis.cdata [<UNIF:U232::{Unit}>] [<UNIF:U233::{Type}>] "      ")
>>     (Basis.join [<UNIF:U232::{Unit}>] [<UNIF:U233::{Type}>]
>>       [<UNIF:U235::{Type}>] [[]] r
>>       (Basis.join [<UNIF:U232::{Unit}>]
>>         [<UNIF:U233::{Type}> ++ <UNIF:U235::{Type}>] [[]] [[]]
>>         (Basis.cdata [<UNIF:U232::{Unit}>]
>>           [<UNIF:U233::{Type}> ++ <UNIF:U235::{Type}>] "\n")
>>         (Basis.cdata [<UNIF:U232::{Unit}>]
>>           [<UNIF:U233::{Type}> ++ <UNIF:U235::{Type}>] "    "))))
>>    Have con:
>> xml <UNIF:U232::{Unit}> <UNIF:U233::{Type}> <UNIF:U235::{Type}>
>>    Need con:
>> xml <UNIF:U232::{Unit}> (<UNIF:U233::{Type}> ++ <UNIF:U235::{Type}>)
>>   <UNIF:U229::{Type}>
>> Constructor occurs check failed
>> Have:  <UNIF:U233::{Type}>
>> Need:  <UNIF:U233::{Type}> ++ <UNIF:U235::{Type}>
>>
>> PS Removing line 26 a well as inserting [r2 <- mkrow (...);] followed
>> by changing line 26 to [{r2}] brings program back to working.