Lean: Types with numeric quantifiers produce unknown identifiers

[protoben]

The following Lean tests are currently failing because of unknown identifiers in numerically quantified Sail types:

• config_vec_list
• type_if_bits

For example, in config_vec_list, let xs : {'n, 'n >= 2. vector('n, string)} = config foo.bar; results in let xs : (Vector String k_n) := #v["D", "C", "B", "A"], with the error

✖ [7/12] Building Out
trace: .> LEAN_PATH=././.lake/build/lib DYLD_LIBRARY_PATH= /Users/hamlinb/.elan/toolchains/leanprover--lean4-nightly---nightly-2025-02-05/bin/lean --tstack=400000 ././././Out.lean -R ./././. -o ././.lake/build/lib/Out.olean -i ././.lake/build/lib/Out.ilean -c ././.lake/build/ir/Out.c --json
error: ././././Out.lean:99:26: unknown identifier 'k_n'
error: Lean exited with code 1

[bacam]

The good news is that current models don't use existential types like this, and it's not currently supported by the Rocq backend either. However, it's pretty close to the top of my list of things that might end up in the RISC-V model (particularly because of the configuration example), so I've been looking at it a little.

In some examples, like the configuration one, it's enough in Rocq to replace the bound type variable with an underscore to get the prover to fill it in. Other tests, such as test/typecheck/pass/ex_cons_infer.sail, need a dependent pair to capture the size.

[bacam]

One awkward point I noticed in the type_if_bits test is that the typechecker's normalisation of function type signatures replaces the some_bits existential type with a universal quantification in if_bits_test. That is,

type some_bits = {'n, 'n in {16, 32, 64}. bits('n)}
...
val if_bits_test : some_bits -> bool

becomes

type some_bits = {'n, 'n in {16, 32, 64}. bits('n)}
...
val if_bits_test : forall 'n, 'n in {16, 32, 64}. bits('n) -> bool

So a dependent pair isn't needed there.

[javra]

The reason this fails is more or less just because Lean currently supports auto-implicits in top-level definitions but not in let-bindings. That seems a bit inconsistent to me, but it should be easy to work around.

[javra]

In some examples, like the configuration one, it's enough in Rocq to replace the bound type variable with an underscore to get the prover to fill it in. Other tests, such as test/typecheck/pass/ex_cons_infer.sail, need a dependent pair to capture the size.

Couldn't we also use an implicit argument? I.e. translate

type some_bits = {'n, 'n in {16, 32, 64}. bits('n)}

from type_if_bits.sail to

abbrev some_bits {k_n} := (BitVec k_n)

EDIT: Ah, no that really doesn't work int he ex_cons_infer case

[bacam]

It would probably work in simple cases, like the underscore trick (which I added for Rocq in 2ee7b9b). In general using a dependent pair seems unavoidable; for example, I was playing with

default Order dec
$include <prelude.sail>

register r : bool

function main() -> unit = {
  let x : {'n, 'n in {32,64}. bits('n)} = if r then 0x76543210 else 0xedcba98765434210;
  print_bits("x = ", x);
  print_int("unsigned(x) = ", unsigned(x));
  print_bits("sext(x) = ", sail_sign_extend(x, 64));
}

where you really need to say which case you're in.

As I said before, though, none of the current models do anything like this, and the case I'm most concerned about is the config example, where simple tricks do work.