[Ur] constructor-level constraints and more

[Sergey Mironov]

Hi. A question about Ur's type-level facilities: I have a function
`add' which adds a field #JQ to the record `t'.


con dpage = fn deps => [ Hdr = record deps, Bdy = transaction page]

val add : t ::: {Type}
  -> css_class
  -> [t ~ [JQ]] => record (dpage (t ++ [JQ = url]))
  -> record (dpage (t ++ [JQ = url]))

it works, but since I'm going to write many different adders, I'd like
to make their signatures shorter. My plan was to add a shorthand for
`record (dpage (t ++ [JQ = url]))' like this:

con my = fn t => record (dpage (t++[JQ=url]))

and then rewrite `add' as

val add : t ::: {Type}
  -> css_class
  -> [t ~ [JQ]] => my t
  -> my t


Unfortunately, Ur doesn't allow me to do that. Even `con my ..' line
alone issues the error:


dev:[grwlf at greyblade:~/proj/urdesign]$ urweb -dbms sqlite App && ./App.exe
/home/grwlf/proj/urdesign/src/menu_jq/Menu_jq.ur:16:41: (to 16:54)
Couldn't prove field name disjointness
    Con 1:  t
    Con 2:  [JQ = ()]
Hnormed 1:  t
Hnormed 2:  [JQ = ()]

Naturally, `con my' doesn't have a constraint and I don't know how to
add it. Is there a solution? Do we have a general quick way to say
that record r contains field n?

Regards,
Sergey