CategoricalData / CQL

Categorical Query Language IDE
http://categoricaldata.net
299 stars 22 forks source link

"Cannot infer a unique well-sorted term" error #37

Closed nolta closed 5 years ago

nolta commented 5 years ago

Sorry if this is a naive question, but I'm wondering why the following schema throws an error:

schema S = literal : empty {
    entities
        A
        B
        C
        D
    foreign_keys
        x : A -> C
        x : B -> C
        y : A -> D
        y : B -> D
        y : C -> D
    path_equations
        A.x.y = A.y
        B.x.y = B.y
}
In equation A.x.y = A.y, Cannot infer a unique well-sorted term for y(x(v)) = y(v).
Candidates: FK v.x[class catdata.aql.exp.Fk].y[class catdata.aql.Term] = FK v[class catdata.aql.exp.Fk].y[class catdata.aql.Term]
FK v.x[class catdata.aql.exp.Fk].y[class catdata.aql.Term] = FK v[class catdata.aql.exp.Fk].y[class catdata.aql.Term]

I'm using the 2019-08-23 version of CQL.

drever commented 5 years ago

When you disambiguate the foreign keys x to e.g. x1 and x2 it compiles. I'm not sure what you are going for with the path equations, but I'm still learning CQL myself.

nolta commented 5 years ago

If the path_equations syntax matched observation_equations, then I could understand the error:

path_equations:
    forall e. e.x.y = e.y

But superficially A.x.y = A.y doesn't seem ambiguous.

wisnesky commented 5 years ago

Path equations were indeed first being translated into observation equations and then type inference was being performed, which in turn was not taking the given source entity into account. We've been moving away from type inference in general since it can be confusing when the same name can appear in multiple tables or types, so to fix I removed type inference from this step altogether. The example is not ambiguous and is working in the latest jar.

nolta commented 5 years ago

Thanks!

I've only been playing with CQL for a few days, but it's a really exciting project.