Repository: rust-lang/rust
File: compiler/rustc_trait_selection/src/traits/coherence.rs (Rust)

Code before:
    };

    // FIXME(with_negative_coherence): the infcx has constraints from equating
    // the impl headers. We should use these constraints as assumptions, not as
    // requirements, when proving the negated where clauses below.
    drop(equate_obligations);
    drop(infcx.take_registered_region_obligations());
    drop(infcx.take_registered_region_assumptions());
    drop(infcx.take_and_reset_region_constraints());

    plug_infer_with_placeholders(
        infcx,
        root_universe,
        (impl1_header.impl_args, impl2_header.impl_args),
    );

    let impl1_header_args = infcx.resolve_vars_if_possible(impl1_header.impl_args);
    let param_env =
        ty::EarlyBinder::bind(tcx.param_env(impl1_def_id)).instantiate(tcx, impl1_header_args);

    util::elaborate(tcx, tcx.predicates_of(impl2_def_id).instantiate(tcx, impl2_header.impl_args))
        .elaborate_sized()
        .any(|(clause, _)| try_prove_negated_where_clause(infcx, clause, param_env))
}

fn plug_infer_with_placeholders<'tcx>(
    infcx: &InferCtxt<'tcx>,
    universe: ty::UniverseIndex,
    value: impl TypeVisitable<TyCtxt<'tcx>>,
) {
    struct PlugInferWithPlaceholder<'a, 'tcx> {
        infcx: &'a InferCtxt<'tcx>,
        universe: ty::UniverseIndex,
        var: ty::BoundVar,
    }

    impl<'tcx> PlugInferWithPlaceholder<'_, 'tcx> {
        fn next_var(&mut self) -> ty::BoundVar {
            let var = self.var;
            self.var = self.var + 1;
            var
        }
    }

    impl<'tcx> TypeVisitor<TyCtxt<'tcx>> for PlugInferWithPlaceholder<'_, 'tcx> {
        fn visit_ty(&mut self, ty: Ty<'tcx>) {
            let ty = self.infcx.shallow_resolve(ty);
            if ty.is_ty_var() {
                let Ok(InferOk { value: (), obligations }) =
                    self.infcx.at(&ObligationCause::dummy(), ty::ParamEnv::empty()).eq(
                        // Comparing against a type variable never registers hidden types anyway

Review comment (bug):
Is it correct to assume this wont have any infer vars? 🤔 I would expect something like:
```rust
trait Bound {}
impl<T: ?Sized> !Bound for T {}

trait Trait {}
impl<T: Sized> Trait for T {}
impl<T: Bound> Trait for T {}
```
to result in the resolved impl1 header args to still be some infer var `?x`, resulting in a param env with `?x: Sized` when trying to prove `?x: !Bound`. Though this example fails to compile for other reasons :>

Code after:
    else {
        return false;
    };

    // FIXME(with_negative_coherence): the infcx has constraints from equating
    // the impl headers. We should use these constraints as assumptions, not as
    // requirements, when proving the negated where clauses below.
    drop(equate_obligations);
    drop(infcx.take_registered_region_obligations());
    drop(infcx.take_registered_region_assumptions());
    drop(infcx.take_and_reset_region_constraints());

    plug_infer_with_placeholders(
        infcx,
        root_universe,
        (impl1_header.impl_args, impl2_header.impl_args),
    );

    // Right above we plug inference variables with placeholders,
    // this gets us new impl1_header_args with the inference variables actually resolved
    // to those placeholders.
    let impl1_header_args = infcx.resolve_vars_if_possible(impl1_header.impl_args);
    // So there are no infer variables left now, except regions which aren't resolved by `resolve_vars_if_possible`.
    assert!(!impl1_header_args.has_non_region_infer());

    let param_env =
        ty::EarlyBinder::bind(tcx.param_env(impl1_def_id)).instantiate(tcx, impl1_header_args);

    util::elaborate(tcx, tcx.predicates_of(impl2_def_id).instantiate(tcx, impl2_header.impl_args))
        .elaborate_sized()
        .any(|(clause, _)| try_prove_negated_where_clause(infcx, clause, param_env))
}

fn plug_infer_with_placeholders<'tcx>(
    infcx: &InferCtxt<'tcx>,
    universe: ty::UniverseIndex,
    value: impl TypeVisitable<TyCtxt<'tcx>>,
) {
    struct PlugInferWithPlaceholder<'a, 'tcx> {
        infcx: &'a InferCtxt<'tcx>,
        universe: ty::UniverseIndex,
        var: ty::BoundVar,
    }

    impl<'tcx> PlugInferWithPlaceholder<'_, 'tcx> {
        fn next_var(&mut self) -> ty::BoundVar {
            let var = self.var;
            self.var = self.var + 1;
            var
        }
    }