unison/unison-src/transcripts/fix2378.md

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.

scratch/main> builtins.merge

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))