Function infer_app_mismatch_errors

crates/kernel/src/infer.rs:834–846

()

  #[test]
  fn infer_binder_errors_restore_lctx_scope() {
    let bad_body = AE::cnst(mk_id("MissingBinderBody"), Box::new([]));
    let cases = [
      ("lambda", AE::lam((), (), sort0(), bad_body.clone())),
      ("forall", AE::all((), (), sort0(), bad_body.clone())),
      ("let", AE::let_((), sort1(), sort0(), bad_body, false)),
    ];

    for (kind, expr) in cases {
      let mut env = test_env();
      let mut tc = TypeChecker::new(&mut env);
      let outer_id = tc.fresh_fvar_id();
      tc.lctx
        .push(outer_id, LocalDecl::CDecl { name: (), bi: (), ty: sort0() });
      let saved = tc.lctx.len();