Treat missing trait declaration as not builtin in trait_impl_is_builtin

[SAY-5]

trait_impl_is_builtin looks up the impl's trait declaration in trans_trait_decls with a bare Map.find. When a trait decl was dropped earlier but its impl is still exported (e.g. the mutually-recursive serde Serialize/Serializer cluster), the lookup raises an uncaught Not_found and aeneas exits after writing partial output. This switches to find_opt and treats an absent declaration as not builtin, as suggested in #1102.

Closes #1102.

[oliver-butterley]

Closes #1102.

Note: this PR doesn't close the linked issue. If the PR version of Aeneas is given one example from the issue:

#[derive(serde::Serialize)]
pub struct Point {
    pub x: u32,
    pub y: u32,
}

Aeneas still generates three warnings and an error. The Lean output is only partial. The root cause behind the behaviour seen in the issue is that Aeneas doesn't yet support recursive traits.

What this PR does: This PR modifies the behaviour of one of the lookups in trait_impl_is_builtin. Previously if the impl's trait declaration wasn't found Aeneas would return a Not_found error. This PR makes it return false (meaning not builtin) in this case instead of throwing an error.

I would say the original behaviour was the correct one in this case, modified as per this PR would means that problems are silenced rather than communicated. Moreover the PR doesn't solve the underlying issue.

I suspect extending Aeneas to support recursive traits is complex and will need to be done in-house since it will touch on lots of deep parts of the code base.

[SAY-5]

That's fair, the loud failure does communicate the missing recursive-trait support better than a silent false. I'll leave it to you whether to keep this as-is, swap it for a clearer diagnostic instead of Not_found, or close in favour of the #176 work.

[oliver-butterley]

That's fair, the loud failure does communicate the missing recursive-trait support better than a silent false. I'll leave it to you whether to keep this as-is, swap it for a clearer diagnostic instead of Not_found, or close in favour of the #176 work.

Thanks for your efforts with this PR! I'm trying to figure out what is best to do since there are multiple issues behind the scenes with #1102. A somewhat convoluted investigation!

Do you have a particular minimal example in mind with this PR work? I've been using the following:

pub trait Gat {
    type Assoc<'a>;
}

pub struct S;

impl Gat for S {
    type Assoc<'a> = &'a u32;
}

pub fn use_it(_s: &S) -> u32 {
    0
}

This has the behaviour described in title of #1102, namely an uncaught exception related to trait_impl_is_builtin. As such it seems a useful reference.

Using the version of Aeneas of this PR, this error is changed to a similar error but now at extract_trait_impl (Not_found from Map.Make.find). As such the PR has just moved the error to another location. I.e., #1137 changes the crash location but not the outcome.

Indeed it would be desirable to avoid Aeneas having a hard crash in these cases, prior to the root cause being supported.

Is it possible to do this for all the consumers that will be missing the relevant data? I.e., a modification like in this PR removes the hard error at trait_impl_is_builtin but then we get one at extract_trait_impl. Is it possible to gracefully raise errors at each affected step? Moreover, the errors shouldn't be silenced, instead there should be a [%craise] span msg to notify of the error.

Do you want to investigate if something complete is possible?

[SAY-5]

You're right that this PR only relocates the crash: trait_impl_is_builtin stops throwing, but extract_trait_impl then hits Not_found from Map.find on the same missing impl, so the outcome is unchanged for your GAT example.

The clean fix is to replace each raw lookup on that data with a [%craise] span diagnostic rather than an uncaught OCaml exception, so every consumer reports a proper span-annotated error instead of crashing. The consumers I can see reaching the missing trait-impl are the trait_impl_is_builtin path and the extract_trait_impl/Map.find path; there may be a few more on the translation side that resolve trait impls by id.

I'll map the full set of call sites that look up trait-impl data by id and see whether they can all be routed through [%craise] span msg with a shared message, so the failure is surfaced (not silenced) consistently until recursive/GAT trait support lands. I'll follow up here with what I find rather than pushing a partial change.

[oliver-butterley]

You're right that this PR only relocates the crash: trait_impl_is_builtin stops throwing, but extract_trait_impl then hits Not_found from Map.find on the same missing impl, so the outcome is unchanged for your GAT example.

The clean fix is to replace each raw lookup on that data with a [%craise] span diagnostic rather than an uncaught OCaml exception, so every consumer reports a proper span-annotated error instead of crashing. The consumers I can see reaching the missing trait-impl are the trait_impl_is_builtin path and the extract_trait_impl/Map.find path; there may be a few more on the translation side that resolve trait impls by id.

I'll map the full set of call sites that look up trait-impl data by id and see whether they can all be routed through [%craise] span msg with a shared message, so the failure is surfaced (not silenced) consistently until recursive/GAT trait support lands.

If that works out, that would be great! It will be very useful to users who encounter such problems in the future so they know exactly what the problem is and can use a workaround until the full fix for the translation is available.

The example can be included in the tests folder of the repo using the known-failure magic comment (as per some other tests which are also known-failure).

[SAY-5]

Sounds good, and thanks for mapping the call sites. Routing every trait-impl-by-id lookup through [%craise] span msg with a shared message is the right shape here, since it turns the Not_found from Map.find into a proper span-annotated diagnostic while recursive/GAT support is still missing. I'd rather not guess at the full set of consumers on the translation side and half-convert them, so I'll defer to your mapping for which sites need it. Happy to fold the GAT example in as a known-failure test once the diagnostic path is settled so the expected message is stable.