Unprintable types cause type-checking problems during rewrites

[bacam]

In riscv/sail-riscv#861 the Rocq output was broken because Sail's type checker was unable to handle the result of a rewrite without more type annotations. In

  let ('n, bytes) = split_misaligned(vaddr, width);
  var data = zeros(8 * n * bytes);

  let (first, last, step) = misaligned_order(n);
  var i : range(0, 'n - 1) = first;
  var finished : bool = false;

  let vaddr = bits_of(vaddr);
  repeat {
    let offset = i;
...

the type of data can't be used to make new type annotations by rewrites, in particular the rewrite to remove assignments which let-binds data later on. The repeat loop assigns to data, and the type checker won't infer the let binding that results, giving a type error.

In this case it's possible to resolve the problem by binding a type variable for bytes, but it isn't clear what to do in general.