Possible bug in unification

[fehrenbach]

I get this somewhat confusing error message.
Is this a bug in the unification code, or could someone explain to me what's wrong with my code?

Unification error: Rows
 |_
and
 |_
 could not be unified because one is closed and the other has a rigid row variable
Unification error: Couldn't match ((id:Int,parent:Int,schema:Int,value:String|_)) -> Bool against ((id:Int,parent:Int,schema:Int,value:String|_)) {}-@ _::Any
/home/stefan/src/dbwiki/xpath.links:287: Type error: The function
    `filter'
has type
    `((id:Int,parent:Int,schema:Int,value:String|_)) -> Bool'
while the arguments passed to it have types
    `(id:Int,parent:Int,schema:Int,value:String|_)'
and the currently allowed effects are
    `'.
In expression: filter(r).

[fehrenbach]

As small as an example as I can manage:

var db = database "stefan";

var exists = compose(not, empty);

typename Data = (parent : Int, value  : String);

typename CompilationContext = TableHandle(Data,Data,Data);

sig filterConstraint : (CompilationContext) ~> (Data) -> Bool
fun filterConstraint (data) {
  var aa = fun (x) {
             for (text <-- data)
             where ( true )
               [(val = text.value)]
             };
  fun (x) {
    exists(
      for (a <- aa(x))
      where (a.val == "b")
        [()]
    )
  }
}

var data = table ("ciawfb_data") with Data from db;
var filter = filterConstraint(data);
query {
  for (r <-- data)
  where (filter(r))
    [r]
}

Replacing sig filterConstraint : (CompilationContext) ~> (Data) -> Bool by sig filterConstraint : (CompilationContext) ~> (Data) {}-> Bool "fixes" the problem.

[slindley]

Here's a smaller example:

var exists = compose(not, empty);

sig filterConstraint : () -> Bool
fun filterConstraint () {
  exists([()])
}

query {
  [(x=filterConstraint())]
}

There is a bug in Links in the way it is reporting the bug in your program. The bug in your program is that due to the ML value restriction, exists is not polymorphic in its effects, but filterConstraint is declared to have a type that is polymorphic in its effects. The solution is to eta expand exists:

fun exists(xs) {not(empty(xs))}

or:

var exists = fun (xs) {compose(not, empty)(xs)};

In fact, we could, and perhaps should relax the value restriction in the case of pure functions (like compose, pure, and empty), in which case your original program would work.

[fehrenbach]

Thanks, I fixed my code :-)
Now I'll have to do some reading on the value restriction.