Fixes #1440 
Fixes #1104 

It turns out we can relatively easily handle these cases by looking for
`BOTTOM` in the `NullnessStore` before the return expression (which
means the path is infeasible). I do wonder if there are other places in
our analyses we should be checking for `BOTTOM`, but we want to be
careful since some users may expect issues to be reported in unreachable
code. But for contract verification, it seems essential.

<!-- This is an auto-generated comment: release notes by coderabbit.ai
-->
## Summary by CodeRabbit

* **New Features**
* Enhanced contract-driven nullness analysis to inspect all nested
return expressions and detect unreachable return paths via contract
dataflow.
* Added an API to identify unreachable/definitively-null access paths
for contract checks.
  * Improved construction of contract-violation messages.

* **Bug Fixes**
* Reduces spurious contract violation reports (including void-like
returns and unreachable branches).

* **Tests**
* Added tests covering propagation, multi-level contracts, ternaries,
void returns, and nested lambdas/anonymous classes.

* **Chores**
* Replaced a runtime assertion with a clearer verification error for
unexpected AST kinds.

<sub>✏️ Tip: You can customize this high-level summary in your review
settings.</sub>
<!-- end of auto-generated comment: release notes by coderabbit.ai -->

)

Fixes #1444 

In certain cases, like the test from #1444 added here, `javac` adds a
`@Nullable` annotation to a type incorrectly as part of its inference.
Here, for a call from the test:

```java
@NullMarked
public class Test {
    static class DefaultConfiguration {
        final @nullable Stream<? extends String> children;
    }
    final Stream<? extends String> children;
    Test(DefaultConfiguration configuration) {
        // relevant call
        this.children = notNull(configuration.children, "children must not be null");
    }
    public static <T> T notNull(@nullable T object, String message) {
        throw new RuntimeException("todo");
    }
}
```
`javac`s inferred type for the return of the `notNull` call matches the
inferred parameter type exactly, `@Nullable Stream<...>`. But, when
applying JSpecify rules, the return cannot be `@Nullable`. To fix this,
add inferred `@NonNull` qualifiers along with `@Nullable` when doing a
substitution inside a type.

<!-- This is an auto-generated comment: release notes by coderabbit.ai
-->
## Summary by CodeRabbit

* **Bug Fixes**
* Simplified printing of error/unknown generic types to show only the
simple type name.
* Improved type-variable substitution so inferred nullability is applied
for both nullable and non-null cases.

* **Tests**
* Added/updated tests covering generic method type inference and
JSpecify/Nullability behaviors (includes a new scenario for issue1444).

<sub>✏️ Tip: You can customize this high-level summary in your review
settings.</sub>
<!-- end of auto-generated comment: release notes by coderabbit.ai -->

…1447)

Also update `AGENTS.md` to help coding agents auto-format release note
bullets properly.