Rewrite effects checking chapter

src/SUMMARY.md

@@ -177,7 +177,7 @@
         - [Inference details](./opaque-types-impl-trait-inference.md)
         - [Return Position Impl Trait In Trait](./return-position-impl-trait-in-trait.md)
         - [Region inference restrictions][opaque-infer]
-- [Effect checking](./effects.md)
+- [Const condition checking](./effects.md)
 - [Pattern and Exhaustiveness Checking](./pat-exhaustive-checking.md)
 - [Unsafety Checking](./unsafety-checking.md)
 - [MIR dataflow](./mir/dataflow.md)

src/effects.md

@@ -1,66 +1,130 @@
-# Effects and effect checking
-
-Note: all of this describes the implementation of the unstable `effects` and
-`const_trait_impl` features. None of this implementation is usable or visible from
-stable Rust.
-
-The implementation of const traits and `~const` bounds is a limited effect system.
-It is used to allow trait bounds on `const fn` to be used within the `const fn` for
-method calls. Within the function, in order to know whether a method on a trait
-bound is `const`, we need to know whether there is a `~const` bound for the trait.
-In order to know whether we can instantiate a `~const` bound on a `const fn`, we
-need to know whether there is a `const_trait` impl for the type and trait being
-used (or whether the `const fn` is used at runtime, then any type implementing the
-trait is ok, just like with other bounds).
-
-We perform these checks via a const generic boolean that gets attached to all
-`const fn` and `const trait`. The following sections will explain the desugarings
-and the way we perform the checks at call sites.
-
-The const generic boolean is inverted to the meaning of `const`. In the compiler
-it is called `host`, because it enables "host APIs" like `static` items, network
-access, disk access, random numbers and everything else that isn't available in
-`const` contexts. So `false` means "const", `true` means "not const" and if it's
-a generic parameter, it means "maybe const" (meaning we're in a const fn or const
-trait).
-
-## `const fn`
-
-All `const fn` have a `#[rustc_host] const host: bool` generic parameter that is
-hidden from users. Any `~const Trait` bounds in the generics list or `where` bounds
-of a `const fn` get converted to `Trait<host> + Trait<true>` bounds. The `Trait<true>`
-exists so that associated types of the generic param can be used from projections
-like `<T as Trait>::Assoc`, because there are no `<T as ~const Trait>` projections for now.
-
-## `#[const_trait] trait`s
-
-The `#[const_trait]` attribute gives the marked trait a `#[rustc_host] const host: bool`
-generic parameter. All functions of the trait "inherit" this generic parameter, just like
-they have all the regular generic parameters of the trait. Any `~const Trait` super-trait
-bounds get desugared to `Trait<host> + Trait<true>` in order to allow using associated
-types and consts of the super traits in the trait declaration. This is necessary, because
-`<Self as SuperTrait>::Assoc` is always `<Self as SuperTrait<true>>::Assoc` as there is
-no `<Self as ~const SuperTrait>` syntax.
-
-## `typeck` performing method and function call checks.
-
-When generic parameters are instantiated for any items, the `host` generic parameter
-is always instantiated as an inference variable. This is a special kind of inference var
-that is not part of the type or const inference variables, similar to how we have
-special inference variables for type variables that we know to be an integer, but not
-yet which one. These separate inference variables fall back to `true` at
-the end of typeck (in `fallback_effects`) to ensure that `let _ = some_fn_item_name;`
-will keep compiling.
-
-All actually used (in function calls, casts, or anywhere else) function items, will
-have the `enforce_context_effects` method invoked.
-It trivially returns if the function being called has no `host` generic parameter.
-
-In order to error if a non-const function is called in a const context, we have not
-yet disabled the const-check logic that happens on MIR, because
-`enforce_context_effects` does not yet perform this check.
-
-The function call's `host` parameter is then equated to the context's `host` value,
-which almost always trivially succeeds, as it was an inference var. If the inference
-var has already been bound (since the function item is invoked twice), the second
-invocation checks it against the first.
+# Effects and const condition checking
+
+## The `HostEffect` predicate
+
+[`HostEffectPredicate`]s are a kind of predicate from `~const Tr` or `const Tr`
+bounds. It has a trait reference, and a `constness` which could be `Maybe` or
+`Const` depending on the bound. Because `~const Tr`, or rather `Maybe` bounds
+apply differently based on whichever contexts they are in, they have different
+behavior than normal bounds. Where normal trait bounds on a function such as
+`T: Tr` are collected within the [`predicates_of`] query to be proven when a
+function is called and to be assumed within the function, bounds such as
+`T: ~const Tr` will behave as a normal trait bound and add `T: Tr` to the result
+from `predicates_of`, but also adds a `HostEffectPredicate` to the
+[`const_conditions`] query.
+
+On the other hand, `T: const Tr` bounds do not change meaning across contexts,
+therefore they will result in `HostEffect(T: Tr, const)` being added to
+`predicates_of`, and not `const_conditions`.
+
+[`HostEffectPredicate`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_type_ir/predicate/struct.HostEffectPredicate.html
+[`predicates_of`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/ty/struct.TyCtxt.html#method.predicates_of
+[`const_conditions`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/ty/struct.TyCtxt.html#method.const_conditions
+
+## The `const_conditions` query
+
+`predicates_of` represents a set of predicates that need to be proven to use an
+item. For example, to use `foo` in the example below:
+
+```rust
+fn foo<T>() where T: Default {}
+```
+
+We must be able to prove that `T` implements `Default`. In a similar vein,
+`const_conditions` represents a set of predicates that need to be proven to use
+an item *in const contexts*. If we adjust the example above to use `const` trait
+bounds:
+
+```rust
+const fn foo<T>() where T: ~const Default {}
+```
+
+Then `foo` would get a `HostEffect(T: Default, maybe)` in the `const_conditions`
+query, suggesting that in order to call `foo` from const contexts, one must
+prove that `T` has a const implementation of `Default`.
+
+## Enforcement of `const_conditions`
+
+`const_conditions` are currently checked in various places. 
+
+Every call in HIR from a const context (which includes `const fn` and `const`
+items) will check that `const_conditions` of the function we are calling hold.
+This is done in [`FnCtxt::enforce_context_effects`]. Note that we don't check
+if the function is only referred to but not called, as the following code needs
+to compile:
+
+```rust
+const fn hi<T: ~const Default>() -> T {
+    T::default()
+}
+const X: fn() -> u32 = hi::<u32>;
+```
+
+For a trait `impl` to be well-formed, we must be able to prove the
+`const_conditions` of the trait from the `impl`'s environment. This is checked
+in [`wfcheck::check_impl`].
+
+Here's an example:
+
+```rust
+#[const_trait]
+trait Bar {}
+#[const_trait]
+trait Foo: ~const Bar {}
+// `const_conditions` contains `HostEffect(Self: Bar, maybe)`
+
+impl const Bar for () {}
+impl const Foo for () {}
+// ^ here we check `const_conditions` for the impl to be well-formed
+```
+
+Methods of trait impls must not have stricter bounds than the method of the
+trait that they are implementing. To check that the methods are compatible, a
+hybrid environment is constructed with the predicates of the `impl` plus the
+predicates of the trait method, and we attempt to prove the predicates of the
+impl method. We do the same for `const_conditions`:
+
+```rust
+#[const_trait]
+trait Foo {
+    fn hi<T: ~const Default>();
+}
+
+impl<T: ~const Clone> Foo for Vec<T> {
+    fn hi<T: ~const PartialEq>();
+    // ^ we can't prove `T: ~const PartialEq` given `T: ~const Clone` and
+    // `T: ~const Default`, therefore we know that the method on the impl
+    // is stricter than the method on the trait.
+}
+```
+
+These checks are done in [`compare_method_predicate_entailment`]. A similar
+function that does the same check for associated types is called
+[`compare_type_predicate_entailment`]. Both of these need to consider
+`const_conditions` when in const contexts.
+
+In MIR, as part of const checking, `const_conditions` of items that are called
+are revalidated again in [`Checker::revalidate_conditional_constness`].
+
+[`compare_method_predicate_entailment`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_hir_analysis/check/compare_impl_item/fn.compare_method_predicate_entailment.html
+[`compare_type_predicate_entailment`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_hir_analysis/check/compare_impl_item/fn.compare_type_predicate_entailment.html
+[`FnCtxt::enforce_context_effects`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_hir_typeck/fn_ctxt/struct.FnCtxt.html#method.enforce_context_effects
+[`wfcheck::check_impl`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_hir_analysis/check/wfcheck/fn.check_impl.html
+[`Checker::revalidate_conditional_constness`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_const_eval/check_consts/check/struct.Checker.html#method.revalidate_conditional_constness
+
+## Proving `HostEffectPredicate`s
+
+`HostEffectPredicate`s are implemented both in the [old solver] and the [new
+trait solver]. In general, we can prove a `HostEffect` predicate when either of
+these conditions are met:
+
+* The predicate can be assumed from caller bounds;
+* The type has a `const` `impl` for the trait, *and* that const conditions on
+the impl holds; or
+* The type has a built-in implementation for the trait in const contexts. For
+example, `Fn` may be implemented by function items if their const conditions
+are satisfied, or `Destruct` is implemented in const contexts if the type can
+be dropped at compile time.
+
+[old solver]: https://doc.rust-lang.org/nightly/nightly-rustc/src/rustc_trait_selection/traits/effects.rs.html
+[new trait solver]: https://doc.rust-lang.org/nightly/nightly-rustc/src/rustc_next_trait_solver/solve/effect_goals.rs.html