Meta.check does not check projections

[nomeata]

The Meta.check function is incomplete, in particular for projections:

private partial def checkAux (e : Expr) : MetaM Unit := do
  check e |>.run
where
  check (e : Expr) : MonadCacheT ExprStructEq Unit MetaM Unit :=
    checkCache { val := e : ExprStructEq } fun _ => do
      match e with
      | .forallE ..      => checkForall e
      | .lam ..          => checkLambdaLet e
      | .letE ..         => checkLambdaLet e
      | .const c lvls    => checkConstant c lvls
      | .app f a         => check f; check a; checkApp f a
      | .mdata _ e       => check e
      | .proj _ _ e      => check e  -- ←←←←←
      | _                => return ()

it should probably do similar checks as the kernel, or as inferType does.

Versions

"4.12.0-nightly-2024-10-09"

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.