unison/unison-src/transcripts/fix2474.md

35 lines
1.0 KiB
Markdown
Raw Permalink Normal View History

2021-10-29 00:45:51 +03:00
Tests an issue with a lack of generality of handlers.
In general, a set of cases:
{ e ... -> k }
2021-10-29 00:45:51 +03:00
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`.
```ucm
scratch/main> builtins.merge
2021-10-29 00:45:51 +03:00
```
```unison
2024-04-15 02:57:08 +03:00
structural ability Stream a where
2021-10-29 00:45:51 +03:00
emit : a -> ()
Stream.uncons : '{Stream a, g} r ->{g} Either r (a, '{Stream a, g} r)
2024-04-15 02:57:08 +03:00
Stream.uncons s =
2021-10-29 00:45:51 +03:00
go : Request {Stream a,g} r -> Either r (a, '{Stream a,g} r)
2024-04-15 02:57:08 +03:00
go = cases
2021-10-29 00:45:51 +03:00
{ r } -> Left r
{ Stream.emit a -> tl } -> Right (a, tl : '{Stream a,g} r)
handle !s with go
```