Should a checker reject a let type mismatch that disappears after substitution?

We are preparing shared regression tests for external Lean checkers and want
to clarify what a checker is expected to validate when it reads an exported
declaration.

Consider this existing serialized declaration, shown here in readable notation:

def EcosystemCase : Sort 2 := let u : Sort 1 := Sort 1; u

The let contains a type mismatch: its value, Sort 1, has type Sort 2, but
its annotation says Sort 1.

If we first substitute the value for u (zeta reduction), the expression becomes:

def EcosystemCase : Sort 2 := Sort 1

That resulting declaration has matching types. The simplification has removed
the incorrect annotation.

Should a full external checker reject the original declaration because of
that mismatch, or is it permitted to simplify the let first and accept the
result? If the interface assumes that incoming expressions have already been
type-checked, could that assumption be stated explicitly instead?

This matters for shared tests: we need to know whether acceptance promises that
the supplied expression was checked, or that a permitted transformation of it
was checked. We are asking about that guarantee, not reporting a false theorem
or asking every reducer to repeat checks on already-validated expressions.

We found separate checking and reduction paths in Lean v4.33.0:
infer_let
checks the annotation/value relationship in checking mode, while the
let reduction branch
substitutes directly. The
3.1.0 format description
lists the let fields but does not state which acceptance guarantee applies.
Is there an existing policy we should cite, or would a short clarification in
that document or the Lean reference manual be appropriate?

For reproducibility, the unchanged candidate NDJSON
and matching control
are each 601 bytes. The notation above explains those bytes; it is not an
elaboration result or a new test run. The body uses u, and the control changes
both the let value and the enclosing declaration type. The
source review
records the exact versions and remaining qualifications.

Read src/kernel/type_checker.cpp at infer_let and the let reduction branch, then review format_ndjson.md and the linked clarification packet. Compare the candidate and matching control only as described in the issue. Done means the acceptance guarantee is decided and stated in the appropriate format documentation or Lean reference material.