Comparing objects sometimes gives compiler type errors

[patrick-east]

Expected Behavior

Comparing two objects should just give a boolean result, for example:

{"a": 1, "b": 2, "c": 3} == {"a": 1, "b": 2, "c": 3}

Should be true, and

{"a": 1, "b": 2, "c": 3} == {"x": false}

Should not be true

Actual Behavior

{"a": 1, "b": 2, "c": 3} == {"a": 1, "b": 2, "c": 3}

is true

{"a": 1, "b": 2, "c": 3} == {"x": false}

gives a compiler error:

1 error occurred: policy.rego:8: rego_type_error: match error
	left  : object<a: number, b: number, c: number>
	right : object<x: boolean>

Ex: https://play.openpolicyagent.org/p/5UvgQRkvir

Additional Info

If at least one side of the comparison is unknown then it works as expected, ex: https://play.openpolicyagent.org/p/bcRCXMnUuU so the underlying comparison is fine. It seems like the type check in the compiler is maybe too aggressive in this case. It isn't wrong in that they are indeed different... but it should probably let this one go to keep behavior consistent instead of bailing out early with the error.

[timothyhinrichs]

There are some corner cases where this behavior is a bit annoying, but typically it comes up when we're doing something we'd never do for real. If the type system finds a type mismatch it should throw the error.

One question is whether there should be a type error on == if we compare two variables of different types. Go certainly treats that as a type error; so too should Rego.

Another question is whether the types are too fine-grained. Because OPA is JSON-centric the types are basically JSON-schema. Two variables are of different types if they are known to have different fields. Programming languages typically just make you create names for each type and complain if two variables in == have different type names. OPA types are more semantic.

If we were to relax the notion of a type to just basically object, array, number, string, etc. then we wouldn't get errors thrown when someone references a field that obviously doesn't exist. Example:

# Throws an error today at x.c.  
# Would not throw an error if relaxed type of x to "object"
hello {
    x := {"a": 1, "b": 2}
    x.c == 3
}

Once we allow base documents (like input) to have their schemas declared, type inference will naturally eliminate references to fields that cannot exist (e.g. it will check that input.user is a valid reference).

Perhaps further, the question becomes should the object type have an extensible and fixed version? The Extensible version would say that the fields included will always exist but there could be more. The Fixed version would say that the fields included are exactly the fields that must exist. But even if we had those two versions, I'd expect that the type inference would treat the hard-coded object {"a": 1, "b": 2} as fixed because we know exactly what the fields could be.

[tsandall]

Perhaps further, the question becomes should the object type have an extensible and fixed version? The Extensible version would say that the fields included will always exist but there could be more. The Fixed version would say that the fields included are exactly the fields that must exist. But even if we had those two versions, I'd expect that the type inference would treat the hard-coded object {"a": 1, "b": 2} as fixed because we know exactly what the fields could be.

Objects and arrays are typed this way today. They have a "static" portion and a "dynamic" portion. The static portion is the fixed set of object properties or array elements elements . The dynamic portion is the extensible set of properties or array elements. I don't think it's possible to construct an array that has both static and dynamic elements, but it is possible to create an object with static and dynamic properties. For example:

> x = "foo"; obj = {x: 1, "bar": 2}
-----8<SNIP>8-----
# obj: object<bar: number>[string: number]

OPA uses uses <> to denote static fields and [] to denote dynamic fields.

Re: the original issue, I'd argue the type checker is not aggressive enough in dealing with the function case. The problem is that the type checker relies on the rules being topologically sorted and processes them bottom up. That said, it could easily break people to introduce stricter type checking so I'm not sure there's anything to be done here.

[patrick-east]

You guys make some excellent points. I'm happy to close this out if the consensus is that it is working as expected.

I tend to disagree that a compile error is the best behavior for these cases, with the example

hello {
    x := {"a": 1, "b": 2}
    x.c == 3
}

I could see us making peoples lives easier by saying that yes, we know c doesn't exist on x so we raise an error. Thats fine by me.

The concern I have, specific to the original issue of comparing objects, is that by having it spit out a compile error it makes for a less than ideal user experience. How is a user supposed to interpret:

1 error occurred: policy.rego:8: rego_type_error: match error
	left  : object<a: number, b: number, c: number>
	right : object<x: boolean>

And infer that yes, you actually can compare those, but just not written this way. The immediate implication is that you cannot compare objects with ==. It might make a lot of sense if you're a rego expert.. but for someone new to the language, or even myself that is at least somewhat experienced, it is confusing and you start wondering how you are supposed to actually compare objects. The error message is hiding the reality that they are comparable, you did write valid rego, but the type checker eagerly evaluated that no, they are infact not the same and cannot be equal. As a user I would expect the evaluation itself to determine that.

[timothyhinrichs]

I'm happy to leave this issue open, as I've had to work around the type-checker multiple times. It's more a question of whether there's a slice of type-checking that could be turned off that would on balance improve the user experience.

On Mon, Feb 24, 2020 at 4:22 PM Patrick East [email protected] wrote:

You guys make some excellent points. I'm happy to close this out if the consensus is that it is working as expected.

I tend to disagree that a compile error is the best behavior for these cases, with the example

hello { x := {"a": 1, "b": 2} x.c == 3 }

I could see us making peoples lives easier by saying that yes, we know c doesn't exist on x so we raise an error. Thats fine by me.

The concern I have, specific to the original issue of comparing objects, is that by having it spit out a compile error it makes for a less than ideal user experience. How is a user supposed to interpret:

1 error occurred: policy.rego:8: rego_type_error: match error left : object<a: number, b: number, c: number> right : object<x: boolean>

And infer that yes, you actually can compare those, but just not written this way. The immediate implication is that you cannot compare objects with ==. It might make a lot of sense if you're a rego expert.. but for someone new to the language, or even myself that is at least somewhat experienced, it is confusing and you start wondering how you are supposed to actually compare objects. The error message is hiding the reality that they are comparable, you did write valid rego, but the type checker eagerly evaluated that no, they are infact not the same and cannot be equal. As a user I would expect the evaluation itself to determine that.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/open-policy-agent/opa/issues/2132?email_source=notifications&email_token=ACMVQK2B3UN4Y5WXLMP3SJLRERQE5A5CNFSM4KZKDCZ2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEM2BQKQ#issuecomment-590616618, or unsubscribe https://github.com/notifications/unsubscribe-auth/ACMVQKYHKEQC62IBUO7RM63RERQE5ANCNFSM4KZKDCZQ .

[anderseknert]

This came up today, having both the user and me scratching our heads before eventually landing here, with a friendly pointer from @srenatus. I think it would have saved us a lot of time if the type error message came with a link to a page explaining the Rego type checker, and why an object comparison would throw a type error and not just fail "silently" like expected.

[stale[bot]]

This issue has been automatically marked as inactive because it has not had any activity in the last 30 days.

[anderseknert]

I haven't seen it mentioned, so if someone struggles with this, here's how you can fool the type checker with this one simple trick!

a := {"foo": 1}
b := {"foo": "bar"}

test_a_eq_b {
    a == b
}

Type error.

a := {"foo": 1}
b := {"foo": "bar"}

test_a_eq_b {
    untyped_equals(a, b)
}

untyped_equals(o1, o2) := o1 == o2

Test works (and fails, as expected).

[stale[bot]]

This issue has been automatically marked as inactive because it has not had any activity in the last 30 days. Although currently inactive, the issue could still be considered and actively worked on in the future. More details about the use-case this issue attempts to address, the value provided by completing it or possible solutions to resolve it would help to prioritize the issue.