`let else` patterns with panic do not lax-check in F*

[clementblaudeau]

As shown in this playground, hax gets confused by patterns of the form let ... = ... else { panic!(" ... ") ; }, where the else branch gets typed as unit while the first branch might be anything:

* Error 189 at Playground.fst(27,4-27,6):
  - Expected expression of type Rust_primitives.Integers.i32
    got expression ()
    of type Prims.unit

The problem is two fold:

1. When removing the semi-colon ";" after the panic!, the error message reveals that there is a missing cast from Hax.t_Never to any type :

* Error 12 at Playground.fst(14,4-23,29):
  - Expected type Rust_primitives.Integers.i32
    but
        Core.Panicking.panic_fmt (Core.Fmt.impl_4__new_const (Rust_primitives.Integers.mk_usize
                  1)
              (Rust_primitives.Hax.array_of_list 1 ["Some string"]))
    has type Rust_primitives.Hax.t_Never

2. Sequences e1; e2 that contain a Hax.t_Never should also get typed as Hax.t_Never rather than has the type of e2

[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

[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]

Will be fixed when porting the importer to Rust (#1524)