I think that mostly works, but it's still possible that different tools assign different semantics for the same syntax, which could then interact in a weird way if the library author wrote the interface annotations with Tool A's semantics in mind, while you ended up checking them against your code with Tool B.

I think the type systems are simple enough that this is probably a theoretical concern, and won't come up often in practice.

I think so. When typing checking a project, its dependencies don't get type checked as well as far as I know. Type errors in dependencies are kind of not relevant for you, and many dependencies are not type-annotated anyway.

Well you probably do still want the type checker to at least look at the public interfaces of any libraries you depend on, since you want it to enforce that you're calling into them correctly.

Absolutely. It should probably not report errors that are not in your code, by default anyway, but still extract information about typing relevant to you as much as it can.