mirror of
https://github.com/unisonweb/unison.git
synced 2024-09-11 02:25:39 +03:00
65 lines
1.3 KiB
Markdown
65 lines
1.3 KiB
Markdown
Tests for an unsound case of ability checking that was erroneously being
|
|
accepted before. In certain cases, abilities were able to be added to rows in
|
|
invariant positions.
|
|
|
|
``` unison
|
|
structural type Runner g = Runner (forall a. '{g} a -> {} a)
|
|
|
|
pureRunner : Runner {}
|
|
pureRunner = Runner base.force
|
|
|
|
-- this compiles, but shouldn't the effect type parameter on Runner be invariant?
|
|
runner : Runner {IO}
|
|
runner = pureRunner
|
|
```
|
|
|
|
``` ucm
|
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
I found an ability mismatch when checking the expression in red
|
|
|
|
3 | pureRunner : Runner {}
|
|
4 | pureRunner = Runner base.force
|
|
5 |
|
|
6 | -- this compiles, but shouldn't the effect type parameter on Runner be invariant?
|
|
7 | runner : Runner {IO}
|
|
8 | runner = pureRunner
|
|
|
|
|
|
When trying to match Runner {} with Runner {IO} the right hand
|
|
side contained extra abilities: {IO}
|
|
|
|
|
|
|
|
```
|
|
Application version:
|
|
|
|
``` unison
|
|
structural type A g = A (forall a. '{g} a ->{} a)
|
|
|
|
anA : A {}
|
|
anA = A base.force
|
|
|
|
h : A {IO} -> ()
|
|
h _ = ()
|
|
|
|
> h anA
|
|
```
|
|
|
|
``` ucm
|
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
I found an ability mismatch when checking the application
|
|
|
|
9 | > h anA
|
|
|
|
|
|
When trying to match A {} with A {IO} the right hand side
|
|
contained extra abilities: {IO}
|
|
|
|
|
|
|
|
```
|