unison/unison-src/transcripts/fix4722.md

Tests an improvement to type checking related to abilities.

foo below typechecks fine as long as all the branches are checked against their expected type. However, it's annoying to have to annotate them. The old code was checking a match by just synthesizing and subtyping, but we can instead check a match by pushing the expected type into each case, allowing top-level annotations to act like annotations on each case.

scratch/main> builtins.merge

ability X a where yield : {X a} ()
ability Y where y : ()

type Foo b a = One a
type Bar a
  = Leaf a
  | Branch (Bar a) (Bar a)

f : (a -> ()) -> '{g, X a} () -> '{g, X a} () -> '{g, X a} ()
f _ x y = y

abra : a -> '{Y, X z} r
abra = bug ""

cadabra : (y -> z) -> '{g, X y} r -> '{g, X z} r
cadabra = bug ""

foo : Bar (Optional b) -> '{Y, X (Foo z ('{Y} r))} ()
foo = cases
  Leaf a -> match a with
    None -> abra a
    Some _ -> cadabra One (abra a)
  Branch l r ->
    f (_ -> ()) (foo l) (foo r)