We mostly keep things the same here, but the message has been moved from the annotation to the diagnostic's top-line message. I think this is perhaps a little worse, but some bigger improvements could be made here. Indeed, we could perhaps even add a "fix" here.
Markdown files within the mdtest/ subdirectory are tests of type inference and type checking;
executed by the tests/mdtest.rs integration test.
See crates/red_knot_test/README.md for documentation of this test format.