Skip to content

Commit

Permalink
Make type annotations to not propagate through merging (#1271)
Browse files Browse the repository at this point in the history 
* First draft of making type not propagating

* Consider record types as such whenever possible

Before this change, a record literal was considered a record type
whenever it met a bunch of conditions AND was used in a type position.
This meant that `{foo : Number, bar : String}` was always considered as
a normal record (fields without definition) when used in a term
position. This was already subtly wrong, because this means for example
that `x | {foo : Number}` and `let C = {foo : Number} in x | C` are
operationally not equivalent.

Now that we've made a stronger distinction between static types and
contracts (types don't propagate through merging), then this behavior
is just unsound. As per this commit, a record literal is considered a
record type whenever it satisfies the syntactic conditions, be it in a
type or a term position.

Additionally, we've forbidden "mixed" style records, that is record
literals that are not a record type, but with fields that have a type
annotation and no definition. Beside being meaningless, they can be
deceiving, and are most often an error or a confusion from users. Either
the should use a record type, or use `|` everywhere, as in a record
contract.

* Fix tests after forbidding typed fields without definition

* More tests on types vs contracts propagation

* Formatting

* Apply suggestions from code review

Co-authored-by: Viktor Kleen <viktor.kleen@tweag.io>

* Update snapshot test output after typo fixup

---------

Co-authored-by: Viktor Kleen <viktor.kleen@tweag.io>
  • Loading branch information
@yannham @vkleen
yannham and vkleen authored Apr 21, 2023
1 parent bdc5f08 commit 116fdb3
Show file tree
Hide file tree
Showing 19 changed files with 408 additions and 87 deletions.
44 changes: 44 additions & 0 deletions src/error.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -385,6 +385,26 @@ pub enum ParseError {
/// - a variable is used as both a record and enum row variable, e.g. in the
/// signature `forall r. [| ; r |] -> { ; r }`.
TypeVariableKindMismatch { ty_var: Ident, span: RawSpan },
/// A record literal, which isn't a record type, has a field with a type annotation but without
/// a definition. While we could technically handle this situation, this is most probably an
/// error from the user, because this type annotation is useless and, maybe non-intuitively,
/// won't have any effect as part of a larger contract:
///
/// ```nickel
/// let MixedContract = {foo : String, bar | Number} in
/// { foo = 1, bar = 2} | MixedContract
/// ```
///
/// This example works, because the `foo : String` annotation doesn't propagate, and contract
/// application is mostly merging, which is probably not the intent. It might become a warning
/// in a future version, but we don't have warnings for now, so we rather forbid such
/// constructions.
TypedFieldWithoutDefinition {
/// The position of the field definition.
field_span: RawSpan,
/// The position of the type annotation.
annot_span: RawSpan,
},
}

/// An error occurring during the resolution of an import.
Expand Down Expand Up @@ -550,6 +570,13 @@ impl ParseError {
InternalParseError::TypeVariableKindMismatch { ty_var, span } => {
ParseError::TypeVariableKindMismatch { ty_var, span }
}
InternalParseError::TypedFieldWithoutDefinition {
field_span,
annot_span,
} => ParseError::TypedFieldWithoutDefinition {
field_span,
annot_span,
},
},
}
}
Expand Down Expand Up @@ -1561,6 +1588,23 @@ impl IntoDiagnostics<FileId> for ParseError {
String::from("Type variables may be used either as types, polymorphic record tails, or polymorphic enum tails."),
String::from("Using the same variable as more than one of these is not permitted.")
]),
ParseError::TypedFieldWithoutDefinition { field_span, annot_span } => {
Diagnostic::error()
.with_message("statically typed field without a definition")
.with_labels(vec![
primary(&field_span).with_message("this field doesn't have a definition"),
secondary(&annot_span).with_message("but it has a type annotation"),
])
.with_notes(vec![
String::from("A static type annotation must be attached to an expression but \
this field doesn't have a definition."),
String::from("Did you mean to use `|` instead of `:`, for example when defining a record contract?"),
String::from("Typed fields without definitions are only allowed inside \
record types, but the enclosing record literal doesn't qualify as a \
record type. Please refer to the manual for the defining conditions of a \
record type."),
])
}
};

vec![diagnostic]
Expand Down
4 changes: 2 additions & 2 deletions src/eval/fixpoint.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -85,7 +85,7 @@ pub fn rec_env<'a, I: Iterator<Item = (&'a Ident, &'a Field)>, C: Cache>(
let id_value = Ident::fresh();
final_env.insert(id_value, idx);

let with_ctr_applied = PendingContract::apply_all(
let with_ctr_applied = RuntimeContract::apply_all(
RichTerm::new(Term::Var(id_value), value.pos),
field.pending_contracts.iter().cloned().flat_map(|ctr| {
// This operation is the heart of our preliminary fix for
Expand All @@ -112,7 +112,7 @@ pub fn rec_env<'a, I: Iterator<Item = (&'a Ident, &'a Field)>, C: Cache>(
} else {
vec![
ctr.clone(),
PendingContract {
RuntimeContract {
contract: ctr.contract,
label: Label {
polarity: ctr.label.polarity.flip(),
Expand Down
8 changes: 4 additions & 4 deletions src/eval/merge.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -646,24 +646,24 @@ impl RevertClosurize for Field {
}
}

impl RevertClosurize for PendingContract {
impl RevertClosurize for RuntimeContract {
fn revert_closurize<C: Cache>(
self,
cache: &mut C,
env: &mut Environment,
with_env: Environment,
) -> PendingContract {
) -> RuntimeContract {
self.map_contract(|ctr| ctr.revert_closurize(cache, env, with_env))
}
}

impl RevertClosurize for Vec<PendingContract> {
impl RevertClosurize for Vec<RuntimeContract> {
fn revert_closurize<C: Cache>(
self,
cache: &mut C,
env: &mut Environment,
with_env: Environment,
) -> Vec<PendingContract> {
) -> Vec<RuntimeContract> {
self.into_iter()
.map(|pending_contract| pending_contract.revert_closurize(cache, env, with_env.clone()))
.collect()
Expand Down
10 changes: 5 additions & 5 deletions src/eval/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -87,7 +87,7 @@ use crate::{
array::ArrayAttrs,
make as mk_term,
record::{Field, RecordData},
BinaryOp, BindingType, LetAttrs, PendingContract, RichTerm, StrChunk, Term, UnaryOp,
BinaryOp, BindingType, LetAttrs, RichTerm, RuntimeContract, StrChunk, Term, UnaryOp,
},
transform::Closurizable,
};
Expand Down Expand Up @@ -253,7 +253,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
value_next = value_next
.map(|value| -> Result<RichTerm, EvalError> {
let pos_value = value.pos;
let value_with_ctr = PendingContract::apply_all(
let value_with_ctr = RuntimeContract::apply_all(
value,
pending_contracts.into_iter(),
pos_value,
Expand Down Expand Up @@ -649,7 +649,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
.pending_contracts
.iter()
.map(|ctr| {
PendingContract::new(
RuntimeContract::new(
ctr.contract.clone().closurize(
&mut self.cache,
&mut local_env,
Expand Down Expand Up @@ -688,10 +688,10 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
// avoiding repeated contract application. Annotations could then be a good way of
// remembering which contracts have been applied to a value.
Term::Annotated(annot, inner) => {
let contracts = annot.as_pending_contracts()?;
let contracts = annot.pending_contracts()?;
let pos = inner.pos;
let inner_with_ctr =
PendingContract::apply_all(inner.clone(), contracts.into_iter(), pos);
RuntimeContract::apply_all(inner.clone(), contracts.into_iter(), pos);

Closure {
body: inner_with_ctr,
Expand Down
30 changes: 15 additions & 15 deletions src/eval/operation.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,8 +27,8 @@ use crate::{
make as mk_term,
record::{self, Field, FieldMetadata, RecordData},
string::NickelString,
BinaryOp, CompiledRegex, IndexMap, MergePriority, NAryOp, Number, PendingContract,
RecordExtKind, RichTerm, SharedTerm, StrChunk, Term, UnaryOp,
BinaryOp, CompiledRegex, IndexMap, MergePriority, NAryOp, Number, RecordExtKind, RichTerm,
RuntimeContract, SharedTerm, StrChunk, Term, UnaryOp,
},
transform::Closurizable,
};
Expand Down Expand Up @@ -526,7 +526,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
let ts = ts
.into_iter()
.map(|t| {
let t_with_ctrs = PendingContract::apply_all(
let t_with_ctrs = RuntimeContract::apply_all(
t,
attrs.pending_contracts.iter().cloned(),
pos.into_inherited(),
Expand Down Expand Up @@ -695,7 +695,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
let terms =
seq_terms(
ts.into_iter().map(|t| {
let t_with_ctr = PendingContract::apply_all(
let t_with_ctr = RuntimeContract::apply_all(
t,
attrs.pending_contracts.iter().cloned(),
pos.into_inherited(),
Expand Down Expand Up @@ -1043,7 +1043,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
.map(|t| {
mk_term::op1(
UnaryOp::Force { ignore_not_exported },
PendingContract::apply_all(
RuntimeContract::apply_all(
t,
attrs.pending_contracts.iter().cloned(),
pos.into_inherited(),
Expand Down Expand Up @@ -1725,12 +1725,12 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
.filter(|ctr| !ctrs_left.contains(ctr) && !ctrs_common.contains(ctr));

ts.extend(ts1.into_iter().map(|t|
PendingContract::apply_all(t, ctrs_left.iter().cloned(), pos1)
RuntimeContract::apply_all(t, ctrs_left.iter().cloned(), pos1)
.closurize(&mut self.cache, &mut env, env1.clone())
));

ts.extend(ts2.into_iter().map(|t|
PendingContract::apply_all(t, ctrs_right.clone(), pos2)
RuntimeContract::apply_all(t, ctrs_right.clone(), pos2)
.closurize(&mut self.cache, &mut env, env2.clone())
));

Expand Down Expand Up @@ -1763,7 +1763,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
return Err(EvalError::Other(format!("elem_at: index out of bounds. Expected an index between 0 and {}, got {}", ts.len(), n), pos_op));
}

let elem_with_ctr = PendingContract::apply_all(
let elem_with_ctr = RuntimeContract::apply_all(
ts.get(n_as_usize).unwrap().clone(),
attrs.pending_contracts.iter().cloned(),
pos1.into_inherited(),
Expand Down Expand Up @@ -1973,7 +1973,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {

let array_with_ctr = Closure {
body: RichTerm::new(
Term::Array(ts, attrs.with_extra_contracts([PendingContract::new(rt3, lbl)])),
Term::Array(ts, attrs.with_extra_contracts([RuntimeContract::new(rt3, lbl)])),
pos2,
),
env: env2,
Expand Down Expand Up @@ -2020,7 +2020,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
};

for (id, field) in record_data.fields.iter_mut() {
field.pending_contracts.push(PendingContract {
field.pending_contracts.push(RuntimeContract {
contract: contract_at_field(*id),
label: label.clone(),
});
Expand Down Expand Up @@ -2989,12 +2989,12 @@ fn eq<C: Cache>(
let pos1 = value1.pos;
let pos2 = value2.pos;

let value1_with_ctr = PendingContract::apply_all(
let value1_with_ctr = RuntimeContract::apply_all(
value1,
pending_contracts1.into_iter(),
pos1,
);
let value2_with_ctr = PendingContract::apply_all(
let value2_with_ctr = RuntimeContract::apply_all(
value2,
pending_contracts2.into_iter(),
pos2,
Expand Down Expand Up @@ -3049,14 +3049,14 @@ fn eq<C: Cache>(
.into_iter()
.map(|t| {
let pos = t.pos.into_inherited();
PendingContract::apply_all(t, a1.pending_contracts.iter().cloned(), pos)
RuntimeContract::apply_all(t, a1.pending_contracts.iter().cloned(), pos)
.closurize(cache, &mut shared_env1, env1.clone())
})
.collect::<Vec<_>>()
.into_iter()
.zip(l2.into_iter().map(|t| {
let pos = t.pos.into_inherited();
PendingContract::apply_all(t, a2.pending_contracts.iter().cloned(), pos)
RuntimeContract::apply_all(t, a2.pending_contracts.iter().cloned(), pos)
.closurize(cache, &mut shared_env2, env2.clone())
}))
.collect::<Vec<_>>();
Expand Down Expand Up @@ -3140,7 +3140,7 @@ where
.value
.map(|value| {
let pos = value.pos;
let value_with_ctrs = PendingContract::apply_all(
let value_with_ctrs = RuntimeContract::apply_all(
value,
field.pending_contracts.iter().cloned(),
pos,
Expand Down
20 changes: 20 additions & 0 deletions src/parser/error.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,4 +44,24 @@ pub enum ParseError {
/// - a variable is used as both a record and enum row variable, e.g. in the
/// signature `forall r. [| ; r |] -> { ; r }`.
TypeVariableKindMismatch { ty_var: Ident, span: RawSpan },
/// A record literal, which isn't a record type, has a field with a type annotation but without
/// a definition. While we could technically handle this situation, this is most probably an
/// error from the user, because this type annotation is useless and, maybe non-intuitively,
/// won't have any effect as part of a larger contract:
///
/// ```nickel
/// let MixedContract = {foo : String, bar | Number} in
/// { foo = 1, bar = 2} | MixedContract
/// ```
///
/// This example works, because the `foo : String` annotation doesn't propagate, and contract
/// application is mostly merging, which is probably not the intent. It might become a warning
/// in a future version, but we don't have warnings for now, so we rather forbid such
/// constructions.
TypedFieldWithoutDefinition {
/// The position of the field definition (the identifier only).
field_span: RawSpan,
/// The position of the type annotation.
annot_span: RawSpan,
},
}
Loading

0 comments on commit 116fdb3

Please sign in to comment.