Consolidate flex and hybrid mutual recursive constraints

This commit is contained in:
Ayaz Hafiz 2022-06-17 12:13:53 -04:00
parent c188690be3
commit 89bf3b583f
No known key found for this signature in database
GPG key ID: 0E2A37416A25EF58
2 changed files with 60 additions and 37 deletions

View file

@ -1931,8 +1931,7 @@ pub fn rec_defs_help(
// hybrid: those with type annotations containing an inference variable, e.g. _ -> b
// flex: those without a type annotation
let mut rigid_info = Info::with_capacity(defs.len());
let mut hybrid_info = Info::with_capacity(defs.len());
let mut flex_info = Info::with_capacity(defs.len());
let mut hybrid_and_flex_info = Info::with_capacity(defs.len());
for def in defs {
let expr_var = def.expr_var;
@ -1956,10 +1955,11 @@ pub fn rec_defs_help(
let def_con = expr_con;
// TODO: shouldn't this be extend??
flex_info.vars = def_pattern_state.vars;
flex_info.constraints.push(def_con);
flex_info.def_types.extend(def_pattern_state.headers);
hybrid_and_flex_info.vars.extend(def_pattern_state.vars);
hybrid_and_flex_info.constraints.push(def_con);
hybrid_and_flex_info
.def_types
.extend(def_pattern_state.headers);
}
Some(annotation) => {
@ -1980,7 +1980,7 @@ pub fn rec_defs_help(
let is_hybrid = !new_infer_variables.is_empty();
hybrid_info.vars.extend(new_infer_variables);
hybrid_and_flex_info.vars.extend(new_infer_variables);
let annotation_expected = FromAnnotation(
def.loc_pattern.clone(),
@ -2106,9 +2106,11 @@ pub fn rec_defs_help(
let def_con = constraints.exists(vars, and_constraint);
if is_hybrid {
hybrid_info.vars.extend(&new_rigid_variables);
hybrid_info.constraints.push(def_con);
hybrid_info.def_types.extend(def_pattern_state.headers);
hybrid_and_flex_info.vars.extend(&new_rigid_variables);
hybrid_and_flex_info.constraints.push(def_con);
hybrid_and_flex_info
.def_types
.extend(def_pattern_state.headers);
} else {
rigid_info.vars.extend(&new_rigid_variables);
@ -2143,9 +2145,11 @@ pub fn rec_defs_help(
let def_con = constraints.and_constraint(cons);
if is_hybrid {
hybrid_info.vars.extend(&new_rigid_variables);
hybrid_info.constraints.push(def_con);
hybrid_info.def_types.extend(def_pattern_state.headers);
hybrid_and_flex_info.vars.extend(&new_rigid_variables);
hybrid_and_flex_info.constraints.push(def_con);
hybrid_and_flex_info
.def_types
.extend(def_pattern_state.headers);
} else {
rigid_info.vars.extend(&new_rigid_variables);
@ -2177,31 +2181,25 @@ pub fn rec_defs_help(
// forcing `b -> c ~ List b -> c` and correctly picking up a recursion error.
// Had we generalized `b -> c`, the call `f [x]` would have been generalized, and this
// error would not be found.
// This works just as well in the mutually recursive context.
//
// 3. We know the real type of hybrid defs, and now need to ensure they agree with what the
// elaborated parts of their type annotations demand.
// - This works just as well for mutually recursive defs.
// - For hybrid defs, we also ensure solved types agree with what the
// elaborated parts of their type annotations demand.
//
// 4. Now properly let-generalize the flex + hybrid defs, since we now know their types and
// 3. Now properly let-generalize the flex + hybrid defs, since we now know their types and
// that they don't have circular type errors.
//
// 5. Solve the bodies of the typed body defs, and check that they agree the types of the type
// 4. Solve the bodies of the typed body defs, and check that they agree the types of the type
// annotation.
//
// 6. Solve the rest of the program that happens after this recursive def block.
// 5. Solve the rest of the program that happens after this recursive def block.
// 2. Solve untyped defs without generalization of their symbols.
let untyped_body_constraints = {
let flex_constrs = constraints.and_constraint(flex_info.constraints);
let hybrid_constrs = constraints.and_constraint(hybrid_info.constraints);
constraints.and_constraint([flex_constrs, hybrid_constrs])
};
let untyped_body_constraints = constraints.and_constraint(hybrid_and_flex_info.constraints);
let untyped_def_symbols_constr = constraints.let_constraint(
[],
[],
(flex_info.def_types.clone().into_iter())
.chain(hybrid_info.def_types.clone().into_iter())
.collect::<Vec<_>>(),
hybrid_and_flex_info.def_types.clone(),
Constraint::True,
untyped_body_constraints,
);
@ -2222,15 +2220,13 @@ pub fn rec_defs_help(
let typed_body_and_final_constr =
constraints.and_constraint([typed_body_constraints, cycle_constraint, body_con]);
// 4. Properly generalize untyped defs after solving them.
// 3. Properly generalize untyped defs after solving them.
let inner = constraints.let_constraint(
[],
flex_info.vars.into_iter().chain(hybrid_info.vars),
(flex_info.def_types.into_iter())
.chain(hybrid_info.def_types)
.collect::<Vec<_>>(),
hybrid_and_flex_info.vars,
hybrid_and_flex_info.def_types,
untyped_def_symbols_constr,
// 5 + 6. Solve the typed body defs, and the rest of the program.
// 4 + 5. Solve the typed body defs, and the rest of the program.
typed_body_and_final_constr,
);