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

Thu Dec 16 19:52:11 EST 2010

I tried solving the following task: Write function which maps a function
a -> b on all values of a record. Because I still have a to try and
error :) I tried splitting the task into pieces:

1) I started using a simple map only (works):
    val app : a ::: Type -> b ::: Type -> (a -> b) -> a -> b
    fun app [a] [b] f v1 = f v1 

2) create an id function ensuring the argument is a record.
    However I didn't get to trying to ensure its a record because
    this test case fails:

          == 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 (?!)

I'm sure I'm missing something obvious again - or nobody ever tried
writing a simple id function before (?)

Is this a bug?

Marc Weber