[Ur] sourcing a record

[Gergely Buday]

I stepped back to solve a simpler problem: an identity function on
records using fold.

fun identity [ r ::: {Type} ] (record : $r) : ($r) =
    fold [ fn t => $t ] (fn [nm ::_]  [ v::_] [r::_]  [[nm]~r] v => fn
acc => ({nm = v} ++ acc )) () record

but the compiler complains that I have too much arguments for the step function:

cellPull.ur:6:24-6:97: Unification failure
Expression:
fn nm :: Name =>
 fn v :: Type =>
  fn r :: {Type} =>
   fn v : $r => fn acc : $<UNIF:D::{Type}> => {nm = v} ++ acc
  Have con:
nm :: Name ->
 v :: Type ->
  r :: {Type} ->
   [[nm = ()] ~ r] =>
    ($r -> ($<UNIF:D::{Type}> -> $(([nm = $r]) ++ <UNIF:D::{Type}>)))
  Need con:
nm :: Name ->
 v :: Type ->
  r :: {Type} -> [[nm = ()] ~ r] => ($r -> $(([nm = v]) ++ r))
Incompatible constructors
Con 1:
($<UNIF:D::{Type}> -> $(([UNBOUND_REL2 = $r]) ++ <UNIF:D::{Type}>))
Con 2:  $(([UNBOUND_REL2 = UNBOUND_REL1]) ++ r)
cellPull.ur:6:4-6:100: Unification failure
Expression:
fold[[Type]] [(fn t :: {Type} => $t)]
 (fn nm :: Name =>
   fn v :: Type =>
    fn r :: {Type} =>
     fn v : $r => fn acc : $<UNIF:D::{Type}> => {nm = v} ++ acc) {}
 [<UNIF:I::{Type}>] _
  Have con:  $<UNIF:I::{Type}>
  Need con:  (<UNIF:J::Type> -> <UNIF:K::Type>)
Incompatible constructors
Con 1:  $<UNIF:I::{Type}>
Con 2:  (<UNIF:J::Type> -> <UNIF:K::Type>)

Why does it tell this? A proper step function should take the value
and the accumulator as arguments, but the "need con" section tells
that fold does not expect that. Or am I misunderstanding the error
message?

- Gergely