[Ur] need help with unification and field name disjointness proof failures

[Marko Schütz Schmuck]

The attached source is giving me some type related errors. I'd very
much appreciate some help ...

Thanks,

Marko

password.ur
Description: Binary data

/home/marko/myStuff/Projects/AssignTAs/sandbox/password.ur:56:4: (to 67:0) 
Error in final record unification
Can't unify record constructors
Have:
<UNIF:U490::{Type}> ++ [Salt = option string, PasswordHash = string]
Need:
[User =
  {Salt : option string, PasswordHash : string, Username : string}]
/home/marko/myStuff/Projects/AssignTAs/sandbox/password.ur:56:4: (to 67:0) 
Stuck unifying these records after canceling matching pieces:
Have:
([Salt = option string, PasswordHash = string]) ++
 <UNIF:U490::{Type}>
Need:
[User =
  $((fn fields :: ({Type} * {Type}) => fields.1)
     (([Salt = option string]) ++
       ([PasswordHash = string]) ++ [Username = string], []))]
/home/marko/myStuff/Projects/AssignTAs/sandbox/password.ur:55:0: (to 67:0) Some 
constructor unification variables are undetermined in declaration
(look for them as "<UNIF:...>")
Decl:

.....
      ([Username = string]) ++
                    ([]) ++ [Salt = option string, PasswordHash = string]]) ++
                 ([]) ++ []] [[]] [[]] [string] [string] [bool]
               (Basis.sql_eq [string])
               (Basis.sql_field [([]) ++ []]
                 [([]) ++ [Salt = option string, PasswordHash = string]]
                 [string] [[]] [[]] [#User] [#Username])
               (Basis.sql_inject
                 [([User =
                     ([Username = string]) ++
                      ([]) ++ [Salt = option string, PasswordHash = string]])
                   ++ ([]) ++ []] [[]] [[]] [string]
                 Basis.sql_prim [string] Basis.sql_string r.#User),
             GroupBy =
              Basis.sql_subset_all
               [[User =
                  ([Username = string]) ++
                   ([]) ++ [Salt = option string, PasswordHash = string]]],
             Having =
              Basis.sql_inject
               [([]) ++
                 [User =
                   ([Username = string]) ++
                    ([]) ++ [Salt = option string, PasswordHash = string]]]
               [([]) ++
                 [User =
                   ([Username = string]) ++
                    ([]) ++ [Salt = option string, PasswordHash = string]]]
               [[]] [bool] Basis.sql_prim [bool] Basis.sql_bool Basis.True,
             SelectFields =
              Basis.sql_subset
               [[User =
                  (([Salt = option string]) ++
                    ([PasswordHash = string]) ++ [Username = string], [])]],
             SelectExps = {}},
          OrderBy =
           Basis.sql_order_by_Nil
            [([]) ++
              [User =
                ([Username = string]) ++
                 ([]) ++ [Salt = option string, PasswordHash = string]]] [[]],
          Limit = Basis.sql_no_limit, Offset = Basis.sql_no_offset}))
    (fn thisUser :
      option
       $(([Salt = option string]) ++
          ([PasswordHash = string]) ++ <UNIF:U490::{Type}>) =>
      case thisUser of
       None =>
        return [transaction] [option string] Basis.transaction_monad
         (None [string]) |
        Some u =>
         case u.#Salt of
          None =>
           return [transaction] [option string] Basis.transaction_monad
            (None [string]) |
           Some s =>
            case
             Basis.eq [string] Basis.eq_string u.#PasswordHash
              (crypt r.#Pass s) of
             Basis.True =>
              return [transaction] [option string] Basis.transaction_monad
               (Some [string] r.#User) |
              Basis.False =>
               return [transaction] [option string] Basis.transaction_monad
                (None [string]))

.....

/home/marko/myStuff/Projects/AssignTAs/sandbox/password.ur:63:15: (to 63:29) 
Couldn't prove field name disjointness
    Con 1:  [PasswordHash = string]
    Con 2:  ([Salt = option string]) ++ <UNIF:U490::{Type}>
Hnormed 1:  [PasswordHash = string]
Hnormed 2:  ([Salt = option string]) ++ <UNIF:U490::{Type}>
/home/marko/myStuff/Projects/AssignTAs/sandbox/password.ur:60:13: (to 60:19) 
Couldn't prove field name disjointness
    Con 1:  [Salt = option string]
    Con 2:  ([PasswordHash = string]) ++ <UNIF:U490::{Type}>
Hnormed 1:  [Salt = option string]
Hnormed 2:  ([PasswordHash = string]) ++ <UNIF:U490::{Type}>

pgpb2KEC0eGOk.pgp
Description: OpenPGP Digital Signature

_______________________________________________
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur