Improve precision when typechecking `==` about cedar HOT 4 OPEN

Implementing this in a backwards compatible manner requires #539

from cedar.

Updating this issue with some more rationale. The status quo is:

1. Expression User::"alice" == Action::"foo" has type False (you can compare two entities of different types)
2. Expression [1] == 1 is a type error (you cannot compare two non-entity values of different types), not type False

The reason for (1) is to handle the cross-product correctly (e.g., when you could have two different principal types you have to allow expressions like User::"bob" == Admin::"boss"), and the reason for (2) is to avoid the unsoundness of assuming two values of differing set types must be unequal (since the empty set [] can be given many possible Set<…> types).

To users, this may appear a little strange. It might appear less strange if we adjusted the behavior to be that e1 == e2 has

1. Type False when e1 and e2 have two different types and they are not both Set<…> types
2. Type Bool when they are both the same Set<T> type
3. Type-incorrect otherwise

This is more lenient and potentially a little easier to explain. A third option might be even better, but unfortunately will not work with analysis:

1. Type False when e1 and e2 have two different types and they are not both Set<…> types
2. Type Bool otherwise

The reason it won't work is that logical comparisons are strongly typed, i.e., both arguments must have the same type (including the same type for set elements).

from cedar.

I think there is a way to support the third option in the logical encoding too. So, let's keep the third option on the table for now. We have to think some about the encoding idea to make sure it actually works.

from cedar.

I think there is a way to support the third option in the logical encoding too. So, let's keep the third option on the table for now. We have to think some about the encoding idea to make sure it actually works.

On further reflection, the approach I had in mind doesn’t work in general. It will work for simple cases, for example a == b where the type of a is Set<String> and type of b is Set<Decimal>. In these situations, the encoding problem can be solved because there is only one way in which a and b can be equal: when they are both empty.

But with nested types, there are infinitely many ways for them to be equal, which means that we can’t enumerate them all. To see why, consider the situation where a has type Set<{ name: String, stuff : Set<Bool>}> and b has type Set<{ name: String, stuff : Set<Int>}>. Then a and b are equal if they are both empty, or they both consist of the same records of the form { name: …, stuff : []}. There are infinitely many such possibilities (because the String type is unbounded).

So, the third option is infeasible to encode efficiently (i.e., without quantifiers or other undecidable features).

from cedar.