Internal error: Unreachable code (at "pretty_print_coq.ml" line 1070):

[nblei]

I was playing with the sail cli and ran

$ sail -coq cheri128_hsb.sail

which produced the following output:

Internal error: Unreachable code (at "pretty_print_coq.ml" line 1070):

34	val HighestSetBit : forall 'N , 'N >= 2. bits('N) -> {'n, 0 <= 'n < 'N . (bool, atom('n))}	^--------------^	inconsistent type int('n) and pattern msb as 'msb
Raised by primitive operation at file "reporting.ml", line 164, characters 18-43
Called from file "pretty_print_coq.ml", line 1070, characters 29-143
Called from file "list.ml", line 92, characters 20-23
Called from file "pretty_print_coq.ml", line 1073, characters 22-53
Called from file "pretty_print_coq.ml", line 1094, characters 28-67
Called from file "pretty_print_coq.ml", line 2235, characters 63-102
Called from file "pretty_print_coq.ml", line 2643, characters 16-38
Called from file "pretty_print_coq.ml", line 2980, characters 15-36
Called from file "pretty_print_coq.ml", line 3021, characters 13-40
Called from file "pretty_print_coq.ml", line 3030, characters 27-54
Please report this as an issue on GitHub at https://github.com/rems-project/sail/issues

[bacam]

Thanks for reporting this. The immediate problem is pretty easy to fix (as is the fact that it reports it at the wrong location), but the underlying support for these existentially quantified tuples isn't complete yet. Fortunately, as far as I know they aren't used in actual models at the moment, so unless you've also encountered this elsewhere I'll leave the issue open for now to return to later.