[Ur] XML unification problem

[Sergey Mironov]

2013/8/9 Adam Chlipala <adamc at csail.mit.edu>:
> On 08/09/2013 08:32 AM, Sergey Mironov wrote:
>>
>> 2013/8/9 Adam Chlipala<adamc at csail.mit.edu>:
>>
>>
>>>
>>> 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..
>
>
> To be clear, I mean a type annotation on the formal parameter itself in the
> .ur file, not a full type at the function level in the .urs file, though the
> latter is good to have, too.

Bingo! Finally it works. Changing

    and template reload (l:lang) = ...

to

    and template (reload: lang -> atag) (l:lang) : page = ...

makes it compile without errors. Still, things is not that simple.
I've noticed that 'template' doesn't depend on main' any more and may
be moved to separate module. Unfortunately, it can't. If I declare
'template' as fun (instead of and) and move it to the beginning of
file, original error will come back. I think it is already a ticket to
register in mantis.

Regards,
Sergey