Unify let-introduction in a single path

Remove branches on determining how let-bindings are introduced to the
scope. This is maybe a little more inefficient, but I think it is a huge
simplification.

One additional change this required was changing how fx suffixes are
checked. The current implementation would add additional constraints for
patterns in let bindings conditionally. However, this is unnecessary. I
believe it is sufficient to check the fx suffix by running the checks on
all introduced symbols after the type is well known (i.e. the body is
checked).
This commit is contained in:
Ayaz Hafiz 2025-01-01 21:46:11 -06:00
parent bd2dd66c96
commit 54cc5e4c29
No known key found for this signature in database
GPG key ID: 4EBD1C71C734E4D4
4 changed files with 102 additions and 223 deletions

View file

@ -211,18 +211,7 @@ enum Work<'a> {
constraint: &'a Constraint,
},
CheckForInfiniteTypes(LocalDefVarsVec<(Symbol, Loc<Variable>)>),
/// The ret_con part of a let constraint that does NOT introduces rigid and/or flex variables
LetConNoVariables {
scope: &'a Scope,
rank: Rank,
let_con: &'a LetConstraint,
/// The variables used to store imported types in the Subs.
/// The `Contents` are copied from the source module, but to
/// mimic `type_to_var`, we must add these variables to `Pools`
/// at the correct rank
pool_variables: &'a [Variable],
},
CheckSuffixFx(LocalDefVarsVec<(Symbol, Loc<Variable>)>),
/// The ret_con part of a let constraint that introduces rigid and/or flex variables
///
/// These introduced variables must be generalized, hence this variant
@ -288,56 +277,6 @@ fn solve(
continue;
}
Work::LetConNoVariables {
scope,
rank,
let_con,
pool_variables,
} => {
// NOTE be extremely careful with shadowing here
let offset = let_con.defs_and_ret_constraint.index();
let ret_constraint = &env.constraints.constraints[offset + 1];
// Add a variable for each def to new_vars_by_env.
let local_def_vars = LocalDefVarsVec::from_def_types(
env,
rank,
problems,
abilities_store,
obligation_cache,
&mut can_types,
aliases,
let_con.def_types,
);
env.pools.get_mut(rank).extend(pool_variables);
let mut new_scope = scope.clone();
for (symbol, loc_var) in local_def_vars.iter() {
check_ability_specialization(
env,
rank,
abilities_store,
obligation_cache,
awaiting_specializations,
problems,
*symbol,
*loc_var,
);
new_scope.insert_symbol_var_if_vacant(*symbol, loc_var.value);
}
stack.push(Work::Constraint {
scope: env.arena.alloc(new_scope),
rank,
constraint: ret_constraint,
});
// Check for infinite types first
stack.push(Work::CheckForInfiniteTypes(local_def_vars));
continue;
}
Work::LetConIntroducesVariables {
scope,
rank,
@ -456,14 +395,8 @@ fn solve(
new_scope.insert_symbol_var_if_vacant(*symbol, loc_var.value);
solve_suffix_fx(
env,
problems,
host_exposed_symbols,
FxSuffixKind::Let(*symbol),
loc_var.value,
&loc_var.region,
);
// At the time of introduction, promote explicitly-effectful symbols.
promote_effectful_symbol(env, FxSuffixKind::Let(*symbol), loc_var.value);
}
// Note that this vars_by_symbol is the one returned by the
@ -473,20 +406,42 @@ fn solve(
mark: final_mark,
};
// Now solve the body, using the new vars_by_symbol which includes
// the assignments' name-to-variable mappings.
stack.push(Work::Constraint {
scope: env.arena.alloc(new_scope),
rank,
constraint: ret_constraint,
});
// Check for infinite types first
stack.push(Work::CheckForInfiniteTypes(local_def_vars));
let next_work = [
// Check for infinite types first
Work::CheckForInfiniteTypes(local_def_vars.clone()),
// Now solve the body, using the new vars_by_symbol which includes
// the assignments' name-to-variable mappings.
Work::Constraint {
scope: env.arena.alloc(new_scope),
rank,
constraint: ret_constraint,
},
// Finally, check the suffix fx, after we have solved all types.
Work::CheckSuffixFx(local_def_vars),
];
for work in next_work.into_iter().rev() {
stack.push(work);
}
state = state_for_ret_con;
continue;
}
Work::CheckSuffixFx(local_def_vars) => {
for (symbol, loc_var) in local_def_vars.iter() {
solve_suffix_fx(
env,
problems,
host_exposed_symbols,
FxSuffixKind::Let(*symbol),
loc_var.value,
&loc_var.region,
);
}
continue;
}
};
state = match constraint {
@ -1004,100 +959,64 @@ fn solve(
let offset = let_con.defs_and_ret_constraint.index();
let defs_constraint = &env.constraints.constraints[offset];
let ret_constraint = &env.constraints.constraints[offset + 1];
let flex_vars = &env.constraints.variables[let_con.flex_vars.indices()];
let rigid_vars = &env.constraints[let_con.rigid_vars];
let pool_variables = &env.constraints.variables[pool_slice.indices()];
if matches!(&ret_constraint, True) && rigid_vars.is_empty() {
debug_assert!(pool_variables.is_empty());
env.introduce(rank, flex_vars);
// If the return expression is guaranteed to solve,
// solve the assignments themselves and move on.
stack.push(Work::Constraint {
scope,
rank,
constraint: defs_constraint,
});
state
} else if rigid_vars.is_empty() && let_con.flex_vars.is_empty() {
// items are popped from the stack in reverse order. That means that we'll
// first solve then defs_constraint, and then (eventually) the ret_constraint.
//
// Note that the LetConSimple gets the current env and rank,
// and not the env/rank from after solving the defs_constraint
stack.push(Work::LetConNoVariables {
scope,
rank,
let_con,
pool_variables,
});
stack.push(Work::Constraint {
scope,
rank,
constraint: defs_constraint,
});
state
// If the let-binding is generalizable, work at the next rank (which will be
// the rank at which introduced variables will become generalized, if they end up
// staying there); otherwise, stay at the current level.
let binding_rank = if let_con.generalizable.0 {
rank.next()
} else {
// If the let-binding is generalizable, work at the next rank (which will be
// the rank at which introduced variables will become generalized, if they end up
// staying there); otherwise, stay at the current level.
let binding_rank = if let_con.generalizable.0 {
rank.next()
} else {
rank
};
rank
};
// determine the next pool
if binding_rank.into_usize() < env.pools.len() {
// Nothing to do, we already accounted for the next rank, no need to
// adjust the pools
} else {
// we should be off by one at this point
debug_assert_eq!(binding_rank.into_usize(), 1 + env.pools.len());
env.pools.extend_to(binding_rank.into_usize());
}
let pool: &mut Vec<Variable> = env.pools.get_mut(binding_rank);
// Introduce the variables of this binding, and extend the pool at our binding
// rank.
for &var in rigid_vars.iter().map(|v| &v.value).chain(flex_vars.iter()) {
env.subs.set_rank(var, binding_rank);
}
pool.reserve(rigid_vars.len() + flex_vars.len());
pool.extend(rigid_vars.iter().map(|v| &v.value));
pool.extend(flex_vars.iter());
// Now, run our binding constraint, generalize, then solve the rest of the
// program.
//
// Items are popped from the stack in reverse order. That means that we'll
// first solve the defs_constraint, and then (eventually) the ret_constraint.
//
// NB: LetCon gets the current scope's env and rank, not the env/rank from after solving the defs_constraint.
// That's because the defs constraints will be solved in next_rank if it is eligible for generalization.
// The LetCon will then generalize variables that are at a higher rank than the rank of the current scope.
stack.push(Work::LetConIntroducesVariables {
scope,
rank,
let_con,
pool_variables,
});
stack.push(Work::Constraint {
scope,
rank: binding_rank,
constraint: defs_constraint,
});
state
// determine the next pool
if binding_rank.into_usize() < env.pools.len() {
// Nothing to do, we already accounted for the next rank, no need to
// adjust the pools
} else {
// we should be off by one at this point
debug_assert_eq!(binding_rank.into_usize(), 1 + env.pools.len());
env.pools.extend_to(binding_rank.into_usize());
}
let pool: &mut Vec<Variable> = env.pools.get_mut(binding_rank);
// Introduce the variables of this binding, and extend the pool at our binding
// rank.
for &var in rigid_vars.iter().map(|v| &v.value).chain(flex_vars.iter()) {
env.subs.set_rank(var, binding_rank);
}
pool.reserve(rigid_vars.len() + flex_vars.len());
pool.extend(rigid_vars.iter().map(|v| &v.value));
pool.extend(flex_vars.iter());
// Now, run our binding constraint, generalize, then solve the rest of the
// program.
//
// Items are popped from the stack in reverse order. That means that we'll
// first solve the defs_constraint, and then (eventually) the ret_constraint.
//
// NB: LetCon gets the current scope's env and rank, not the env/rank from after solving the defs_constraint.
// That's because the defs constraints will be solved in next_rank if it is eligible for generalization.
// The LetCon will then generalize variables that are at a higher rank than the rank of the current scope.
stack.push(Work::LetConIntroducesVariables {
scope,
rank,
let_con,
pool_variables,
});
stack.push(Work::Constraint {
scope,
rank: binding_rank,
constraint: defs_constraint,
});
state
}
IsOpenType(type_index) => {
let actual = either_type_index_to_var(
@ -1773,6 +1692,20 @@ fn solve_suffix_fx(
}
}
fn promote_effectful_symbol(env: &mut InferenceEnv<'_>, kind: FxSuffixKind, variable: Variable) {
if kind.suffix() != IdentSuffix::Bang {
return;
}
if !matches!(
env.subs.get_content_without_compacting(variable),
Content::FlexVar(_)
) {
return;
}
env.subs
.set_content(variable, Content::Structure(FlatType::EffectfulFunc));
}
fn chase_alias_content(subs: &Subs, mut var: Variable) -> (Variable, &Content) {
loop {
match subs.get_content_without_compacting(var) {
@ -2147,7 +2080,7 @@ fn check_ability_specialization(
}
}
#[derive(Debug)]
#[derive(Debug, Clone)]
enum LocalDefVarsVec<T> {
Stack(arrayvec::ArrayVec<T, 32>),
Heap(Vec<T>),