language-servers/roc
1
0
Fork 0
mirror of https://github.com/roc-lang/roc.git synced 2025-10-03 16:44:33 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions 6

Correct soundness bug with the presence of inference variables

Browse source
This commit is contained in:
Ayaz Hafiz 2022-06-17 11:17:33 -04:00
parent c9ca3effbc
commit f27a841bec
No known key found for this signature in database
GPG key ID: 0E2A37416A25EF58
3 changed files with 216 additions and 44 deletions
Download patch file Download diff file Expand all files Collapse all files

118
compiler/constrain/src/expr.rs
View file

@ -1916,15 +1916,7 @@ fn constrain_recursive_defs(
body_con: Constraint,
cycle_mark: IllegalCycleMark,
) -> Constraint {
rec_defs_help(
constraints,
env,
defs,
body_con,
Info::with_capacity(defs.len()),
Info::with_capacity(defs.len()),
cycle_mark,
)
rec_defs_help(constraints, env, defs, body_con, cycle_mark)
}
pub fn rec_defs_help(
@ -1932,10 +1924,16 @@ pub fn rec_defs_help(
env: &mut Env,
defs: &[Def],
body_con: Constraint,
mut rigid_info: Info,
mut flex_info: Info,
cycle_mark: IllegalCycleMark,
) -> Constraint {
// We partition recursive defs into three buckets:
// rigid: those with fully-elaborated type annotations (no inference vars), e.g. a -> b
// 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());
for def in defs {
let expr_var = def.expr_var;
let expr_type = Type::Variable(expr_var);
@ -1958,6 +1956,7 @@ 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);
@ -1979,7 +1978,9 @@ pub fn rec_defs_help(
&mut def_pattern_state.headers,
);
flex_info.vars.extend(new_infer_variables);
let is_hybrid = !new_infer_variables.is_empty();
hybrid_info.vars.extend(new_infer_variables);
let annotation_expected = FromAnnotation(
def.loc_pattern.clone(),
@ -2104,16 +2105,22 @@ pub fn rec_defs_help(
let and_constraint = constraints.and_constraint(cons);
let def_con = constraints.exists(vars, and_constraint);
rigid_info.vars.extend(&new_rigid_variables);
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);
} else {
rigid_info.vars.extend(&new_rigid_variables);
rigid_info.constraints.push(constraints.let_constraint(
new_rigid_variables,
def_pattern_state.vars,
[], // no headers introduced (at this level)
def_con,
Constraint::True,
));
rigid_info.def_types.extend(def_pattern_state.headers);
rigid_info.constraints.push(constraints.let_constraint(
new_rigid_variables,
def_pattern_state.vars,
[], // no headers introduced (at this level)
def_con,
Constraint::True,
));
rigid_info.def_types.extend(def_pattern_state.headers);
}
}
_ => {
let expected = annotation_expected;
@ -2135,16 +2142,22 @@ pub fn rec_defs_help(
];
let def_con = constraints.and_constraint(cons);
rigid_info.vars.extend(&new_rigid_variables);
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);
} else {
rigid_info.vars.extend(&new_rigid_variables);
rigid_info.constraints.push(constraints.let_constraint(
new_rigid_variables,
def_pattern_state.vars,
[], // no headers introduced (at this level)
def_con,
Constraint::True,
));
rigid_info.def_types.extend(def_pattern_state.headers);
rigid_info.constraints.push(constraints.let_constraint(
new_rigid_variables,
def_pattern_state.vars,
[], // no headers introduced (at this level)
def_con,
Constraint::True,
));
rigid_info.def_types.extend(def_pattern_state.headers);
}
}
}
}
@ -2152,28 +2165,43 @@ pub fn rec_defs_help(
}
// Strategy for recursive defs:
// 1. Let-generalize the type annotations we know; these are the source of truth we'll solve
// everything else with. If there are circular type errors here, they will be caught during
// the let-generalization.
// 2. Introduce all symbols of the untyped defs, but don't generalize them yet. Now, solve
// the untyped defs' bodies. This way, when checking something like
//
// 1. Let-generalize all rigid annotations. These are the source of truth we'll solve
// everything else with. If there are circular type errors here, they will be caught
// during the let-generalization.
//
// 2. Introduce all symbols of the flex + hybrid defs, but don't generalize them yet.
// Now, solve those defs' bodies. This way, when checking something like
// f = \x -> f [x]
// we introduce `f: b -> c`, then constrain the call `f [x]`,
// 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.
// 3. Now properly let-generalize the untyped body defs, since we now know their types and
// 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.
//
// 4. Now properly let-generalize the flex + hybrid defs, since we now know their types and
// that they don't have circular type errors.
// 4. Solve the bodies of the typed body defs, and check that they agree the types of the type
//
// 5. Solve the bodies of the typed body defs, and check that they agree the types of the type
// annotation.
// 5. Solve the rest of the program that happens after this recursive def block.
//
// 6. 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 = constraints.and_constraint(flex_info.constraints);
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_def_symbols_constr = constraints.let_constraint(
[],
[],
flex_info.def_types.clone(),
(flex_info.def_types.clone().into_iter())
.chain(hybrid_info.def_types.clone().into_iter())
.collect::<Vec<_>>(),
Constraint::True,
untyped_body_constraints,
);
@ -2194,13 +2222,15 @@ pub fn rec_defs_help(
let typed_body_and_final_constr =
constraints.and_constraint([typed_body_constraints, cycle_constraint, body_con]);
// 3. Properly generalize untyped defs after solving them.
// 4. Properly generalize untyped defs after solving them.
let inner = constraints.let_constraint(
[],
flex_info.vars,
flex_info.def_types,
flex_info.vars.into_iter().chain(hybrid_info.vars),
(flex_info.def_types.into_iter())
.chain(hybrid_info.def_types)
.collect::<Vec<_>>(),
untyped_def_symbols_constr,
// 4 + 5. Solve the typed body defs, and the rest of the program.
// 5 + 6. Solve the typed body defs, and the rest of the program.
typed_body_and_final_constr,
);