unison/unison-src/transcripts/fix3037.output.md

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}
  
  

```