Ability to solve implicit sizes in bitvector concatenation

[Timmmm]

It would be neat if this worked:

let x : bits(5) = 0b1 @ zeros();

Unfortunately it doesn't currently:

14 |  let x : bits(5) = 0b1 @ zeros();
   |                    ^-----------^ checking function argument has type bitvector('m)
   | Cannot solve implicit 'n in zeros()

Obviously there will be situations where it is impossible:

let x : bits(5) = ones() @ zeros();

But as long as there is at most 1 implicit length in the concatenation it should be possible in theory I guess?

Workaround is to put it in a function and make it explicit within the function, but it's not as nice.

val leading_one : forall 'n, 'n >= 1. (implicit('n)) -> bits('n)
function leading_one(n) = 0b1 @ zeros('n - 1)

function main() -> unit = {
  let x : bits(5) = leading_one();
}

[Alasdair]

Would make sense to have this because it works for vector concatenation patterns, however concatenation expressions are type checked as regular functions. That has its advantages, but also means special casing things might be tricky.

[Alasdair]

Should be fixed by https://github.com/rems-project/sail/pull/753