Constrained(z, c)`

Premise at line 34. Observed failure causes: failed_judgment.

normalize-r

Line	Coverage	Source
34	5	(prove_normalize(decls, env, assumptions, y) => Constrained(z, c))
35	✗	(prove_after(decls, c, assumptions, Relation::sub(x, &z)) => c)
		──────── ("normalize-r")
37	6	(prove_sub(decls, env, assumptions, x, y) => c)

5 tests failed proving this premise:

Source location: tests/mir_typeck.rs:147

fn foo (b: bool) -> u32 {
    if b {
        return 1_u32;
    } else {
        return false;
    }
}

Failed proof tree

check_all_crates failed mod.rs:41
- args
- rule "check all prefixes" mod.rs:53
  - check_crate failed mod.rs:60
    
    args
    
    rule "check crate" mod.rs:73
    
    check_crate_item failed mod.rs:178
    
    rule "free fn" mod.rs:206
    
    check_free_fn failed fns.rs:14
    
    args
    
    rule "check free fn" fns.rs:24
    
    check_fn failed fns.rs:31
    
    args
    
    rule "check fn" fns.rs:55
    
    check_fn_body failed fns.rs:62
    
    args
    
    rule "expr fn body" fns.rs:90
    
    borrow_check failed nll.rs:127
    
    args
    
    rule "borrow_check" nll.rs:138
    
    borrow_check_block failed nll.rs:145
    
    rule "basic block" nll.rs:160
    
    borrow_check_statement failed nll.rs:177
    
    args
    
    rule "if" nll.rs:221
    
    borrow_check_block failed nll.rs:145
    
    args
    
    rule "basic block" nll.rs:160
    
    borrow_check_statement failed nll.rs:177
    
    args
    
    rule "return" nll.rs:282
    
    prove_assignable failed nll.rs:1067
    
    args
    
    rule "subtype" nll.rs:1085
    
    prove failed function.rs:250
    
    args
    
    rule function.rs:250
    
    prove_wc_list failed prove_wc_list.rs:8
    
    args
    
    rule "some" prove_wc_list.rs:26
    
    prove_wc failed prove_wc.rs:21
    
    args
    
    rule "subtype" prove_wc.rs:131
    
    prove_sub failed prove_sub.rs:12
    
    args
    
    rule "normalize-r" prove_sub.rs:34
    
    prove_normalize failed prove_normalize.rs:20
    
    args
    
    rule "if" nll.rs:221
    
    borrow_check_block failed nll.rs:145
    
    args
    
    rule "basic block" nll.rs:160
    
    borrow_check_statement failed nll.rs:177
    
    args
    
    rule "return" nll.rs:282
    
    prove_assignable failed nll.rs:1067
    
    args
    
    rule "subtype" nll.rs:1085
    
    prove failed function.rs:250
    
    args
    
    rule function.rs:250
    
    prove_wc_list failed prove_wc_list.rs:8
    
    args
    
    rule "some" prove_wc_list.rs:26
    
    prove_wc failed prove_wc.rs:21
    
    args
    
    rule "subtype" prove_wc.rs:131
    
    prove_sub failed prove_sub.rs:12
    
    args
    
    rule "normalize-r" prove_sub.rs:34
    
    prove_normalize failed prove_normalize.rs:20
    
    args

Source location: tests/mir_typeck.rs:300

fn bar(v1: ()) -> () {
    let v0: () = foo(v1);
    return v0;
}

Failed proof tree

check_all_crates failed mod.rs:41
- args
- rule "check all prefixes" mod.rs:53
  - check_crate failed mod.rs:60
    
    args
    
    rule "check crate" mod.rs:73
    
    check_crate_item failed mod.rs:178
    
    rule "free fn" mod.rs:206
    
    check_free_fn failed fns.rs:14
    
    args
    
    rule "check free fn" fns.rs:24
    
    check_fn failed fns.rs:31
    
    args
    
    rule "check fn" fns.rs:55
    
    check_fn_body failed fns.rs:62
    
    args
    
    rule "expr fn body" fns.rs:90
    
    borrow_check failed nll.rs:127
    
    args
    
    rule "borrow_check" nll.rs:138
    
    borrow_check_block failed nll.rs:145
    
    rule "basic block" nll.rs:160
    
    borrow_check_statement failed nll.rs:177
    
    args
    
    rule "let" nll.rs:194
    
    borrow_check_expr_has_ty failed nll.rs:351
    
    args
    
    rule "block" nll.rs:364
    
    borrow_check_expr failed nll.rs:372
    
    args
    
    rule "call" nll.rs:443
    
    borrow_check_expr_has_ty failed nll.rs:351
    
    args
    
    rule "block" nll.rs:365
    
    prove_assignable failed nll.rs:1067
    
    args
    
    rule "subtype" nll.rs:1085
    
    prove failed function.rs:250
    
    args
    
    rule function.rs:250
    
    prove_wc_list failed prove_wc_list.rs:8
    
    args
    
    rule "some" prove_wc_list.rs:26
    
    prove_wc failed prove_wc.rs:21
    
    args
    
    rule "subtype" prove_wc.rs:131
    
    prove_sub failed prove_sub.rs:12
    
    args
    
    rule "normalize-r" prove_sub.rs:34
    
    prove_normalize failed prove_normalize.rs:20
    
    args
    
    rule "block" nll.rs:365
    
    prove_assignable failed nll.rs:1067
    
    args
    
    rule "subtype" nll.rs:1085
    
    prove failed function.rs:250
    
    args
    
    rule function.rs:250
    
    prove_wc_list failed prove_wc_list.rs:8
    
    args
    
    rule "some" prove_wc_list.rs:26
    
    prove_wc failed prove_wc.rs:21
    
    args
    
    rule "subtype" prove_wc.rs:131
    
    prove_sub failed prove_sub.rs:12
    
    args
    
    rule "normalize-r" prove_sub.rs:34
    
    prove_normalize failed prove_normalize.rs:20
    
    args

Source location: tests/mir_typeck.rs:360

fn bar(v1: u32) -> u32 {
    let v0: u32 = identity::<bool>(v1);
    return v0;
}

Failed proof tree

check_all_crates failed mod.rs:41
- args
- rule "check all prefixes" mod.rs:53
  - check_crate failed mod.rs:60
    
    args
    
    rule "check crate" mod.rs:73
    
    check_crate_item failed mod.rs:178
    
    rule "free fn" mod.rs:206
    
    check_free_fn failed fns.rs:14
    
    args
    
    rule "check free fn" fns.rs:24
    
    check_fn failed fns.rs:31
    
    args
    
    rule "check fn" fns.rs:55
    
    check_fn_body failed fns.rs:62
    
    args
    
    rule "expr fn body" fns.rs:90
    
    borrow_check failed nll.rs:127
    
    args
    
    rule "borrow_check" nll.rs:138
    
    borrow_check_block failed nll.rs:145
    
    rule "basic block" nll.rs:160
    
    borrow_check_statement failed nll.rs:177
    
    args
    
    rule "let" nll.rs:194
    
    borrow_check_expr_has_ty failed nll.rs:351
    
    args
    
    rule "block" nll.rs:364
    
    borrow_check_expr failed nll.rs:372
    
    args
    
    rule "call" nll.rs:443
    
    borrow_check_expr_has_ty failed nll.rs:351
    
    args
    
    rule "block" nll.rs:365
    
    prove_assignable failed nll.rs:1067
    
    args
    
    rule "subtype" nll.rs:1085
    
    prove failed function.rs:250
    
    args
    
    rule function.rs:250
    
    prove_wc_list failed prove_wc_list.rs:8
    
    args
    
    rule "some" prove_wc_list.rs:26
    
    prove_wc failed prove_wc.rs:21
    
    args
    
    rule "subtype" prove_wc.rs:131
    
    prove_sub failed prove_sub.rs:12
    
    args
    
    rule "normalize-r" prove_sub.rs:34
    
    prove_normalize failed prove_normalize.rs:20
    
    args
    
    rule "block" nll.rs:365
    
    prove_assignable failed nll.rs:1067
    
    args
    
    rule "subtype" nll.rs:1085
    
    prove failed function.rs:250
    
    args
    
    rule function.rs:250
    
    prove_wc_list failed prove_wc_list.rs:8
    
    args
    
    rule "some" prove_wc_list.rs:26
    
    prove_wc failed prove_wc.rs:21
    
    args
    
    rule "subtype" prove_wc.rs:131
    
    prove_sub failed prove_sub.rs:12
    
    args
    
    rule "normalize-r" prove_sub.rs:34
    
    prove_normalize failed prove_normalize.rs:20
    
    args

Source location: tests/mir_typeck.rs:421

fn foo (v1: ()) -> u32 {
    return v1;
}

Failed proof tree

check_all_crates failed mod.rs:41
- args
- rule "check all prefixes" mod.rs:53
  - check_crate failed mod.rs:60
    
    args
    
    rule "check crate" mod.rs:73
    
    check_crate_item failed mod.rs:178
    
    rule "free fn" mod.rs:206
    
    check_free_fn failed fns.rs:14
    
    args
    
    rule "check free fn" fns.rs:24
    
    check_fn failed fns.rs:31
    
    args
    
    rule "check fn" fns.rs:55
    
    check_fn_body failed fns.rs:62
    
    args
    
    rule "expr fn body" fns.rs:90
    
    borrow_check failed nll.rs:127
    
    args
    
    rule "borrow_check" nll.rs:138
    
    borrow_check_block failed nll.rs:145
    
    rule "basic block" nll.rs:160
    
    borrow_check_statement failed nll.rs:177
    
    args
    
    rule "return" nll.rs:282
    
    prove_assignable failed nll.rs:1067
    
    args
    
    rule "subtype" nll.rs:1085
    
    prove failed function.rs:250
    
    args
    
    rule function.rs:250
    
    prove_wc_list failed prove_wc_list.rs:8
    
    args
    
    rule "some" prove_wc_list.rs:26
    
    prove_wc failed prove_wc.rs:21
    
    args
    
    rule "subtype" prove_wc.rs:131
    
    prove_sub failed prove_sub.rs:12
    
    args
    
    rule "normalize-r" prove_sub.rs:34
    
    prove_normalize failed prove_normalize.rs:20
    
    args
    
    rule "return" nll.rs:282
    
    prove_assignable failed nll.rs:1067
    
    args
    
    rule "subtype" nll.rs:1085
    
    prove failed function.rs:250
    
    args
    
    rule function.rs:250
    
    prove_wc_list failed prove_wc_list.rs:8
    
    args
    
    rule "some" prove_wc_list.rs:26
    
    prove_wc failed prove_wc.rs:21
    
    args
    
    rule "subtype" prove_wc.rs:131
    
    prove_sub failed prove_sub.rs:12
    
    args
    
    rule "normalize-r" prove_sub.rs:34
    
    prove_normalize failed prove_normalize.rs:20
    
    args

Source location: tests/mir_typeck.rs:630

fn foo (v1: u32) -> u32 {
    let v2: Dummy = Dummy { value: false };
    return v1;
}

Failed proof tree

check_all_crates failed mod.rs:41
- args
- rule "check all prefixes" mod.rs:53
  - check_crate failed mod.rs:60
    
    args
    
    rule "check crate" mod.rs:73
    
    check_crate_item failed mod.rs:178
    
    rule "free fn" mod.rs:206
    
    check_free_fn failed fns.rs:14
    
    args
    
    rule "check free fn" fns.rs:24
    
    check_fn failed fns.rs:31
    
    args
    
    rule "check fn" fns.rs:55
    
    check_fn_body failed fns.rs:62
    
    args
    
    rule "expr fn body" fns.rs:90
    
    borrow_check failed nll.rs:127
    
    args
    
    rule "borrow_check" nll.rs:138
    
    borrow_check_block failed nll.rs:145
    
    rule "basic block" nll.rs:160
    
    borrow_check_statement failed nll.rs:177
    
    args
    
    rule "let" nll.rs:194
    
    borrow_check_expr_has_ty failed nll.rs:351
    
    args
    
    rule "block" nll.rs:364
    
    borrow_check_expr failed nll.rs:372
    
    args
    
    rule "struct" nll.rs:564
    
    borrow_check_expr_has_ty failed nll.rs:351
    
    args
    
    rule "block" nll.rs:365
    
    prove_assignable failed nll.rs:1067
    
    args
    
    rule "subtype" nll.rs:1085
    
    prove failed function.rs:250
    
    args
    
    rule function.rs:250
    
    prove_wc_list failed prove_wc_list.rs:8
    
    args
    
    rule "some" prove_wc_list.rs:26
    
    prove_wc failed prove_wc.rs:21
    
    args
    
    rule "subtype" prove_wc.rs:131
    
    prove_sub failed prove_sub.rs:12
    
    args
    
    rule "normalize-r" prove_sub.rs:34
    
    prove_normalize failed prove_normalize.rs:20
    
    args

Keyboard shortcuts

A MIR Formality

Negative coverage: prove_sub / normalize-r / premise prove_normalize(decls, env, assumptions, y) => Constrained(z, c)

Negative coverage: `prove_sub` / `normalize-r` / premise `prove_normalize(decls, env, assumptions, y) => Constrained(z, c)`