unison/unison-src/transcripts/fix3037.md
2024-06-25 11:11:07 -07:00

33 lines
639 B
Markdown

```ucm:hide
scratch/main> builtins.merge
```
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:error
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
```
Application version:
```unison:error
structural type A g = A (forall a. '{g} a ->{} a)
anA : A {}
anA = A base.force
h : A {IO} -> ()
h _ = ()
> h anA
```