Skip to content

Latest commit

 

History

History
23 lines (15 loc) · 582 Bytes

fix3037.output.md

File metadata and controls

23 lines (15 loc) · 582 Bytes

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.

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

  The expression in red needs the {IO} ability, but this location does not have access to any abilities.
  
      8 | runner = pureRunner