vendor/chalk-solve-0.55.0/src/infer/test.rs

   1 #![cfg(test)]
   2
   3 use super::unify::RelationResult;
   4 use super::*;
   5 use chalk_integration::interner::ChalkIr;
   6 use chalk_integration::{arg, lifetime, ty};
   7
   8 // We just use a vec of 20 `Invariant`, since this is zipped and no substs are
   9 // longer than this
  10 #[derive(Debug)]
  11 struct TestDatabase;
  12 impl UnificationDatabase<ChalkIr> for TestDatabase {
  13     fn fn_def_variance(&self, _fn_def_id: FnDefId<ChalkIr>) -> Variances<ChalkIr> {
  14         Variances::from_iter(&ChalkIr, [Variance::Invariant; 20].iter().copied())
  15     }
  16
  17     fn adt_variance(&self, _adt_id: AdtId<ChalkIr>) -> Variances<ChalkIr> {
  18         Variances::from_iter(&ChalkIr, [Variance::Invariant; 20].iter().copied())
  19     }
  20 }
  21
  22 #[test]
  23 fn universe_error() {
  24     // exists(A -> forall(X -> A = X)) ---> error
  25     let interner = &ChalkIr;
  26     let mut table: InferenceTable<ChalkIr> = InferenceTable::new();
  27     let environment0 = Environment::new(interner);
  28     let a = table.new_variable(U0).to_ty(interner);
  29     table
  30         .relate(
  31             interner,
  32             &TestDatabase,
  33             &environment0,
  34             Variance::Invariant,
  35             &a,
  36             &ty!(placeholder 1),
  37         )
  38         .unwrap_err();
  39 }
  40
  41 #[test]
  42 fn cycle_error() {
  43     // exists(A -> A = foo A) ---> error
  44     let interner = &ChalkIr;
  45     let mut table: InferenceTable<ChalkIr> = InferenceTable::new();
  46     let environment0 = Environment::new(interner);
  47     let a = table.new_variable(U0).to_ty(interner);
  48     table
  49         .relate(
  50             interner,
  51             &TestDatabase,
  52             &environment0,
  53             Variance::Invariant,
  54             &a,
  55             &ty!(apply (item 0) (expr a)),
  56         )
  57         .unwrap_err();
  58
  59     // exists(A -> A = for<'a> A)
  60     table
  61         .relate(
  62             interner,
  63             &TestDatabase,
  64             &environment0,
  65             Variance::Invariant,
  66             &a,
  67             &ty!(function 1 (infer 0)),
  68         )
  69         .unwrap_err();
  70 }
  71
  72 #[test]
  73 fn cycle_indirect() {
  74     // exists(A -> A = foo B, A = B) ---> error
  75     let interner = &ChalkIr;
  76     let mut table: InferenceTable<ChalkIr> = InferenceTable::new();
  77     let environment0 = Environment::new(interner);
  78     let a = table.new_variable(U0).to_ty(interner);
  79     let b = table.new_variable(U0).to_ty(interner);
  80     table
  81         .relate(
  82             interner,
  83             &TestDatabase,
  84             &environment0,
  85             Variance::Invariant,
  86             &a,
  87             &ty!(apply (item 0) (expr b)),
  88         )
  89         .unwrap();
  90     table
  91         .relate(
  92             interner,
  93             &TestDatabase,
  94             &environment0,
  95             Variance::Invariant,
  96             &a,
  97             &b,
  98         )
  99         .unwrap_err();
 100 }
 101
 102 #[test]
 103 fn universe_error_indirect_1() {
 104     // exists(A -> forall(X -> exists(B -> B = X, A = B))) ---> error
 105     let interner = &ChalkIr;
 106     let mut table: InferenceTable<ChalkIr> = InferenceTable::new();
 107     let environment0 = Environment::new(interner);
 108     let a = table.new_variable(U0).to_ty(interner);
 109     let b = table.new_variable(U1).to_ty(interner);
 110     table
 111         .relate(
 112             interner,
 113             &TestDatabase,
 114             &environment0,
 115             Variance::Invariant,
 116             &b,
 117             &ty!(placeholder 1),
 118         )
 119         .unwrap();
 120     table
 121         .relate(
 122             interner,
 123             &TestDatabase,
 124             &environment0,
 125             Variance::Invariant,
 126             &a,
 127             &b,
 128         )
 129         .unwrap_err();
 130 }
 131
 132 #[test]
 133 fn universe_error_indirect_2() {
 134     // exists(A -> forall(X -> exists(B -> B = A, B = X))) ---> error
 135     let interner = &ChalkIr;
 136     let mut table: InferenceTable<ChalkIr> = InferenceTable::new();
 137     let environment0 = Environment::new(interner);
 138     let a = table.new_variable(U0).to_ty(interner);
 139     let b = table.new_variable(U1).to_ty(interner);
 140     table
 141         .relate(
 142             interner,
 143             &TestDatabase,
 144             &environment0,
 145             Variance::Invariant,
 146             &a,
 147             &b,
 148         )
 149         .unwrap();
 150     table
 151         .relate(
 152             interner,
 153             &TestDatabase,
 154             &environment0,
 155             Variance::Invariant,
 156             &b,
 157             &ty!(placeholder 1),
 158         )
 159         .unwrap_err();
 160 }
 161
 162 #[test]
 163 fn universe_promote() {
 164     // exists(A -> forall(X -> exists(B -> A = foo(B), A = foo(i32)))) ---> OK
 165     let interner = &ChalkIr;
 166     let mut table: InferenceTable<ChalkIr> = InferenceTable::new();
 167     let environment0 = Environment::new(interner);
 168     let a = table.new_variable(U0).to_ty(interner);
 169     let b = table.new_variable(U1).to_ty(interner);
 170     table
 171         .relate(
 172             interner,
 173             &TestDatabase,
 174             &environment0,
 175             Variance::Invariant,
 176             &a,
 177             &ty!(apply (item 0) (expr b)),
 178         )
 179         .unwrap();
 180     table
 181         .relate(
 182             interner,
 183             &TestDatabase,
 184             &environment0,
 185             Variance::Invariant,
 186             &a,
 187             &ty!(apply (item 0) (apply (item 1))),
 188         )
 189         .unwrap();
 190 }
 191
 192 #[test]
 193 fn universe_promote_bad() {
 194     // exists(A -> forall(X -> exists(B -> A = foo(B), B = X))) ---> error
 195     let interner = &ChalkIr;
 196     let mut table: InferenceTable<ChalkIr> = InferenceTable::new();
 197     let environment0 = Environment::new(interner);
 198     let a = table.new_variable(U0).to_ty(interner);
 199     let b = table.new_variable(U1).to_ty(interner);
 200     table
 201         .relate(
 202             interner,
 203             &TestDatabase,
 204             &environment0,
 205             Variance::Invariant,
 206             &a,
 207             &ty!(apply (item 0) (expr b)),
 208         )
 209         .unwrap();
 210     table
 211         .relate(
 212             interner,
 213             &TestDatabase,
 214             &environment0,
 215             Variance::Invariant,
 216             &b,
 217             &ty!(placeholder 1),
 218         )
 219         .unwrap_err();
 220 }
 221
 222 #[test]
 223 fn projection_eq() {
 224     // exists(A -> A = Item0<<A as Item1>::foo>)
 225     //                       ^^^^^^^^^^^^ Can A repeat here? For now,
 226     //                       we say no, but it's an interesting question.
 227     let interner = &ChalkIr;
 228     let mut table: InferenceTable<ChalkIr> = InferenceTable::new();
 229     let environment0 = Environment::new(interner);
 230     let a = table.new_variable(U0).to_ty(interner);
 231
 232     // expect an error ("cycle during unification")
 233     table
 234         .relate(
 235             interner,
 236             &TestDatabase,
 237             &environment0,
 238             Variance::Invariant,
 239             &a,
 240             &ty!(apply (item 0) (projection (item 1) (expr a))),
 241         )
 242         .unwrap_err();
 243 }
 244
 245 const U0: UniverseIndex = UniverseIndex { counter: 0 };
 246 const U1: UniverseIndex = UniverseIndex { counter: 1 };
 247 const U2: UniverseIndex = UniverseIndex { counter: 2 };
 248
 249 fn make_table() -> InferenceTable<ChalkIr> {
 250     let mut table: InferenceTable<ChalkIr> = InferenceTable::new();
 251     let _ = table.new_universe(); // U1
 252     let _ = table.new_universe(); // U2
 253     table
 254 }
 255
 256 #[test]
 257 fn quantify_simple() {
 258     let interner = &ChalkIr;
 259     let mut table = make_table();
 260     let _ = table.new_variable(U0);
 261     let _ = table.new_variable(U1);
 262     let _ = table.new_variable(U2);
 263
 264     assert_eq!(
 265         table
 266             .canonicalize(interner, ty!(apply (item 0) (infer 2) (infer 1) (infer 0)))
 267             .quantified,
 268         Canonical {
 269             value: ty!(apply (item 0) (bound 0) (bound 1) (bound 2)),
 270             binders: CanonicalVarKinds::from_iter(
 271                 interner,
 272                 vec![
 273                     CanonicalVarKind::new(VariableKind::Ty(TyVariableKind::General), U2),
 274                     CanonicalVarKind::new(VariableKind::Ty(TyVariableKind::General), U1),
 275                     CanonicalVarKind::new(VariableKind::Ty(TyVariableKind::General), U0),
 276                 ]
 277             ),
 278         }
 279     );
 280 }
 281
 282 #[test]
 283 fn quantify_bound() {
 284     let interner = &ChalkIr;
 285     let mut table = make_table();
 286     let environment0 = Environment::new(interner);
 287
 288     let v0 = table.new_variable(U0).to_ty(interner);
 289     let v1 = table.new_variable(U1).to_ty(interner);
 290     let v2a = table.new_variable(U2).to_ty(interner);
 291     let v2b = table.new_variable(U2).to_ty(interner);
 292
 293     table
 294         .relate(
 295             interner,
 296             &TestDatabase,
 297             &environment0,
 298             Variance::Invariant,
 299             &v2b,
 300             &ty!(apply (item 1) (expr v1) (expr v0)),
 301         )
 302         .unwrap();
 303
 304     assert_eq!(
 305         table
 306             .canonicalize(
 307                 interner,
 308                 ty!(apply (item 0) (expr v2b) (expr v2a) (expr v1) (expr v0))
 309             )
 310             .quantified,
 311         Canonical {
 312             value: ty!(apply (item 0) (apply (item 1) (bound 0) (bound 1)) (bound 2) (bound 0) (bound 1)),
 313             binders: CanonicalVarKinds::from_iter(
 314                 interner,
 315                 vec![
 316                     CanonicalVarKind::new(VariableKind::Ty(TyVariableKind::General), U1),
 317                     CanonicalVarKind::new(VariableKind::Ty(TyVariableKind::General), U0),
 318                     CanonicalVarKind::new(VariableKind::Ty(TyVariableKind::General), U2),
 319                 ]
 320             ),
 321         }
 322     );
 323 }
 324
 325 #[test]
 326 fn quantify_ty_under_binder() {
 327     let interner = &ChalkIr;
 328     let mut table = make_table();
 329     let v0 = table.new_variable(U0);
 330     let v1 = table.new_variable(U0);
 331     let _r2 = table.new_variable(U0);
 332
 333     // Unify v0 and v1.
 334     let environment0 = Environment::new(interner);
 335     table
 336         .relate(
 337             interner,
 338             &TestDatabase,
 339             &environment0,
 340             Variance::Invariant,
 341             &v0.to_ty(interner),
 342             &v1.to_ty(interner),
 343         )
 344         .unwrap();
 345
 346     // Here: the `function` introduces 3 binders, so in the result,
 347     // `(bound 3)` references the first canonicalized inference
 348     // variable. -- note that `infer 0` and `infer 1` have been
 349     // unified above, as well.
 350     assert_eq!(
 351         table
 352             .canonicalize(
 353                 interner,
 354                 ty!(function 3 (apply (item 0) (bound 1) (infer 0) (infer 1) (lifetime (infer 2))))
 355             )
 356             .quantified,
 357         Canonical {
 358             value: ty!(function 3 (apply (item 0) (bound 1) (bound 1 0) (bound 1 0) (lifetime (bound 1 1)))),
 359             binders: CanonicalVarKinds::from_iter(
 360                 interner,
 361                 vec![
 362                     CanonicalVarKind::new(VariableKind::Ty(TyVariableKind::General), U0),
 363                     CanonicalVarKind::new(VariableKind::Lifetime, U0)
 364                 ]
 365             ),
 366         }
 367     );
 368 }
 369
 370 #[test]
 371 fn lifetime_constraint_indirect() {
 372     let interner = &ChalkIr;
 373     let mut table: InferenceTable<ChalkIr> = InferenceTable::new();
 374     let _ = table.new_universe(); // U1
 375
 376     let _t_0 = table.new_variable(U0);
 377     let _l_1 = table.new_variable(U1);
 378
 379     let environment0 = Environment::new(interner);
 380
 381     // Here, we unify '?1 (the lifetime variable in universe 1) with
 382     // '!1.
 383     let t_a = ty!(apply (item 0) (lifetime (placeholder 1)));
 384     let t_b = ty!(apply (item 0) (lifetime (infer 1)));
 385     let RelationResult { goals } = table
 386         .relate(
 387             interner,
 388             &TestDatabase,
 389             &environment0,
 390             Variance::Invariant,
 391             &t_a,
 392             &t_b,
 393         )
 394         .unwrap();
 395     assert!(goals.is_empty());
 396
 397     // Here, we try to unify `?0` (the type variable in universe 0)
 398     // with something that involves `'?1`. Since `'?1` has been
 399     // unified with `'!1`, and `'!1` is not visible from universe 0,
 400     // we will replace `'!1` with a new variable `'?2` and introduce a
 401     // (likely unsatisfiable) constraint relating them.
 402     let t_c = ty!(infer 0);
 403     let RelationResult { goals } = table
 404         .relate(
 405             interner,
 406             &TestDatabase,
 407             &environment0,
 408             Variance::Invariant,
 409             &t_c,
 410             &t_b,
 411         )
 412         .unwrap();
 413     assert_eq!(goals.len(), 2);
 414     assert_eq!(
 415         format!("{:?}", goals[0]),
 416         "InEnvironment { environment: Env([]), goal: \'?2: \'!1_0 }",
 417     );
 418     assert_eq!(
 419         format!("{:?}", goals[1]),
 420         "InEnvironment { environment: Env([]), goal: \'!1_0: \'?2 }",
 421     );
 422 }