[Ur] kind syntax and semantics

[Gergely Buday]

Hi,

I am trying to code a simple function that augments a record with an {
Other : other } field. What am I doing wrong?

$ cat implicit.urs
val join : record ::: {Type} -> other ::: Type ->  [ #Other ~ record ] =>
          $record -> other -> $(record ++ [ Other = other ])

$ cat implicit.ur
fun join [record] [other] [ #Other ~ record ] (r:$record) (f:other) =
r ++ { Other = f }

$ urweb implicit
implicit.urs:1:53-1:59: Wrong kind
Constructor:  #Other
  Have kind:  Name
  Need kind:  {<UNIF:A>}
Incompatible kinds
Kind 1:  Name
Kind 2:  {<UNIF:A>}
implicit.ur:1:24-1:30: Wrong kind
Constructor:  #Other
  Have kind:  Name
  Need kind:  {<UNIF:G>}
Incompatible kinds
Kind 1:  Name
Kind 2:  {<UNIF:G>}
implicit.ur:1:24-1:30: Wrong kind
Constructor:  #Other
  Have kind:  Name
  Need kind:  {<UNIF:K>}
Incompatible kinds
Kind 1:  Name
Kind 2:  {<UNIF:K>}

- Gergely