Allow caps in result types of functions to be mapped to reaches

[odersky]

Allow caps in result types of functions to be mapped to reach capabilities

Example: If we have val f: A => C^ then f has type A => C^{f*}. Before it had that type only if A was pure. On the other hand, result caps are not replaced anymore. We used to have for val f: (x: A) => C^ with A pure that f: (x: A) => C^{f*}. That's no longer the case. In this case, f now has type f: (x: A) => C^ with the ^ understood to be existentially bound.

This aligns the implementation with the Capless paper.

[Linyxus]

looks great to me overall!

There is one thing about which we have to be extra careful after this change: we should restrict widening a dependent function to the non-dependent one, since this will implicitly change the way caps are interpreted as existentials and mess things up. For instance, the following example typechecks currently but morally it should not:

import language.experimental.captureChecking
trait File
def usingFile[R](op: File^ => R): R = op(new File {})
def id(x: File^): File^{x} = x
def test1(): Unit =
  val op: File^ -> File^ = id  // this should be disallowed
  val g: File^ -> File^{op*} = op  // otherwise we can brand arbitrary File as simply capturing op*

The thing is that we should not widen (f: File^) -> File^{f} to File^ -> File^ since the latter means exists c. File^ -> File^{c} where the existential is quantified at the outermost level and couldn't refer to this local parameter f.

[odersky]

@Linyxus The error goes undetected since we turn off separation checking by default now. With separation checking on, we get:

-- [E007] Type Mismatch Error: reach-in-results.scala:7:4 ----------------------
7 |    val y = (x: File^) => id(x)  // this should be disallowed
  |    ^
  |Found:    (x: File^) -> File^²
  |Required: (x: File^) -> File^³
  |
  |where:    ^  refers to the universal root capability
  |          ^² refers to a root capability associated with the result type of (x: File^): File^²
  |          ^³ refers to a fresh root capability in the type of value op
8 |    y
  |
  | longer explanation available when compiling with `-explain`

I'll tweak the rules so that we produce FreshCap instances even if separation checking is off.

[Linyxus]

LGTM!