Engine crashes on refinement types with wildcard as binder

[W95Psp]

#[hax_lib::refinement_type(|_| true)]
pub struct Empty(usize);

The engine assumes |_| true is a function of arity one with a var pattern, not with a wildcard pattern.

cargo hax into fstar crashes with:

   Compiling literals v0.1.0 (/home/lucas/repos/hax/main/tests/literals)
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.21s
Fatal error: exception "Option.value_exn None"
Raised at Base__Error.raise in file "src/error.ml" (inlined), line 9, characters 14-30
Called from Base__Option.value_exn in file "src/option.ml", line 114, characters 4-21
Called from Fstar_backend.Make.pitem_unwrapped in file "backends/fstar/fstar_backend.ml", line 976, characters 16-67
Called from Fstar_backend.Make.pitem in file "backends/fstar/fstar_backend.ml", line 877, characters 12-29
Called from Fstar_backend.strings_of_item in file "backends/fstar/fstar_backend.ml", line 1453, characters 2-18
Called from Base__List.concat_map.aux in file "src/list.ml", line 726, characters 34-40
Called from Fstar_backend.string_of_items in file "backends/fstar/fstar_backend.ml", line 1514, characters 4-73
Called from Fstar_backend.translate.(fun) in file "backends/fstar/fstar_backend.ml", line 1572, characters 11-63
Called from Base__List.concat_map.aux in file "src/list.ml", line 726, characters 34-40
Called from Hax_engine__Diagnostics.Core.try_ in file "lib/diagnostics.ml", line 128, characters 26-32
Called from Lib.run in file "bin/lib.ml", line 115, characters 4-348
Called from Lib.main in file "bin/lib.ml", line 136, characters 11-24
Re-raised at Lib.main in file "bin/lib.ml", line 163, characters 6-42
Called from Dune__exe__Native_driver in file "bin/native_driver.ml", line 23, characters 2-13
error: hax: hax-engine exited with non-zero code 2

Open this code snippet in the playground

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[W95Psp]

Still relevant, but that's a very small issue, it's trivial to fix

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[W95Psp]

Very easy to fix, let's plan to do this soon

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[clementblaudeau]

We should have a proper error message or a fix.