[Ur] disjointness proof in type-level functions

[Sergey Mironov]

Ok, I finally become familiar with searching in mail archives . Looks
like disjointness proofs are impossible on type level.

2013/8/7 Sergey Mironov <grrwlf at gmail.com>:
> Hi. I faced a problem while exploring the type system. Looks like I
> can't define a constructor-level function which adds a field (of int
> type) to the record. I've tried to do the following:
>
>> con addIntField = fn (n :: Name) (t::{Type}) => [n = int] ++ t
>
> Ur complains about missing disjointness proof. I understand what it
> is, but what I don't know it how to add this proof. Is it ever
> possible on this level? All examples I've seen so far have such proof
> on value-level, like 'project' function from [1]. I need this to teach
> my app to define tables for custom records, adding primary key named
> Id, like
>
> con c_users = [ Name = string, Pass = string]
>
> ..
>
> table users : $(addIntField #Id c_users) PRIMARY KEY Id
>
> Regards,
> Sergey
>
> [1] - http://www.impredicative.com/ur/tutorial/tlc.html