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

Thu Dec 16 20:00:30 EST 2010

Marc Weber wrote:
>            == main.urs ==
>            val main : unit ->  transaction page
>            val recIdTopLevel: a ::: Type ->  a ->  a
>
>
>            == main.ur ==
>            fun recIdTopLevel [a] b = b
>
>            fun main () : transaction page =
>              let
>                fun recId [a ::: Type] (b:a) : a = b
>              in
>                return<xml><head></head>
>                    <body>
>                      {[ (recId 7) ]}<<  ok
>                      {[ (recIdTopLevel 7) ]}<<  fails see below
>                    </body>
>                  </xml>
>
>              end
>
>
>        ERROR:
>          main.ur|41 col 14| 41:27: Substitution in constructor is blocked by a too-deep unification variable
>          || Replacement:<UNIF:U127::<UNIF:X>>
>          ||        Body:  (<UNIF:P::Type>  ->  <UNIF:P::Type>)
>
>      Note: recIdTopLevel and recId should behave the same way.
>      However only recId compiles (?!)
>    

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.