index out of bounds calling > toWeighted nat

[jastice]

Create scratch file containing only this:

> toWeighted nat

It crashes ucm:

.>

  ✅

  ~/playspace/udah/scratch.u changed.

  Now evaluating any watch expressions (lines starting with `>`)... Ctrl+C cancels.
ucm: ./Data/Vector/Generic/Mutable.hs:691 (read): index out of bounds (-1,0)
CallStack (from HasCallStack):
  error, called at ./Data/Vector/Internal/Check.hs:87:5 in vector-0.12.0.1-GGZqQZyzchy8YFPCF67wxL:Data.Vector.Internal.Check

[pchiusano]

Adding a bit more color here, based on #1489 it really looks like this is an issue when the current runtime attempts to decompile functions.

[pchiusano]

Also possibly same issue:

Stream.tail : '{Stream a} () -> Optional ('{Stream a} ())
Stream.tail stream =
  h = cases
    {Stream.emit e -> resume} ->
      Some resume
    {u} -> None
  handle !stream with h

> Stream.tail '(Stream.range 0 5)

ucm: ./Data/Vector/Generic/Mutable.hs:691 (read): index out of bounds (-1,0)
CallStack (from HasCallStack):
  error, called at ./Data/Vector/Internal/Check.hs:87:5 in vector-0.12.0.3-LfvlcMFJAcY18uD1Y2O5Ig:Data.Vector.Internal.Check

Changing the watch expression to this works fine:

> Optional.map Stream.toList <| Stream.tail '(Stream.range 0 5)

This demonstrates that the problem is in decompiling the function inside the Some to print it back to the user. In the new runtime, we get the message "decompiling a captured continuation" but no crash.

I'd like to just have decompilation always work, even if it's a continuation and we have to make up crappy synthetic variable names.