unison/unison-src/transcripts/fix2355.output.md
2021-08-31 11:17:11 -04:00

700 B
Raw 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

  I tried to infer a cyclic ability.
  
  The expression in red was inferred to require the ability: 
  
      {A t25 {𝕖39, 𝕖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