[Ur] couldn't prove field name disjointness compile error

Adam Chlipala adamc at impredicative.com
Thu Dec 31 17:24:04 EST 2009


Daniel Patterson wrote:
> it errors with the following:
>
> userpass.ur:35:4-35:15: Couldn't prove field name disjointness
>      Con 1:  [#Password = Basis.string]
>      Con 2:  ([#Salt = Basis.string]) ++<UNIF:U898::{Type}>
> Hnormed 1:  [#Password = Basis.string]
> Hnormed 2:  ([#Salt = Basis.string]) ++<UNIF:U898::{Type}>
>
> Is this something that I can fix with explicit typing (if so how)? I'm
> confused because it is saying that they are disjointed (which I read as
> mismatched types), but they are all Basis.string's (which is what strcat
> takes)...
>    

"Disjoint" means "not sharing any record field names."  The unification 
variable [U898] is undetermined, so it's impossible to prove that it 
doesn't use the name [Password].  Such a fact is usually not very 
helpful directly; diagnosis depends on context.

The code you've included in your message does not occur in the web 
interface you linked to, so it's hard for me to give an exact 
recommendation.  You're probably trying to select field [Password] from 
a record that calls that field [Salt] instead, or vice versa.



More information about the Ur mailing list