[Ur] Unification Problems

[Adam Chlipala]

On 10/21/2012 07:04 PM, David Snider wrote:
> What I'm trying to figure out is why I have to put an explicit type here:
>
> fun checkPassword (r : {Email : string, Password : string}) =
>
> instead of just using:
> fun checkPassword r =

The reason is that the annotation-free version is ambiguous and doesn't 
uniquely determine the type of the function.  All functions must have 
uniquely determined types in Ur.

Presumably you want to call [checkPassword] from other modules, so you'd 
want to include a declaration for it in the .urs file, anyway, in which 
case the annotation in the .ur file is unnecessary.