Negative coverage: check_fn_in_impl / check_fn_in_impl / premise super::fns::check_fn(program, env, impl_assumptions, ii_fn, crate_id) => ()
Premise at line 194. Observed failure causes: failed_judgment.
check_fn_in_impl| Line | Coverage | Source |
|---|---|---|
| 188 | ✗ | (if let Some(ti_fn) = trait_items .iter() .downcasted::<Fn>() .find(|trait_f| trait_f.id == ii_fn.id)) |
| 194 | 1 | (super::fns::check_fn(program, env, impl_assumptions, ii_fn, crate_id) => ()) |
| 197 | ✗ | (scope(enter_universally(env, &merge_binders(&ii_fn.binder, &ti_fn.binder)?) => (env, ( FnBoundData { input_args: ii_input_args, output_ty: ii_output_ty, where_clauses: ii_where_clauses, body: _ }, FnBoundData { input_args: ti_input_args, output_ty: ti_output_ty, where_clauses: ti_where_clauses, body: _ }, ))) with() // Prove impl where-clauses follow from trait where-clauses (super::prove_goal(program, env, (impl_assumptions, ti_where_clauses), ii_where_clauses) => ()) // Check argument count matches (if ii_input_args.len() == ti_input_args.len()) // Check each argument: trait arg is subtype of impl arg (contravariance) (for_all(pair in ii_input_args.iter().zip(ti_input_args.iter())) (let (ii_input_arg, ti_input_arg) = pair) (super::prove_goal(program, env, (impl_assumptions, ii_where_clauses), AtomicPredicate::sub(&ti_input_arg.ty, &ii_input_arg.ty)) => ())) // Check return type: impl return is subtype of trait return (covariance) (super::prove_goal(program, env, (impl_assumptions, ii_where_clauses), AtomicPredicate::sub(ii_output_ty, ti_output_ty)) => ())) |
| ──────── ("check_fn_in_impl") | ||
| 218 | 5 | (check_fn_in_impl(program, env, impl_assumptions, trait_items, ii_fn, crate_id) => ()) |
1 test failed proving this premise:
Source location: tests/drop.rs:83 (all coverage from this test)
Failed proof tree
check_all_crates failedmod.rs:42args
rule "check all prefixes"mod.rs:54check_crate failedmod.rs:61args
rule "check crate"mod.rs:74check_crate_item failedmod.rs:179rule "trait impl"mod.rs:194check_trait_impl failedimpls.rs:14rule "check_trait_impl"impls.rs:36check_trait_impl_item failedimpls.rs:151rule "fn in impl"impls.rs:163check_fn_in_impl failedimpls.rs:176rule "check_fn_in_impl"impls.rs:194check_fn failedfns.rs:31args
rule "check fn"fns.rs:50prove failedfunction.rs:250args
rulefunction.rs:250prove_predicate_list failedprove_predicate_list.rs:8args
rule "some"prove_predicate_list.rs:26prove_predicate failedprove_predicate.rs:22args
rule "assumption"prove_predicate.rs:48prove_via failedprove_via.rs:9args
rule "parameter well formed"prove_predicate.rs:149prove_wf failedprove_wf.rs:11args
rule "ADT"prove_wf.rs:64prove_after failedprove_after.rs:8args
rule "prove_after"prove_after.rs:19prove failedprove_after.rs:19args
ruleprove_after.rs:19prove_predicate_list failedprove_predicate_list.rs:8args
rule "some"prove_predicate_list.rs:26prove_predicate failedprove_predicate.rs:22args
rule "assumption"prove_predicate.rs:48prove_via failedprove_via.rs:9args
rule "trait implied bound"prove_predicate.rs:106 (failed: empty_collection)