unisonweb/unison
1
0
Fork 0
mirror of https://github.com/unisonweb/unison.git synced 2024-08-15 13:30:27 +03:00
Code Issues Projects Releases Wiki Activity
trunk
unison/unison-src/transcripts/fix3037.output.md
Greg Pfeil 0031542faf
Add a space before code block info strings 
This is for consistency with the `cmark` style. Now the blocks we still
pretty-print ourselves will match the bulk of them that `cmark`
produces.
2024-07-10 13:56:07 -06:00

1.3 KiB
Raw Permalink Blame History

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


  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:

structural type A g = A (forall a. '{g} a ->{} a)

anA : A {}
anA = A base.force

h : A {IO} -> ()
h _ = ()

> h anA


  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}