Skip to content

Commit

Permalink
introduce variances into subtyping
Browse files Browse the repository at this point in the history 
The rules are probably stricter than needed.
  • Loading branch information
@nikomatsakis
nikomatsakis committed Feb 20, 2024
1 parent 2311faa commit 18306dd
Show file tree
Hide file tree
Showing 7 changed files with 199 additions and 20 deletions.
13 changes: 12 additions & 1 deletion src/grammar.rs
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
pub use crate::dada_lang::grammar::*;
use crate::dada_lang::FormalityLang;
use formality_core::{term, Fallible, Set, Upcast, UpcastFrom};
use formality_core::{term, Downcast, Fallible, Set, Upcast, UpcastFrom};
use std::sync::Arc;

mod cast_impls;
Expand Down Expand Up @@ -210,6 +210,17 @@ pub enum Parameter {
Perm(Perm),
}

impl Parameter {
pub fn is_var(&self, v: impl Upcast<Variable>) -> bool {
let Some(u) = self.downcast::<Variable>() else {
return false;
};

let v: Variable = v.upcast();
v == u
}
}

impl formality_core::language::HasKind<FormalityLang> for Parameter {
fn kind(&self) -> formality_core::language::CoreKind<FormalityLang> {
match self {
Expand Down
33 changes: 32 additions & 1 deletion src/type_system/classes.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,8 @@ use fn_error_context::context;
use formality_core::Fallible;

use crate::grammar::{
Atomic, ClassDecl, ClassDeclBoundData, FieldDecl, NamedTy, Program, Var, VarianceKind,
Atomic, ClassDecl, ClassDeclBoundData, FieldDecl, NamedTy, Predicate, Program, Var,
VarianceKind,
};

use super::{
Expand Down Expand Up @@ -71,3 +72,33 @@ fn check_field(class_ty: &NamedTy, env: &Env, decl: &FieldDecl) -> Fallible<()>

Ok(())
}

impl ClassDecl {
/// Compute, for each generic parameter of this class,
/// the relevant variance declarations.
pub fn variances(&self) -> Vec<Vec<VarianceKind>> {
let (
bound_vars,
ClassDeclBoundData {
predicates,
fields: _,
methods: _,
},
) = self.binder.open();

bound_vars
.iter()
.map(|v| {
// Find the variance predicates
// applied to the generic parameter `v`
predicates
.iter()
.filter_map(|p| match p {
Predicate::Variance(kind, parameter) if parameter.is_var(&v) => Some(*kind),
_ => None,
})
.collect()
})
.collect()
}
}
10 changes: 9 additions & 1 deletion src/type_system/env.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ use crate::{
grammar::{Binder, ExistentialVar, UniversalVar, VarIndex, Variable},
Term,
},
grammar::{Kind, LocalVariableDecl, Predicate, Program, Ty, TypeName, Var},
grammar::{Kind, LocalVariableDecl, Predicate, Program, Ty, TypeName, Var, VarianceKind},
};

use super::in_flight::{InFlight, Transform};
Expand Down Expand Up @@ -41,6 +41,14 @@ impl Env {
}
}

pub fn variances(&self, type_name: &TypeName) -> Fallible<Vec<Vec<VarianceKind>>> {
match type_name {
TypeName::Tuple(n) => Ok(vec![vec![]; *n]),
TypeName::Int => Ok(vec![]),
TypeName::Id(name) => Ok(self.program.class_named(name)?.variances()),
}
}

pub fn add_assumptions(&mut self, assumptions: impl Upcast<Vec<Predicate>>) {
let assumptions: Vec<Predicate> = assumptions.upcast();
self.assumptions.extend(assumptions);
Expand Down
25 changes: 16 additions & 9 deletions src/type_system/subtypes.rs
View file
Original file line number Diff line number Diff line change
@@ -1,14 +1,14 @@
use formality_core::{judgment_fn, Cons, Set};

use crate::{
grammar::{NamedTy, Parameter, Perm, Place, Ty},
grammar::{NamedTy, Parameter, Perm, Place, Ty, VarianceKind},
type_system::{
env::Env,
is_::{lien_chain_is_leased, lien_chain_is_shared},
lien_chains::{lien_chains, ty_chains, Lien, LienChain, My, Our, TyChain},
lien_set::lien_set_from_chain,
liveness::LivePlaces,
quantifiers::fold_zipped,
quantifiers::{fold, fold_zipped},
},
};

Expand Down Expand Up @@ -107,8 +107,11 @@ judgment_fn! {
(if name_a == name_b) // FIXME: subtyping between classes
(if env.is_class_ty(&name_a))!
(sub_lien_chains(env, &live_after, &chain_a, &chain_b) => env)
(fold_zipped(env, &parameters_a, &parameters_b, &|env, parameter_a, parameter_b| {
sub_generic_parameter(env, &live_after, &chain_a, parameter_a, &chain_b, parameter_b)
(let variances = env.variances(&name_a)?)
(if parameters_a.len() == variances.len())
(if parameters_b.len() == variances.len())
(fold(env, 0..variances.len(), &|env, &i| {
sub_generic_parameter(env, &live_after, &variances[i], &chain_a, &parameters_a[i], &chain_b, &parameters_b[i])
}) => env)
(compatible_layout(env, &chain_a, &chain_b) => env)
-------------------------------- ("class ty")
Expand Down Expand Up @@ -173,38 +176,42 @@ judgment_fn! {
fn sub_generic_parameter(
env: Env,
live_after: LivePlaces,
variances: Vec<VarianceKind>,
cx_a: LienChain,
a: Parameter,
cx_b: LienChain,
b: Parameter,
) => Env {
debug(cx_a, a, cx_b, b, live_after, env)
debug(variances, cx_a, a, cx_b, b, live_after, env)

// FIXME: this may be stricter than needed: we may everything invariant
// even if it's just relative and not atomic, is that correct?

(
(sub_in_cx(env, &live_after, My(), &a, My(), &b) => env)
(sub_in_cx(env, &live_after, My(), &b, My(), &a) => env)
------------------------------- ("invariant")
(sub_generic_parameter(env, live_after, _cx_a, a, _cx_b, b) => env)
(sub_generic_parameter(env, live_after, _variances, _cx_a, a, _cx_b, b) => env)
)

(
(lien_chain_is_shared(&env, &cx_a) => ())
(sub_in_cx(&env, &live_after, &cx_a, &a, &cx_b, &b) => env)
------------------------------- ("shared_a")
(sub_generic_parameter(env, live_after, cx_a, a, cx_b, b) => env)
(sub_generic_parameter(env, live_after, (), cx_a, a, cx_b, b) => env)
)

(
(lien_chain_is_shared(&env, &cx_b) => ())
(sub_in_cx(&env, &live_after, &cx_a, &a, &cx_b, &b) => env)
------------------------------- ("shared_b")
(sub_generic_parameter(env, live_after, cx_a, a, cx_b, b) => env)
(sub_generic_parameter(env, live_after, (), cx_a, a, cx_b, b) => env)
)

(
(sub_in_cx(env, live_after, My(), a, My(), b) => env)
------------------------------- ("my")
(sub_generic_parameter(env, live_after, My(), a, My(), b) => env)
(sub_generic_parameter(env, live_after, (), My(), a, My(), b) => env)
)
}
}
Expand Down
1 change: 1 addition & 0 deletions src/type_system/tests.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ mod permission_check;
mod subtyping;
mod type_check;
mod value_types;
mod variance_subtyping;

/// Check what happens when we encounter a bad class name in a function parameter.
#[test]
Expand Down
16 changes: 8 additions & 8 deletions src/type_system/tests/subtyping.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -743,15 +743,15 @@ fn leased_vec_my_Data_to_leased_vec_leased_Data() {
judgment `sub_ty_chain_sets { ty_liens_a: {NamedTy(leased{source}, Vec[my Data])}, ty_liens_b: {NamedTy(leased{source}, Vec[leased {source} Data])}, live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: leased {source} Vec[my Data], source: my Vec[my Data]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "cons" failed at step #1 (src/file.rs:LL:CC) because
judgment `sub_ty_chains { ty_chain_a: NamedTy(leased{source}, Vec[my Data]), ty_chain_b: NamedTy(leased{source}, Vec[leased {source} Data]), live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: leased {source} Vec[my Data], source: my Vec[my Data]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "class ty" failed at step #5 (src/file.rs:LL:CC) because
judgment `sub_generic_parameter { cx_a: leased{source}, a: my Data, cx_b: leased{source}, b: leased {source} Data, live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: leased {source} Vec[my Data], source: my Vec[my Data]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "class ty" failed at step #8 (src/file.rs:LL:CC) because
judgment `sub_generic_parameter { variances: [], cx_a: leased{source}, a: my Data, cx_b: leased{source}, b: leased {source} Data, live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: leased {source} Vec[my Data], source: my Vec[my Data]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "invariant" failed at step #0 (src/file.rs:LL:CC) because
judgment `sub_in_cx { cx_a: my, a: my Data, cx_b: my, b: leased {source} Data, live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: leased {source} Vec[my Data], source: my Vec[my Data]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "sub" failed at step #2 (src/file.rs:LL:CC) because
judgment `sub_ty_chain_sets { ty_liens_a: {NamedTy(my, Data)}, ty_liens_b: {NamedTy(leased{source}, Data)}, live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: leased {source} Vec[my Data], source: my Vec[my Data]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "cons" failed at step #1 (src/file.rs:LL:CC) because
judgment `sub_ty_chains { ty_chain_a: NamedTy(my, Data), ty_chain_b: NamedTy(leased{source}, Data), live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: leased {source} Vec[my Data], source: my Vec[my Data]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "class ty" failed at step #6 (src/file.rs:LL:CC) because
the rule "class ty" failed at step #9 (src/file.rs:LL:CC) because
judgment `compatible_layout { chain_a: my, chain_b: leased{source}, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: leased {source} Vec[my Data], source: my Vec[my Data]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "my-shared" failed at step #0 (src/file.rs:LL:CC) because
judgment had no applicable rules: `lien_chain_is_shared { chain: leased{source}, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: leased {source} Vec[my Data], source: my Vec[my Data]}, assumptions: {}, fresh: 0 } }`
Expand Down Expand Up @@ -795,8 +795,8 @@ fn leased_vec_leased_Data_to_leased_vec_my_Data() {
judgment `sub_ty_chain_sets { ty_liens_a: {NamedTy(leased{source}, Vec[leased {source} Data])}, ty_liens_b: {NamedTy(leased{source}, Vec[my Data])}, live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: leased {source} Vec[leased {source} Data], source: my Vec[my Data]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "cons" failed at step #1 (src/file.rs:LL:CC) because
judgment `sub_ty_chains { ty_chain_a: NamedTy(leased{source}, Vec[leased {source} Data]), ty_chain_b: NamedTy(leased{source}, Vec[my Data]), live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: leased {source} Vec[leased {source} Data], source: my Vec[my Data]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "class ty" failed at step #5 (src/file.rs:LL:CC) because
judgment `sub_generic_parameter { cx_a: leased{source}, a: leased {source} Data, cx_b: leased{source}, b: my Data, live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: leased {source} Vec[leased {source} Data], source: my Vec[my Data]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "class ty" failed at step #8 (src/file.rs:LL:CC) because
judgment `sub_generic_parameter { variances: [], cx_a: leased{source}, a: leased {source} Data, cx_b: leased{source}, b: my Data, live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: leased {source} Vec[leased {source} Data], source: my Vec[my Data]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "invariant" failed at step #0 (src/file.rs:LL:CC) because
judgment `sub_in_cx { cx_a: my, a: leased {source} Data, cx_b: my, b: my Data, live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: leased {source} Vec[leased {source} Data], source: my Vec[my Data]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "sub" failed at step #2 (src/file.rs:LL:CC) because
Expand Down Expand Up @@ -866,15 +866,15 @@ fn forall_P_vec_my_Data_to_P_vec_P_Data() {
judgment `sub_ty_chain_sets { ty_liens_a: {NamedTy(!perm_0, Vec[Data])}, ty_liens_b: {NamedTy(!perm_0, Vec[!perm_0 Data])}, live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: !perm_0 Vec[Data], source: my Vec[my Data]}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
the rule "cons" failed at step #1 (src/file.rs:LL:CC) because
judgment `sub_ty_chains { ty_chain_a: NamedTy(!perm_0, Vec[Data]), ty_chain_b: NamedTy(!perm_0, Vec[!perm_0 Data]), live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: !perm_0 Vec[Data], source: my Vec[my Data]}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
the rule "class ty" failed at step #5 (src/file.rs:LL:CC) because
judgment `sub_generic_parameter { cx_a: !perm_0, a: Data, cx_b: !perm_0, b: !perm_0 Data, live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: !perm_0 Vec[Data], source: my Vec[my Data]}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
the rule "class ty" failed at step #8 (src/file.rs:LL:CC) because
judgment `sub_generic_parameter { variances: [], cx_a: !perm_0, a: Data, cx_b: !perm_0, b: !perm_0 Data, live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: !perm_0 Vec[Data], source: my Vec[my Data]}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
the rule "invariant" failed at step #0 (src/file.rs:LL:CC) because
judgment `sub_in_cx { cx_a: my, a: Data, cx_b: my, b: !perm_0 Data, live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: !perm_0 Vec[Data], source: my Vec[my Data]}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
the rule "sub" failed at step #2 (src/file.rs:LL:CC) because
judgment `sub_ty_chain_sets { ty_liens_a: {NamedTy(my, Data)}, ty_liens_b: {NamedTy(!perm_0, Data)}, live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: !perm_0 Vec[Data], source: my Vec[my Data]}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
the rule "cons" failed at step #1 (src/file.rs:LL:CC) because
judgment `sub_ty_chains { ty_chain_a: NamedTy(my, Data), ty_chain_b: NamedTy(!perm_0, Data), live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: !perm_0 Vec[Data], source: my Vec[my Data]}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
the rule "class ty" failed at step #6 (src/file.rs:LL:CC) because
the rule "class ty" failed at step #9 (src/file.rs:LL:CC) because
judgment `compatible_layout { chain_a: my, chain_b: !perm_0, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: !perm_0 Vec[Data], source: my Vec[my Data]}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
the rule "my-shared" failed at step #0 (src/file.rs:LL:CC) because
judgment `lien_chain_is_shared { chain: !perm_0, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: !perm_0 Vec[Data], source: my Vec[my Data]}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
Expand Down
Loading

0 comments on commit 18306dd

Please sign in to comment.