[Ur] How to implement top-level id function f a = a ?

[Adam Chlipala]

Marc Weber wrote:
> Excerpts from Adam Chlipala's message of Fri Dec 17 02:00:30 +0100 2010:
>    
>> Marc Weber wrote:
>>      
>>>             == main.urs ==
>>>             val main : unit ->   transaction page
>>>             val recIdTopLevel: a ::: Type ->   a ->   a
>>>        
>    
>> The important difference between the two definitions is that [recId] has
>> explicit type annotations for arguments and return type, while
>> [recIdTopLevel] doesn't.  Type inference for Ur is undecidable, so
>> sometimes you need to annotate to satisfy the type checker.
>>      
> So the type annotations in main.urs are for humans only?
>    

No, signatures hide details of implementations, just like in ML.  But 
the following is true, too:

> So the types of declarations in .ur and .urs file are compared after
> type checking has taken place ..
>    

That is, in checking a module, principal types are synthesized for all 
its components, then these types are checked for compatibility with the 
signature.  The error message you gave was generated before the first 
stage finished.