[Ur] simple example about constructing rects - guarded types?

[Marc Weber]

I want to build a simple type constructor: It takes two names and two
types and should build the record type {name1 = type1, name2 = type2}

So this is the trivial implementation (?)

con build_record :: Name      -> Name   -> Type      -> Type  -> {Type}
                  = fn  (a::Name)   (b::Name)  (c::Type) (d::Type) => [ a = c ] ++ [ b = d]


And of course urweb can't proof that name1 differs from name2:

  typeexperiments.ur|16 col 69| 16:78: Couldn't prove field name disjointness
  ||     Con 1:  [a = ()]
  ||     Con 2:  [b = ()]
  || Hnormed 1:  [a = ()]
  || Hnormed 2:  [b = ()]

So how to fix is? Is this a case where guarded types must be used?
I couldn't find out how to apply it here.


Also looking at this example:
http://impredicative.com/wiki/index.php/Using_Top.Fold_to_count_fields_of_a_record:

  con rr :: {Type} = [One = int, Two = string, Three = bool, Four = list float] 

  val q : int = @@fold [fn (rx :: {Type}) => (int)]
                  (fn [nm :: Name] [t :: Type] [r :: {Type}] [[nm] ~ r] acc => 1 + acc)
                  (0) [rr] (_ : folder rr)

I don't understand why the arguments of the fn lambda are put in square
brackets.

Is this the "polymorphic function abstraction":
  lambda [x ? kappa] => e

which is listed in the expression section of the manual?

Marc Weber