[rustc.git] / vendor / chalk-solve-0.14.0 / src / infer / test.rs

#![cfg(test)]

use super::unify::UnificationResult;
use super::*;
use chalk_integration::interner::ChalkIr;

#[test]
fn infer() {
    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
        .unify(interner, &environment0, &a, &ty!(apply (item 0) (expr b)))
        .unwrap();
    assert_eq!(
        table.normalize_deep(interner, &a),
        ty!(apply (item 0) (expr b))
    );
    table
        .unify(interner, &environment0, &b, &ty!(apply (item 1)))
        .unwrap();
    assert_eq!(
        table.normalize_deep(interner, &a),
        ty!(apply (item 0) (apply (item 1)))
    );
}

#[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
        .unify(interner, &environment0, &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
        .unify(interner, &environment0, &a, &ty!(apply (item 0) (expr a)))
        .unwrap_err();

    // exists(A -> A = for<'a> A)
    table
        .unify(interner, &environment0, &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
        .unify(interner, &environment0, &a, &ty!(apply (item 0) (expr b)))
        .unwrap();
    table.unify(interner, &environment0, &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
        .unify(interner, &environment0, &b, &ty!(placeholder 1))
        .unwrap();
    table.unify(interner, &environment0, &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.unify(interner, &environment0, &a, &b).unwrap();
    table
        .unify(interner, &environment0, &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
        .unify(interner, &environment0, &a, &ty!(apply (item 0) (expr b)))
        .unwrap();
    table
        .unify(
            interner,
            &environment0,
            &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
        .unify(interner, &environment0, &a, &ty!(apply (item 0) (expr b)))
        .unwrap();
    table
        .unify(interner, &environment0, &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
        .unify(
            interner,
            &environment0,
            &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(
                interner,
                vec![
                    CanonicalVarKind::new(VariableKind::Ty(TyKind::General), U2),
                    CanonicalVarKind::new(VariableKind::Ty(TyKind::General), U1),
                    CanonicalVarKind::new(VariableKind::Ty(TyKind::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
        .unify(
            interner,
            &environment0,
            &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(
                interner,
                vec![
                    CanonicalVarKind::new(VariableKind::Ty(TyKind::General), U1),
                    CanonicalVarKind::new(VariableKind::Ty(TyKind::General), U0),
                    CanonicalVarKind::new(VariableKind::Ty(TyKind::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
        .unify(
            interner,
            &environment0,
            &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(
                interner,
                vec![
                    CanonicalVarKind::new(VariableKind::Ty(TyKind::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 UnificationResult { goals, constraints } =
        table.unify(interner, &environment0, &t_a, &t_b).unwrap();
    assert!(goals.is_empty());
    assert!(constraints.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 UnificationResult { goals, constraints } =
        table.unify(interner, &environment0, &t_c, &t_b).unwrap();
    assert!(goals.is_empty());
    assert_eq!(constraints.len(), 2);
    assert_eq!(
        format!("{:?}", constraints[0]),
        "InEnvironment { environment: Env([]), goal: \'?2: \'!1_0 }",
    );
    assert_eq!(
        format!("{:?}", constraints[1]),
        "InEnvironment { environment: Env([]), goal: \'!1_0: \'?2 }",
    );
}
Commit	Line	Data
f035d41b XL	1	#![cfg(test)]
	2
	3	use super::unify::UnificationResult;
	4	use super::*;
	5	use chalk_integration::interner::ChalkIr;
	6
	7	#[test]
	8	fn infer() {
	9	let interner = &ChalkIr;
	10	let mut table: InferenceTable<ChalkIr> = InferenceTable::new();
	11	let environment0 = Environment::new(interner);
	12	let a = table.new_variable(U0).to_ty(interner);
	13	let b = table.new_variable(U0).to_ty(interner);
	14	table
	15	.unify(interner, &environment0, &a, &ty!(apply (item 0) (expr b)))
	16	.unwrap();
	17	assert_eq!(
	18	table.normalize_deep(interner, &a),
	19	ty!(apply (item 0) (expr b))
	20	);
	21	table
	22	.unify(interner, &environment0, &b, &ty!(apply (item 1)))
	23	.unwrap();
	24	assert_eq!(
	25	table.normalize_deep(interner, &a),
	26	ty!(apply (item 0) (apply (item 1)))
	27	);
	28	}
	29
	30	#[test]
	31	fn universe_error() {
	32	// exists(A -> forall(X -> A = X)) ---> error
	33	let interner = &ChalkIr;
	34	let mut table: InferenceTable<ChalkIr> = InferenceTable::new();
	35	let environment0 = Environment::new(interner);
	36	let a = table.new_variable(U0).to_ty(interner);
	37	table
	38	.unify(interner, &environment0, &a, &ty!(placeholder 1))
	39	.unwrap_err();
	40	}
	41
	42	#[test]
	43	fn cycle_error() {
	44	// exists(A -> A = foo A) ---> error
	45	let interner = &ChalkIr;
	46	let mut table: InferenceTable<ChalkIr> = InferenceTable::new();
	47	let environment0 = Environment::new(interner);
	48	let a = table.new_variable(U0).to_ty(interner);
	49	table
	50	.unify(interner, &environment0, &a, &ty!(apply (item 0) (expr a)))
	51	.unwrap_err();
	52
	53	// exists(A -> A = for<'a> A)
	54	table
	55	.unify(interner, &environment0, &a, &ty!(function 1 (infer 0)))
	56	.unwrap_err();
	57	}
	58
	59	#[test]
	60	fn cycle_indirect() {
	61	// exists(A -> A = foo B, A = B) ---> error
	62	let interner = &ChalkIr;
	63	let mut table: InferenceTable<ChalkIr> = InferenceTable::new();
	64	let environment0 = Environment::new(interner);
65	let a = table.new_variable(U0).to_ty(interner);
66	let b = table.new_variable(U0).to_ty(interner);
67	table
68	.unify(interner, &environment0, &a, &ty!(apply (item 0) (expr b)))
69	.unwrap();
70	table.unify(interner, &environment0, &a, &b).unwrap_err();
71	}
72
73	#[test]
74	fn universe_error_indirect_1() {
75	// exists(A -> forall(X -> exists(B -> B = X, A = B))) ---> error
76	let interner = &ChalkIr;
77	let mut table: InferenceTable<ChalkIr> = InferenceTable::new();
78	let environment0 = Environment::new(interner);
79	let a = table.new_variable(U0).to_ty(interner);
80	let b = table.new_variable(U1).to_ty(interner);
81	table
82	.unify(interner, &environment0, &b, &ty!(placeholder 1))
83	.unwrap();
84	table.unify(interner, &environment0, &a, &b).unwrap_err();
85	}
86
87	#[test]
88	fn universe_error_indirect_2() {
89	// exists(A -> forall(X -> exists(B -> B = A, B = X))) ---> error
90	let interner = &ChalkIr;
91	let mut table: InferenceTable<ChalkIr> = InferenceTable::new();
92	let environment0 = Environment::new(interner);
93	let a = table.new_variable(U0).to_ty(interner);
94	let b = table.new_variable(U1).to_ty(interner);
95	table.unify(interner, &environment0, &a, &b).unwrap();
96	table
97	.unify(interner, &environment0, &b, &ty!(placeholder 1))
98	.unwrap_err();
99	}
100
101	#[test]
102	fn universe_promote() {
103	// exists(A -> forall(X -> exists(B -> A = foo(B), A = foo(i32)))) ---> OK
104	let interner = &ChalkIr;
105	let mut table: InferenceTable<ChalkIr> = InferenceTable::new();
106	let environment0 = Environment::new(interner);
107	let a = table.new_variable(U0).to_ty(interner);
108	let b = table.new_variable(U1).to_ty(interner);
109	table
110	.unify(interner, &environment0, &a, &ty!(apply (item 0) (expr b)))
111	.unwrap();
112	table
113	.unify(
114	interner,
115	&environment0,
116	&a,
117	&ty!(apply (item 0) (apply (item 1))),
118	)
119	.unwrap();
120	}
121
122	#[test]
123	fn universe_promote_bad() {
124	// exists(A -> forall(X -> exists(B -> A = foo(B), B = X))) ---> error
125	let interner = &ChalkIr;
126	let mut table: InferenceTable<ChalkIr> = InferenceTable::new();
127	let environment0 = Environment::new(interner);
128	let a = table.new_variable(U0).to_ty(interner);
129	let b = table.new_variable(U1).to_ty(interner);
130	table
131	.unify(interner, &environment0, &a, &ty!(apply (item 0) (expr b)))
132	.unwrap();
133	table
134	.unify(interner, &environment0, &b, &ty!(placeholder 1))
135	.unwrap_err();
136	}
137
138	#[test]
139	fn projection_eq() {
140	// exists(A -> A = Item0<<A as Item1>::foo>)
141	// ^^^^^^^^^^^^ Can A repeat here? For now,
142	// we say no, but it's an interesting question.
143	let interner = &ChalkIr;
144	let mut table: InferenceTable<ChalkIr> = InferenceTable::new();
145	let environment0 = Environment::new(interner);
146	let a = table.new_variable(U0).to_ty(interner);
147
148	// expect an error ("cycle during unification")
149	table
150	.unify(
151	interner,
152	&environment0,
153	&a,
154	&ty!(apply (item 0) (projection (item 1) (expr a))),
155	)
156	.unwrap_err();
157	}
158
159	const U0: UniverseIndex = UniverseIndex { counter: 0 };
160	const U1: UniverseIndex = UniverseIndex { counter: 1 };
161	const U2: UniverseIndex = UniverseIndex { counter: 2 };
162
163	fn make_table() -> InferenceTable<ChalkIr> {
164	let mut table: InferenceTable<ChalkIr> = InferenceTable::new();
165	let _ = table.new_universe(); // U1
166	let _ = table.new_universe(); // U2
167	table
168	}
169
170	#[test]
171	fn quantify_simple() {
172	let interner = &ChalkIr;
173	let mut table = make_table();
174	let _ = table.new_variable(U0);
175	let _ = table.new_variable(U1);
176	let _ = table.new_variable(U2);
177
178	assert_eq!(
179	table
180	.canonicalize(interner, &ty!(apply (item 0) (infer 2) (infer 1) (infer 0)))
181	.quantified,
182	Canonical {
183	value: ty!(apply (item 0) (bound 0) (bound 1) (bound 2)),
184	binders: CanonicalVarKinds::from(
185	interner,
186	vec![
187	CanonicalVarKind::new(VariableKind::Ty(TyKind::General), U2),
188	CanonicalVarKind::new(VariableKind::Ty(TyKind::General), U1),
189	CanonicalVarKind::new(VariableKind::Ty(TyKind::General), U0),
190	]
191	),
192	}
193	);
194	}
195
196	#[test]
197	fn quantify_bound() {
198	let interner = &ChalkIr;
199	let mut table = make_table();
200	let environment0 = Environment::new(interner);
201
202	let v0 = table.new_variable(U0).to_ty(interner);
203	let v1 = table.new_variable(U1).to_ty(interner);
204	let v2a = table.new_variable(U2).to_ty(interner);
205	let v2b = table.new_variable(U2).to_ty(interner);
206
207	table
208	.unify(
209	interner,
210	&environment0,
211	&v2b,
212	&ty!(apply (item 1) (expr v1) (expr v0)),
213	)
214	.unwrap();
215
216	assert_eq!(
217	table
218	.canonicalize(
219	interner,
220	&ty!(apply (item 0) (expr v2b) (expr v2a) (expr v1) (expr v0))
221	)
222	.quantified,
223	Canonical {
224	value: ty!(apply (item 0) (apply (item 1) (bound 0) (bound 1)) (bound 2) (bound 0) (bound 1)),
225	binders: CanonicalVarKinds::from(
226	interner,
227	vec![
228	CanonicalVarKind::new(VariableKind::Ty(TyKind::General), U1),
229	CanonicalVarKind::new(VariableKind::Ty(TyKind::General), U0),
230	CanonicalVarKind::new(VariableKind::Ty(TyKind::General), U2),
231	]
232	),
233	}
234	);
235	}
236
237	#[test]
238	fn quantify_ty_under_binder() {
239	let interner = &ChalkIr;
240	let mut table = make_table();
241	let v0 = table.new_variable(U0);
242	let v1 = table.new_variable(U0);
243	let _r2 = table.new_variable(U0);
244
245	// Unify v0 and v1.
246	let environment0 = Environment::new(interner);
247	table
248	.unify(
249	interner,
250	&environment0,
251	&v0.to_ty(interner),
252	&v1.to_ty(interner),
253	)
254	.unwrap();
255
256	// Here: the `function` introduces 3 binders, so in the result,
257	// `(bound 3)` references the first canonicalized inference
258	// variable. -- note that `infer 0` and `infer 1` have been
259	// unified above, as well.
260	assert_eq!(
261	table
262	.canonicalize(
263	interner,
264	&ty!(function 3 (apply (item 0) (bound 1) (infer 0) (infer 1) (lifetime (infer 2))))
265	)
266	.quantified,
267	Canonical {
268	value: ty!(function 3 (apply (item 0) (bound 1) (bound 1 0) (bound 1 0) (lifetime (bound 1 1)))),
269	binders: CanonicalVarKinds::from(
270	interner,
271	vec![
272	CanonicalVarKind::new(VariableKind::Ty(TyKind::General), U0),
273	CanonicalVarKind::new(VariableKind::Lifetime, U0)
274	]
275	),
276	}
277	);
278	}
279
280	#[test]
281	fn lifetime_constraint_indirect() {
282	let interner = &ChalkIr;
283	let mut table: InferenceTable<ChalkIr> = InferenceTable::new();
284	let _ = table.new_universe(); // U1
285
286	let _t_0 = table.new_variable(U0);
287	let _l_1 = table.new_variable(U1);
288
289	let environment0 = Environment::new(interner);
290
291	// Here, we unify '?1 (the lifetime variable in universe 1) with
292	// '!1.
293	let t_a = ty!(apply (item 0) (lifetime (placeholder 1)));
294	let t_b = ty!(apply (item 0) (lifetime (infer 1)));
295	let UnificationResult { goals, constraints } =
296	table.unify(interner, &environment0, &t_a, &t_b).unwrap();
297	assert!(goals.is_empty());
298	assert!(constraints.is_empty());
299
300	// Here, we try to unify `?0` (the type variable in universe 0)
301	// with something that involves `'?1`. Since `'?1` has been
302	// unified with `'!1`, and `'!1` is not visible from universe 0,
303	// we will replace `'!1` with a new variable `'?2` and introduce a
304	// (likely unsatisfiable) constraint relating them.
305	let t_c = ty!(infer 0);
306	let UnificationResult { goals, constraints } =
307	table.unify(interner, &environment0, &t_c, &t_b).unwrap();
308	assert!(goals.is_empty());
309	assert_eq!(constraints.len(), 2);
310	assert_eq!(
311	format!("{:?}", constraints[0]),
312	"InEnvironment { environment: Env([]), goal: \'?2: \'!1_0 }",
313	);
314	assert_eq!(
315	format!("{:?}", constraints[1]),
316	"InEnvironment { environment: Env([]), goal: \'!1_0: \'?2 }",
317	);
318	}