Term-level type annotations for effectful operations.

[dhil]

This patch makes it possible to annotate effectful operations at the term-level. Type annotations are crucial when operations are polymorphic. Prior to this patch, it was only possible to annotate polymorphic operations in signatures. As a consequence it was impossible to make the following kind of program type-check.

handle(do Throw) {
  case ans -> Just(ans)
  case <Throw> : (forall a. () => a) -> Nothing
}

The problem is that Links does not infer polymorphism (rightly so), so the inferred type of Throw will fail to check against the pattern type in the Throw-case. With this patch we can annotate the invocation to make the program type check.

handle(do (Throw : forall a. () => a)) {
  case ans -> Just(ans)
  case <Throw> : (forall a. () => a) -> Nothing
}

[dhil]

Closing and reopening to activate CI.