mirror of
https://github.com/unisonweb/unison.git
synced 2024-09-11 02:25:39 +03:00
Add some tests
This commit is contained in:
parent
80b3a64eee
commit
627669dbec
26
unison-src/transcripts/fix2350.md
Normal file
26
unison-src/transcripts/fix2350.md
Normal file
@ -0,0 +1,26 @@
|
|||||||
|
|
||||||
|
This tests an issue where ability variables were being defaulted over
|
||||||
|
eagerly. In general, we want to avoid collecting up variables from the
|
||||||
|
use of definitions with types like:
|
||||||
|
|
||||||
|
T ->{e} U
|
||||||
|
|
||||||
|
Since this type works for every `e`, it is, 'pure;' and we might as
|
||||||
|
well have `e = {}`, since `{}` is a subrow of every other row.
|
||||||
|
However, if `e` isn't just a quantified variable, but one involved in
|
||||||
|
ongoing inference, it's undesirable to default it. Previously there
|
||||||
|
was a check to see if `e` occurred in the context. However, the wanted
|
||||||
|
abilities being collected aren't in the context, so types like:
|
||||||
|
|
||||||
|
T ->{S e} U ->{e} V
|
||||||
|
|
||||||
|
were a corner case. We would add `S e` to the wanted abilities, then
|
||||||
|
not realize that `e` shouldn't be defaulted.
|
||||||
|
|
||||||
|
```unison
|
||||||
|
unique ability Storage d g where
|
||||||
|
save.impl : a ->{Storage d g} ('{g} (d a))
|
||||||
|
|
||||||
|
save : a ->{Storage d g, g} (d a)
|
||||||
|
save a = !(save.impl a)
|
||||||
|
```
|
39
unison-src/transcripts/fix2350.output.md
Normal file
39
unison-src/transcripts/fix2350.output.md
Normal file
@ -0,0 +1,39 @@
|
|||||||
|
|
||||||
|
This tests an issue where ability variables were being defaulted over
|
||||||
|
eagerly. In general, we want to avoid collecting up variables from the
|
||||||
|
use of definitions with types like:
|
||||||
|
|
||||||
|
T ->{e} U
|
||||||
|
|
||||||
|
Since this type works for every `e`, it is, 'pure;' and we might as
|
||||||
|
well have `e = {}`, since `{}` is a subrow of every other row.
|
||||||
|
However, if `e` isn't just a quantified variable, but one involved in
|
||||||
|
ongoing inference, it's undesirable to default it. Previously there
|
||||||
|
was a check to see if `e` occurred in the context. However, the wanted
|
||||||
|
abilities being collected aren't in the context, so types like:
|
||||||
|
|
||||||
|
T ->{S e} U ->{e} V
|
||||||
|
|
||||||
|
were a corner case. We would add `S e` to the wanted abilities, then
|
||||||
|
not realize that `e` shouldn't be defaulted.
|
||||||
|
|
||||||
|
```unison
|
||||||
|
unique ability Storage d g where
|
||||||
|
save.impl : a ->{Storage d g} ('{g} (d a))
|
||||||
|
|
||||||
|
save : a ->{Storage d g, g} (d a)
|
||||||
|
save a = !(save.impl a)
|
||||||
|
```
|
||||||
|
|
||||||
|
```ucm
|
||||||
|
|
||||||
|
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`:
|
||||||
|
|
||||||
|
unique ability Storage d g
|
||||||
|
save : a ->{g, Storage d g} d a
|
||||||
|
|
||||||
|
```
|
35
unison-src/transcripts/fix2474.md
Normal file
35
unison-src/transcripts/fix2474.md
Normal file
@ -0,0 +1,35 @@
|
|||||||
|
|
||||||
|
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
|
||||||
|
.> builtins.mergeio
|
||||||
|
```
|
||||||
|
|
||||||
|
```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
|
||||||
|
```
|
51
unison-src/transcripts/fix2474.output.md
Normal file
51
unison-src/transcripts/fix2474.output.md
Normal file
@ -0,0 +1,51 @@
|
|||||||
|
|
||||||
|
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
|
||||||
|
.> builtins.mergeio
|
||||||
|
|
||||||
|
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
|
||||||
|
|
||||||
|
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)
|
||||||
|
|
||||||
|
```
|
Loading…
Reference in New Issue
Block a user