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

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