mirror of
https://github.com/unisonweb/unison.git
synced 2024-09-19 06:17:33 +03:00
Add tests
This commit is contained in:
parent
f5ce1c75d2
commit
99ff320820
25
unison-src/transcripts-using-base/fix2158-1.md
Normal file
25
unison-src/transcripts-using-base/fix2158-1.md
Normal file
@ -0,0 +1,25 @@
|
||||
This transcript tests an ability check failure regression.
|
||||
|
||||
```unison
|
||||
ability Async t g where
|
||||
fork : '{Async t g, g} a -> t a
|
||||
await : t a -> a
|
||||
|
||||
Async.parMap : (a ->{Async t g, g} b) -> [a] ->{Async t g} [b]
|
||||
Async.parMap f as =
|
||||
tasks = List.map (a -> fork '(f a)) as
|
||||
List.map await tasks
|
||||
```
|
||||
|
||||
The issue was that certain ability processing was happing in less
|
||||
optimal order. `g` appears both as an ability used and as a parameter
|
||||
to `Async`. However, the latter occurrence is more strict. Unifying
|
||||
the types `Async t g1` and `Async t g2` requires `g1` and `g2` to
|
||||
be equal, while abilities that occur directly in a row are subject to
|
||||
some subtyping.
|
||||
|
||||
However, the ability handling was just processing rows in whatever
|
||||
order they occurred, and during inference it happened that `g`
|
||||
occurred in the row before `Async t g`. Processing the stricter parts
|
||||
first is better, becauase it can solve things more precisely and avoid
|
||||
ambiguities relating to subtyping.
|
39
unison-src/transcripts-using-base/fix2158-1.output.md
Normal file
39
unison-src/transcripts-using-base/fix2158-1.output.md
Normal file
@ -0,0 +1,39 @@
|
||||
This transcript tests an ability check failure regression.
|
||||
|
||||
```unison
|
||||
ability Async t g where
|
||||
fork : '{Async t g, g} a -> t a
|
||||
await : t a -> a
|
||||
|
||||
Async.parMap : (a ->{Async t g, g} b) -> [a] ->{Async t g} [b]
|
||||
Async.parMap f as =
|
||||
tasks = List.map (a -> fork '(f a)) as
|
||||
List.map await tasks
|
||||
```
|
||||
|
||||
```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`:
|
||||
|
||||
ability Async t g
|
||||
Async.parMap : (a ->{g, Async t g} b)
|
||||
-> [a]
|
||||
->{Async t g} [b]
|
||||
|
||||
```
|
||||
The issue was that certain ability processing was happing in less
|
||||
optimal order. `g` appears both as an ability used and as a parameter
|
||||
to `Async`. However, the latter occurrence is more strict. Unifying
|
||||
the types `Async t g1` and `Async t g2` requires `g1` and `g2` to
|
||||
be equal, while abilities that occur directly in a row are subject to
|
||||
some subtyping.
|
||||
|
||||
However, the ability handling was just processing rows in whatever
|
||||
order they occurred, and during inference it happened that `g`
|
||||
occurred in the row before `Async t g. Processing the stricter parts
|
||||
first is better, becauase it can solve things more precisely and avoid
|
||||
ambiguities relating to subtyping.
|
28
unison-src/transcripts/fix2167.md
Normal file
28
unison-src/transcripts/fix2167.md
Normal file
@ -0,0 +1,28 @@
|
||||
```ucm:hide
|
||||
.> builtins.merge
|
||||
```
|
||||
|
||||
This is just a simple transcript to regression check an ability
|
||||
inference/checking issue.
|
||||
|
||||
```unison
|
||||
ability R t where
|
||||
die : () -> x
|
||||
near.impl : Nat -> Either () [Nat]
|
||||
|
||||
R.near n = match near.impl n with
|
||||
Left e -> die ()
|
||||
Right a -> a
|
||||
|
||||
R.near1 region loc = match R.near 42 with
|
||||
[loc] -> loc
|
||||
ls -> R.die ()
|
||||
```
|
||||
|
||||
The issue was that abilities with parameters like this were sometimes
|
||||
causing failures like this because the variable in the parameter would
|
||||
escape to a scope where it no longer made sense. Then solving would
|
||||
fail because the type was invalid.
|
||||
|
||||
The fix was to avoid dropping certain existential variables out of
|
||||
scope.
|
37
unison-src/transcripts/fix2167.output.md
Normal file
37
unison-src/transcripts/fix2167.output.md
Normal file
@ -0,0 +1,37 @@
|
||||
This is just a simple transcript to regression check an ability
|
||||
inference/checking issue.
|
||||
|
||||
```unison
|
||||
ability R t where
|
||||
die : () -> x
|
||||
near.impl : Nat -> Either () [Nat]
|
||||
|
||||
R.near n = match near.impl n with
|
||||
Left e -> die ()
|
||||
Right a -> a
|
||||
|
||||
R.near1 region loc = match R.near 42 with
|
||||
[loc] -> loc
|
||||
ls -> R.die ()
|
||||
```
|
||||
|
||||
```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`:
|
||||
|
||||
ability R t
|
||||
R.near : Nat ->{R t} [Nat]
|
||||
R.near1 : region -> loc ->{R t} Nat
|
||||
|
||||
```
|
||||
The issue was that abilities with parameters like this were sometimes
|
||||
causing failures like this because the variable in the parameter would
|
||||
escape to a scope where it no longer made sense. Then solving would
|
||||
fail because the type was invalid.
|
||||
|
||||
The fix was to avoid dropping certain existential variables out of
|
||||
scope.
|
Loading…
Reference in New Issue
Block a user