unison/unison-src/transcripts/fix2355.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

743 B
Raw Permalink Blame History

Tests for a loop that was previously occurring in the type checker.

structural ability A t g where 
  fork : '{g, A t g} a -> t a
  await : t a -> a
  empty! : t a
  put : a -> t a -> ()

example : '{A t {}} Nat
example = 'let
  r = A.empty!
  go u = 
    t = A.fork '(go (u + 1))
    A.await t
  
  go 0
  t2 = A.fork '(A.put 10 r)
  A.await r

  Loading changes detected in scratch.u.

  I tried to infer a cyclic ability.
  
  The expression in red was inferred to require the ability: 
  
      {A t25 {𝕖36, 𝕖18}}
  
  where `𝕖18` is its overall abilities.
  
  I need a type signature to help figure this out.
  
     10 |   go u = 
     11 |     t = A.fork '(go (u + 1))
     12 |     A.await t