mirror of
https://github.com/unisonweb/unison.git
synced 2024-08-15 13:30:27 +03:00
0031542faf
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.
1.4 KiB
1.4 KiB
Tests for an ability failure that was caused by order dependence of checking wanted vs. provided abilities. It was necessary to re-check rows until a fixed point is reached.
unique ability C c where
new : c a
receive : c a -> a
send : a -> c a -> ()
unique ability A t g where
fork : '{A t g, g, Exception} a -> t a
await : t a -> a
unique ability Ex where raise : () -> x
Ex.catch : '{Ex, g} a ->{g} Either () a
Ex.catch _ = todo "Exception.catch"
C.pure.run : (forall c . '{C c, g} r) ->{Ex, g} r
C.pure.run _ = todo "C.pure.run"
A.pure.run : (forall t . '{A t g, g} a) ->{Ex,g} a
A.pure.run _ = todo "A.pure.run"
ex : '{C c, A t {C c}} Nat
ex _ =
c = C.new
x = A.fork 'let
a = receive c
a + 10
y = A.fork 'let
send 0 c
()
A.await x
x : '{} (Either () Nat)
x _ = Ex.catch '(C.pure.run '(A.pure.run ex))
Loading changes detected in scratch.u.
I found and typechecked these definitions in scratch.u. If you
do an `add` or `update`, here's how your codebase would
change:
⍟ These new definitions are ok to `add`:
ability A t g
ability C c
ability Ex
A.pure.run : (∀ t. '{g, A t g} a) ->{g, Ex} a
C.pure.run : (∀ c. '{g, C c} r) ->{g, Ex} r
Ex.catch : '{g, Ex} a ->{g} Either () a
ex : '{C c, A t {C c}} Nat
x : 'Either () Nat