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} ```