[Ur] XML unification problem

Fri Aug 9 08:32:46 EDT 2013

2013/8/9 Adam Chlipala <adamc at csail.mit.edu>:
> On 08/09/2013 07:04 AM, Sergey Mironov wrote:
>>
>> Code below (and here [1]) triggers XML unification error (at the
>> bottom) which I can't understand. However, the code can be compiled if
>> one remove second (or first) call to 'reload<lang>'.
>>
>> [...]
>>
>>
>> and template reload (l:lang) =
>>     <xml>
>>       [...]
>>         {reload Ru}
>>
>
>
> You probably just need to add a full type annotation on [reload].  Ur
> necessarily has incomplete type inference, since the full problem is
> undecidable.

No, it didn't help.. I've updated the [1] code (new version below),
now it contains full signatures in main.urs. Error is the same. By the
way, I had to remove 'datatype lang = Ru | En' from the design since
it is not visible from main.ur if moved to main.urs.

> I'm still planning to look into your previous issue.

I'm looking forward to trying new things.

Regards,
Sergey

--- Code ---

[1] - https://github.com/grwlf/foocms/tree/master/tst/first-class-link-expr-4

fun main' (l:lang) = let
  val reloader = fn (l':lang) => <xml><p><a link={main' l'}>Switch to
{[l]}</a></p></xml>
  in return (template reloader l) end

and template reload (l:lang) =
   <xml>
     <head>
       <title>MultyLang page</title>
     </head>
     <body>
       <h1>The body</h1>
       <p>Current page is in {[l]}</p>
       <p>The content</p>
       <p>Other languages:</p>
       {reload "Ru"}
       {reload "En"} (* Compiles if one remove second call to reload *)
     </body>
   </xml>

fun main {} = main' "En"