unison/unison-src/transcripts/fix2474.md
Greg Pfeil b657d0dd50
Fix a few transcripts with incorrect Markdown
These weren’t errors in any way, but the `cmark`-produced outputs made
it clear that some of our transcripts weren’t formatted the way we
intended.
2024-07-10 13:56:10 -06:00

1.0 KiB

Tests an issue with a lack of generality of handlers.

In general, a set of cases:

{ e ... -> k }

should be typed in the following way:

  1. The scrutinee has type Request {E, g} r -> s where E is all the abilities being handled. g is a slack variable, because all abilities that are used in the handled expression pass through the handler. Previously this was being inferred as merely Request {E} r -> s
  2. The continuation variable k should have type o ->{E, g} r, matching the above types (o is the result type of e). Previously this was being checked as o ->{E0} r, where E0 is the ability that contains e.
scratch/main> builtins.merge
structural ability Stream a where
  emit : a -> ()

Stream.uncons : '{Stream a, g} r ->{g} Either r (a, '{Stream a, g} r)
Stream.uncons s =
  go : Request {Stream a,g} r -> Either r (a, '{Stream a,g} r)
  go = cases
    { r } -> Left r
    { Stream.emit a -> tl } -> Right (a, tl : '{Stream a,g} r)
  handle !s with go