diff options
Diffstat (limited to 'vendor/chalk-solve-0.87.0/src/infer/test.rs')
| -rw-r--r-- | vendor/chalk-solve-0.87.0/src/infer/test.rs | 422 |
1 files changed, 422 insertions, 0 deletions
diff --git a/vendor/chalk-solve-0.87.0/src/infer/test.rs b/vendor/chalk-solve-0.87.0/src/infer/test.rs new file mode 100644 index 000000000..2ac35f027 --- /dev/null +++ b/vendor/chalk-solve-0.87.0/src/infer/test.rs @@ -0,0 +1,422 @@ +#![cfg(test)] + +use super::unify::RelationResult; +use super::*; +use chalk_integration::interner::ChalkIr; +use chalk_integration::{arg, lifetime, ty}; + +// We just use a vec of 20 `Invariant`, since this is zipped and no substs are +// longer than this +#[derive(Debug)] +struct TestDatabase; +impl UnificationDatabase<ChalkIr> for TestDatabase { + fn fn_def_variance(&self, _fn_def_id: FnDefId<ChalkIr>) -> Variances<ChalkIr> { + Variances::from_iter(ChalkIr, [Variance::Invariant; 20].iter().copied()) + } + + fn adt_variance(&self, _adt_id: AdtId<ChalkIr>) -> Variances<ChalkIr> { + Variances::from_iter(ChalkIr, [Variance::Invariant; 20].iter().copied()) + } +} + +#[test] +fn universe_error() { + // exists(A -> forall(X -> A = X)) ---> error + let interner = ChalkIr; + let mut table: InferenceTable<ChalkIr> = InferenceTable::new(); + let environment0 = Environment::new(interner); + let a = table.new_variable(U0).to_ty(interner); + table + .relate( + interner, + &TestDatabase, + &environment0, + Variance::Invariant, + &a, + &ty!(placeholder 1), + ) + .unwrap_err(); +} + +#[test] +fn cycle_error() { + // exists(A -> A = foo A) ---> error + let interner = ChalkIr; + let mut table: InferenceTable<ChalkIr> = InferenceTable::new(); + let environment0 = Environment::new(interner); + let a = table.new_variable(U0).to_ty(interner); + table + .relate( + interner, + &TestDatabase, + &environment0, + Variance::Invariant, + &a, + &ty!(apply (item 0) (expr a)), + ) + .unwrap_err(); + + // exists(A -> A = for<'a> A) + table + .relate( + interner, + &TestDatabase, + &environment0, + Variance::Invariant, + &a, + &ty!(function 1 (infer 0)), + ) + .unwrap_err(); +} + +#[test] +fn cycle_indirect() { + // exists(A -> A = foo B, A = B) ---> error + let interner = ChalkIr; + let mut table: InferenceTable<ChalkIr> = InferenceTable::new(); + let environment0 = Environment::new(interner); + let a = table.new_variable(U0).to_ty(interner); + let b = table.new_variable(U0).to_ty(interner); + table + .relate( + interner, + &TestDatabase, + &environment0, + Variance::Invariant, + &a, + &ty!(apply (item 0) (expr b)), + ) + .unwrap(); + table + .relate( + interner, + &TestDatabase, + &environment0, + Variance::Invariant, + &a, + &b, + ) + .unwrap_err(); +} + +#[test] +fn universe_error_indirect_1() { + // exists(A -> forall(X -> exists(B -> B = X, A = B))) ---> error + let interner = ChalkIr; + let mut table: InferenceTable<ChalkIr> = InferenceTable::new(); + let environment0 = Environment::new(interner); + let a = table.new_variable(U0).to_ty(interner); + let b = table.new_variable(U1).to_ty(interner); + table + .relate( + interner, + &TestDatabase, + &environment0, + Variance::Invariant, + &b, + &ty!(placeholder 1), + ) + .unwrap(); + table + .relate( + interner, + &TestDatabase, + &environment0, + Variance::Invariant, + &a, + &b, + ) + .unwrap_err(); +} + +#[test] +fn universe_error_indirect_2() { + // exists(A -> forall(X -> exists(B -> B = A, B = X))) ---> error + let interner = ChalkIr; + let mut table: InferenceTable<ChalkIr> = InferenceTable::new(); + let environment0 = Environment::new(interner); + let a = table.new_variable(U0).to_ty(interner); + let b = table.new_variable(U1).to_ty(interner); + table + .relate( + interner, + &TestDatabase, + &environment0, + Variance::Invariant, + &a, + &b, + ) + .unwrap(); + table + .relate( + interner, + &TestDatabase, + &environment0, + Variance::Invariant, + &b, + &ty!(placeholder 1), + ) + .unwrap_err(); +} + +#[test] +fn universe_promote() { + // exists(A -> forall(X -> exists(B -> A = foo(B), A = foo(i32)))) ---> OK + let interner = ChalkIr; + let mut table: InferenceTable<ChalkIr> = InferenceTable::new(); + let environment0 = Environment::new(interner); + let a = table.new_variable(U0).to_ty(interner); + let b = table.new_variable(U1).to_ty(interner); + table + .relate( + interner, + &TestDatabase, + &environment0, + Variance::Invariant, + &a, + &ty!(apply (item 0) (expr b)), + ) + .unwrap(); + table + .relate( + interner, + &TestDatabase, + &environment0, + Variance::Invariant, + &a, + &ty!(apply (item 0) (apply (item 1))), + ) + .unwrap(); +} + +#[test] +fn universe_promote_bad() { + // exists(A -> forall(X -> exists(B -> A = foo(B), B = X))) ---> error + let interner = ChalkIr; + let mut table: InferenceTable<ChalkIr> = InferenceTable::new(); + let environment0 = Environment::new(interner); + let a = table.new_variable(U0).to_ty(interner); + let b = table.new_variable(U1).to_ty(interner); + table + .relate( + interner, + &TestDatabase, + &environment0, + Variance::Invariant, + &a, + &ty!(apply (item 0) (expr b)), + ) + .unwrap(); + table + .relate( + interner, + &TestDatabase, + &environment0, + Variance::Invariant, + &b, + &ty!(placeholder 1), + ) + .unwrap_err(); +} + +#[test] +fn projection_eq() { + // exists(A -> A = Item0<<A as Item1>::foo>) + // ^^^^^^^^^^^^ Can A repeat here? For now, + // we say no, but it's an interesting question. + let interner = ChalkIr; + let mut table: InferenceTable<ChalkIr> = InferenceTable::new(); + let environment0 = Environment::new(interner); + let a = table.new_variable(U0).to_ty(interner); + + // expect an error ("cycle during unification") + table + .relate( + interner, + &TestDatabase, + &environment0, + Variance::Invariant, + &a, + &ty!(apply (item 0) (projection (item 1) (expr a))), + ) + .unwrap_err(); +} + +const U0: UniverseIndex = UniverseIndex { counter: 0 }; +const U1: UniverseIndex = UniverseIndex { counter: 1 }; +const U2: UniverseIndex = UniverseIndex { counter: 2 }; + +fn make_table() -> InferenceTable<ChalkIr> { + let mut table: InferenceTable<ChalkIr> = InferenceTable::new(); + let _ = table.new_universe(); // U1 + let _ = table.new_universe(); // U2 + table +} + +#[test] +fn quantify_simple() { + let interner = ChalkIr; + let mut table = make_table(); + let _ = table.new_variable(U0); + let _ = table.new_variable(U1); + let _ = table.new_variable(U2); + + assert_eq!( + table + .canonicalize(interner, ty!(apply (item 0) (infer 2) (infer 1) (infer 0))) + .quantified, + Canonical { + value: ty!(apply (item 0) (bound 0) (bound 1) (bound 2)), + binders: CanonicalVarKinds::from_iter( + interner, + vec![ + CanonicalVarKind::new(VariableKind::Ty(TyVariableKind::General), U2), + CanonicalVarKind::new(VariableKind::Ty(TyVariableKind::General), U1), + CanonicalVarKind::new(VariableKind::Ty(TyVariableKind::General), U0), + ] + ), + } + ); +} + +#[test] +fn quantify_bound() { + let interner = ChalkIr; + let mut table = make_table(); + let environment0 = Environment::new(interner); + + let v0 = table.new_variable(U0).to_ty(interner); + let v1 = table.new_variable(U1).to_ty(interner); + let v2a = table.new_variable(U2).to_ty(interner); + let v2b = table.new_variable(U2).to_ty(interner); + + table + .relate( + interner, + &TestDatabase, + &environment0, + Variance::Invariant, + &v2b, + &ty!(apply (item 1) (expr v1) (expr v0)), + ) + .unwrap(); + + assert_eq!( + table + .canonicalize( + interner, + ty!(apply (item 0) (expr v2b) (expr v2a) (expr v1) (expr v0)) + ) + .quantified, + Canonical { + value: ty!(apply (item 0) (apply (item 1) (bound 0) (bound 1)) (bound 2) (bound 0) (bound 1)), + binders: CanonicalVarKinds::from_iter( + interner, + vec![ + CanonicalVarKind::new(VariableKind::Ty(TyVariableKind::General), U1), + CanonicalVarKind::new(VariableKind::Ty(TyVariableKind::General), U0), + CanonicalVarKind::new(VariableKind::Ty(TyVariableKind::General), U2), + ] + ), + } + ); +} + +#[test] +fn quantify_ty_under_binder() { + let interner = ChalkIr; + let mut table = make_table(); + let v0 = table.new_variable(U0); + let v1 = table.new_variable(U0); + let _r2 = table.new_variable(U0); + + // Unify v0 and v1. + let environment0 = Environment::new(interner); + table + .relate( + interner, + &TestDatabase, + &environment0, + Variance::Invariant, + &v0.to_ty(interner), + &v1.to_ty(interner), + ) + .unwrap(); + + // Here: the `function` introduces 3 binders, so in the result, + // `(bound 3)` references the first canonicalized inference + // variable. -- note that `infer 0` and `infer 1` have been + // unified above, as well. + assert_eq!( + table + .canonicalize( + interner, + ty!(function 3 (apply (item 0) (bound 1) (infer 0) (infer 1) (lifetime (infer 2)))) + ) + .quantified, + Canonical { + value: ty!(function 3 (apply (item 0) (bound 1) (bound 1 0) (bound 1 0) (lifetime (bound 1 1)))), + binders: CanonicalVarKinds::from_iter( + interner, + vec![ + CanonicalVarKind::new(VariableKind::Ty(TyVariableKind::General), U0), + CanonicalVarKind::new(VariableKind::Lifetime, U0) + ] + ), + } + ); +} + +#[test] +fn lifetime_constraint_indirect() { + let interner = ChalkIr; + let mut table: InferenceTable<ChalkIr> = InferenceTable::new(); + let _ = table.new_universe(); // U1 + + let _t_0 = table.new_variable(U0); + let _l_1 = table.new_variable(U1); + + let environment0 = Environment::new(interner); + + // Here, we unify '?1 (the lifetime variable in universe 1) with + // '!1. + let t_a = ty!(apply (item 0) (lifetime (placeholder 1))); + let t_b = ty!(apply (item 0) (lifetime (infer 1))); + let RelationResult { goals } = table + .relate( + interner, + &TestDatabase, + &environment0, + Variance::Invariant, + &t_a, + &t_b, + ) + .unwrap(); + assert!(goals.is_empty()); + + // Here, we try to unify `?0` (the type variable in universe 0) + // with something that involves `'?1`. Since `'?1` has been + // unified with `'!1`, and `'!1` is not visible from universe 0, + // we will replace `'!1` with a new variable `'?2` and introduce a + // (likely unsatisfiable) constraint relating them. + let t_c = ty!(infer 0); + let RelationResult { goals } = table + .relate( + interner, + &TestDatabase, + &environment0, + Variance::Invariant, + &t_c, + &t_b, + ) + .unwrap(); + assert_eq!(goals.len(), 2); + assert_eq!( + format!("{:?}", goals[0]), + "InEnvironment { environment: Env([]), goal: \'?2: \'!1_0 }", + ); + assert_eq!( + format!("{:?}", goals[1]), + "InEnvironment { environment: Env([]), goal: \'!1_0: \'?2 }", + ); +} |