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

[Marc Weber]

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?
That's new to me.
So the types of declarations in .ur and .urs file are compared after
type checking has taken place ..

Marc Weber