unison/unison-src/transcripts/fix693.md

scratch/main> builtins.merge

structural ability X t where
  x : t -> a -> a

structural ability Abort where
  abort : a

scratch/main> add

This code should not type check. The match on X.x ought to introduce a skolem variable a such that c : a and the continuation has type a ->{X} b. Thus, handle c with h : Optional a, which is not the correct result type.

h0 : Request {X t} b -> Optional b
h0 req = match req with
  { X.x _ c -> _ } -> handle c with h0
  { d } -> Some d

This code should not check because t does not match b.

h1 : Request {X t} b -> Optional b
h1 req = match req with
  { X.x t _ -> _ } -> handle t with h1
  { d } -> Some d

This code should not check for reasons similar to the first example, but with the continuation rather than a parameter.

h2 : Request {Abort} r -> r
h2 req = match req with
  { Abort.abort -> k } -> handle k 5 with h2
  { r } -> r

This should work fine.

h3 : Request {X b, Abort} b -> Optional b
h3 = cases
  { r } -> Some r
  { Abort.abort -> _ } -> None
  { X.x b _ -> _ } -> Some b