Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix unsound record contract deduplication #2042

Merged
merged 4 commits into from
Sep 16, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
53 changes: 51 additions & 2 deletions core/src/typecheck/eq.rs
Original file line number Diff line number Diff line change
Expand Up @@ -548,20 +548,69 @@ fn erows_as_map<E: TermEnvironment>(

/// Check for contract equality between record fields. Fields are equal if they are both without a
/// definition, or are both defined and their values are equal.
///
/// The attached metadata must be equal as well: most record contracts are written as field with
/// metadata but without definition. For example, take `{ foo | {bar | Number}}` and `{foo | {bar |
/// String}}`. Those two record contracts are obviously not equal, but to know that, we have to
/// look at the contracts of each bar field.
fn contract_eq_fields<E: TermEnvironment>(
state: &mut State,
field1: &Field,
env1: &E,
field2: &Field,
env2: &E,
) -> bool {
match (&field1.value, &field2.value) {
// Check that the pending contracts are equal.
//
// [^contract-eq-ignore-label]: We mostly ignore the label here, which doesn't impact the fact
// that a contract blame or not. Different labels might lead to different error messages,
// though. Note that there is one important exception: the field `type_environment` does impact
// the evaluation of the contract. Fortunately, it's a simple datastructure that is easy to
// compare, so we do check for equality here.
//
// Otherwise, comparing the rest of the labels seem rather clumsy (as labels store a wide
// variety of static and runtime data) and not very meaningful.
let pending_contracts_eq = field1
.pending_contracts
.iter()
.zip(field2.pending_contracts.iter())
.all(|(c1, c2)| {
c1.label.type_environment == c2.label.type_environment
&& contract_eq_bounded(state, &c1.contract, env1, &c2.contract, env2)
});

// Check that the type and contrat annotations are equal. [^contract-eq-ignore-label] applies
// here as well.
let annotations_eq = field1
.metadata
.annotation
.iter()
.zip(field2.metadata.annotation.iter())
.all(|(t1, t2)| {
t1.label.type_environment == t2.label.type_environment
&& type_eq_bounded(
state,
&GenericUnifType::from_type(t1.typ.clone(), env1),
env1,
&GenericUnifType::from_type(t2.typ.clone(), env2),
env2,
)
});

// Check that "scalar" metadata (simple values) are equals
let scalar_metadata_eq = field1.metadata.opt == field2.metadata.opt
&& field1.metadata.not_exported == field2.metadata.not_exported
&& field1.metadata.priority == field2.metadata.priority;

let value_eq = match (&field1.value, &field2.value) {
(Some(ref value1), Some(ref value2)) => {
contract_eq_bounded(state, value1, env1, value2, env2)
}
(None, None) => true,
_ => false,
}
};

pending_contracts_eq && annotations_eq && scalar_metadata_eq && value_eq
}

/// Perform the type equality comparison on types. Structurally recurse into type constructors and
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,49 @@
# test.type = 'error'
# eval = 'full'
#
# [test.metadata]
# error = 'EvalError::BlameError'

# Regression test for https://github.com/tweag/nickel/issues/1700
let outer = {
spec
| {
hostAliases | Number,
containers | Number,
},
}
in

let inner = {
spec
| {
hostAliases,
containers
| Array {
..
},
},
}
in

std.deep_seq
(
{
spec = {
hostAliases = "this should fail",
containers = [
{
name = "test",
image = "nginx",
ports = [
{
containerPort = 80,
name = "http"
}
],
}
]
}
} | inner | outer
)
true