mirror of
https://github.com/unisonweb/unison.git
synced 2024-09-11 10:35:57 +03:00
55 lines
1.4 KiB
Markdown
55 lines
1.4 KiB
Markdown
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`.
|
|
|
|
``` ucm
|
|
scratch/main> builtins.merge
|
|
|
|
Done.
|
|
|
|
```
|
|
``` unison
|
|
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
|
|
```
|
|
|
|
``` ucm
|
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
I found and typechecked these definitions in scratch.u. If you
|
|
do an `add` or `update`, here's how your codebase would
|
|
change:
|
|
|
|
⍟ These new definitions are ok to `add`:
|
|
|
|
structural ability Stream a
|
|
Stream.uncons : '{g, Stream a} r
|
|
->{g} Either r (a, '{g, Stream a} r)
|
|
|
|
```
|