unison/unison-src/transcripts/fix2355.output.md

42 lines
743 B
Markdown
Raw Permalink Normal View History

Tests for a loop that was previously occurring in the type checker.
``` unison
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
```
``` ucm
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.
2021-08-31 18:17:11 +03:00
I need a type signature to help figure this out.
10 | go u =
11 | t = A.fork '(go (u + 1))
12 | A.await t
```