simplify HR processing and link to detailed blog post

Author: lqd

posts/inside-rust/2023-09-25-polonius-update.md

@@ -77,7 +77,7 @@ Here are the roadmap's milestones:
 
 ### 1. Factoring out higher-ranked concerns from the main path
 
-Today, the trait solver produces higher-ranked outlives constraints and the borrow checker solves them. In the future, we would like to make the [next trait solver](https://github.com/rust-lang/trait-system-refactor-initiative/) responsible for solving these higher-ranked constraints itself, so that it only produces constraints on regions in the root [universe](https://rustc-dev-guide.rust-lang.org/borrow_check/region_inference/placeholders_and_universes.html#what-is-a-universe) (which the borrow checker can easily process). This would allow us to solve implication predicates like `for<T> { if (T: 'a, 'a: 'b) { T: 'b } }` without having to effectively reproduce the same trait solving logic again.
+Today, the trait solver produces higher-ranked outlives constraints and the borrow checker solves them. In the future, we would like to make the [next trait solver](https://github.com/rust-lang/trait-system-refactor-initiative/) responsible for solving these higher-ranked constraints itself, so that it only produces the simpler `subset` constraint used in Polonius. This would allow us to solve implication predicates like `for<T> { if (T: 'a, 'a: 'b) { T: 'b } }` without having to effectively reproduce the same trait solving logic again. [This blog post](https://smallcultfollowing.com/babysteps/blog/2019/01/21/hereditary-harrop-region-constraints/) describes the problem and possible solution in more detail.
 
 In the shorter term, we are exploring refactoring the borrow checker to separate out the higher-ranked processing from the ordinary processing. The goal would be to preprocess the outlives constraints in a kind of Polonius ["leak check"](https://rustc-dev-guide.rust-lang.org/traits/hrtb.html#basic-matching-and-placeholder-leaks), where we can compute the higher-ranked errors. This could then be removed once the trait solver can solve these constraints.