Consider emitting unreachable!() for absurd cases

[workingjubilee]

In https://arxiv.org/pdf/2108.02995.pdf section 5.5 you say:

Handling absurd cases.

We follow the general strategy outlined in Section 5.1.3. The natural choice for implementing the elimination principle for an empty type is to use Rust’s panic! macro. In this case the elimination principle for False extracts to the following Rust code.

fn False_rect<P: Copy>(&’a self, u: ( ) ) -> P {
    panic!("Absurd case!")
}

We identify pattern-matchings with no branches at the pretty-printing stage and insert the
panic! macro

Have you considered simply reducing this to just emitting unreachable!(), which, as it diverges, will trivially unify with the other arms of a match expression where relevant? Using the stdlib macro will allow it to pick up any code-size improvements in this specific panic we manage to garner.

[spitters]

I don't think we have. Thanks for the suggestion!

…

On Tue, Mar 19, 2024 at 6:33 PM Jubilee ***@***.***> wrote: In https://arxiv.org/pdf/2108.02995.pdf section 5.5 you say: Handling absurd cases. We follow the general strategy outlined in Section 5.1.3. The natural choice for implementing the elimination principle for an empty type is to use Rust’s panic! macro. In this case the elimination principle for False extracts to the following Rust code. fn False_rect<P: Copy>(&’a self, u: ( ) ) → P { panic!("Absurd case!")} We identify pattern-matchings with no branches at the pretty-printing stage and insert the panic! macro Have you considered simply reducing this to just emitting unreachable!(), which, as it diverges, will trivially unify with the other arms of a match expression where relevant? — Reply to this email directly, view it on GitHub <#19>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AABTNTXYGQNWSXK4QT66VPLYZBZHTAVCNFSM6AAAAABE6AVENWVHI2DSMVQWIX3LMV43ASLTON2WKOZSGE4TKNJXGQZTAOA> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>