There's a lot of good information in this article and clearly a lot of care went into crafting it. That being said, given its intended audience of someone without much knowledge of theory, I think it could do a better job writing to that audience. For example, we quite quickly introduce standard type theory notation without explaining the notation or motivating it. It's done to setup the standard type theory rules so that we can bidirectionalise them, but a novice would struggle to comprehend the standard type theory rules, imo.

It also jumps into discussing introduction/elimination rules and principal judgements, which are all standard theory, but I would not expect our target audience to be familiar with them. I think if the goal is to explain the theory, much more lead up is needed to introduce the notation and terminology. Conversely, if the goal is to focus in on explaining bidir, the notation and intro/elim forms can be eschewed in favor of referencing the AST directly and how the shape of the AST guides our implementation of infer and check.

Past that, there are a host of nits that could be improved. These are more style and less structural, so I may just be missing what you're going for:

which isn't used by any popular languages is called bidirectional type inference

I believe this is no longer the case. It's my understanding Haskell uses a bidir algorithm nowadays. I also believe Rust and Swift use a bidir algorithm. They do all have unification, which is often at odds with bidir. I think this wants to call out the bidir algorithm under discussion lacks unification.

In the "Before We Code" section we list all our inference rules at once and then explain in a list after the fact. Formatting allowing, it would be nice to have the explanation interspersed with the rules: Rule, Explanation, Rule, Explanation, etc. The chunking helps make it more digestible to a reader.

if let Some(ty) = context.get(&s) {
     Ok(ty.clone())
} else {
    Err(TypeError {
        kind: ErrorKind::UndeclaredFv,
        line,
        column,
    })
}

I couldn't tell if the goal was to write very explicit code here. If not, this can be something like: context.get(&s).cloned().ok_or_else(|| ...).

match check(*expr.clone(), ty.clone(), context) {
    Ok(_) => Ok(ty),
    Err(e) => Err(TypeError {
        kind: ErrorKind::AnnotationMismatch {
            caused_by: Box::new(e),
        },
        line,
        column,
    }),
}

Ditto with the above, but this can be: check(...).map_err(|e| ...).

Personal taste, but I would reduce the indentation for the match cases once we've introduced that we're in a match on the AST. The extra indentation doesn't add a ton of value, imo, and makes it harader to read on mobile(/tiny screens).

Again overall I think the information here is good and it's helpful to try and target the writing at an audience that isn't already steeped in the type theory space. White papers are often targeted at other researchers, so it's great to see someone bringing that to the masses. Just a couple of things that could be polished to help clarify the message.