dyn Foo is, as you said, a transient thing - it doesn't really exist by itself. It's a non-Sized value which stores part of itself in whatever its being stored behind.
In my mental model, I think of dyn Foo as the data half of the trait object + an obligation on whatever is storing it. The first part of dyn Foo is thing at the end of the *mut () in the code you posted. The second is an abstract concept of "whatever is storing me stores a vtable too".
Yes, it pattern matches first. However after that, I would change two things.
First, it won't match the dyn on both sides, because A isn't a type. It'll only do pattern matching up to types, so it will match the & on the left and the right, but then it ends up with dyn B on the left and dyn A on the right.
I say this because pattern matching the dyn away wouldn't really mean anything. A is a trait, not a type - dyn A has values, but A only has a set of types which implement it. When matching the left and right hand side, the compiler is thinking of types and values, and thus it'll only unwrap to dyn A (and dyn B). A and B only exists as types with the dyn.
Second, I would use a different word for the next part. After it finds dyn B on the left and something of type dyn A on the right, it checks whether dyn A can be coerced into dyn A.
I'm being a bit pedantic: in practice, checking for coercion into a dyn Trait does check whether the right hand side implements that trait. But it also checks other things to ensure the coercion can happen, such as the right-hand-side being Sized.
The other reason I'd say it checks for coercion is that there are other things, besides casting into a dyn Trait, which the coercion check enables. For instance, this piece of code works on the same basis:
let owned = String::from("hi");
let a: &String = &owned;
let b: &str = &a;
String doesn't somehow implements str, but rather that String can coerce into str, the same way i32 can coerce into dyn A. In this case, the coercion is done through deref coercions.
I think you're definitely on the right track! You've got the end result down, I think there are just a few things in the middle where the compiler works slightly differently from what you've said.