This adds some cases to checkWanted that try to improve the flow of type information down through some constructs that could be thought of as branches. The primary one is if expressions. Previously the checking of

if b then t else f

would just be handled like ifFun b t f, where ifFun : Boolean -> a -> a -> a. But this means that t and f are synthesized, even in checking mode. Instead, now checking an if statement against T will check t and f against T.

Similarly, list literals are now checked against T by determining an element type and checking each element against that type. If T is of the form List E, then the element type is of course E. If T is a variable, then we make up a new variable, unify T with List e, then check against e.

This allows type information from annotations to successfully flow down through more varieties of expressions, which helps annotations to resolve duplicate ability variable problems in more situations. Previously, annotations on these expressions wouldn't do any good, because they flip over into synthesis mode, which gathers up multiple ability variables and then gets stuck, even if the annotation would prune away most of those variables when pushed through.

One thing to note is that the new if checking mode will sometimes reject things that happened to work before. For instance, if you write:

thunk : '{IO} ()
thunk = do ()

if x == 0 then id thunk
else if x == 1 then id thunk
else id thunk

Then it used to work, and now doesn't. However, the way this used to work is almost an accident. If you instead tried to write:

if x == 0 then
  if y == 0 then id thunk
  else id thunk
else id thunk

then it wouldn't work in the past, because the order the expression gets inferred in causes the problem. Now both fail, and can be resolved by annotating the if.

There are a couple other tweaks to try to maintain error message output. One message changed slightly, but it's essentially the same (just focusing on a subexpression).