Skip to content

Commit

Permalink
Add some explanation to src/eval/fixpoint.rs
Browse files Browse the repository at this point in the history
  • Loading branch information
vkleen committed Mar 24, 2023
1 parent 6b1450f commit e692ffb
Showing 1 changed file with 19 additions and 0 deletions.
19 changes: 19 additions & 0 deletions src/eval/fixpoint.rs
Original file line number Diff line number Diff line change
Expand Up @@ -88,6 +88,25 @@ pub fn rec_env<'a, I: Iterator<Item = (&'a Ident, &'a Field)>, C: Cache>(
let with_ctr_applied = PendingContract::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
// [#1161](https://github.com/tweag/nickel/issues/1161). Whenever we detect
// the presence of free type variables in a contract, by witnessing a nonempty
// type environment in the label, we need to not just apply the original
// contract but also its dual. The rationale here is that a record field that
// recursively depends on another of type `T`, say, should be considered a
// function with domain `T`. Consequently, the same contract that would be a
// applied to the argument of a function of type `T -> Dyn` should be applied
// to the recursive reference.
//
// Thus, the recursive reference must satisfy the contract for `T` as well as
// the "dual" contract `T.dualize()`; the latter is defined to be the domain
// contract for a function of type `T -> Dyn`. This sublety only matters if
// `T` contains free type variables because only then does `T.dualize()` differ
// from `T` at all.
//
// We expect to implement a way of solving this dilemma without essentially
// applying every contract twice. This will likely involve a rewriting of
// contracts corresponding to free variables which is yet to be proved sound.
if ctr.label.type_environment.is_empty() {
vec![ctr]
} else {
Expand Down

0 comments on commit e692ffb

Please sign in to comment.