[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