Under CC, subtyping between a type variable and its impure upper bound is rejected

[Linyxus]

Compiler version

main

Minimized code

import language.experimental.captureChecking
trait IO

def foo[X <: IO^](x: X): IO^ = x

Output

-- [E007] Type Mismatch Error: issues/cc-typeapp.scala:4:31 ------------------------------------------------------------------------------------------------------------------------------------------------------------
4 |def foo[X <: IO^](x: X): IO^ = x
  |                               ^
  |                               Found:    (x : X)
  |                               Required: IO^
  |
  | longer explanation available when compiling with `-explain`

Expectation

It should work.

[Linyxus]

@noti0na1 and I looked into this issue and it seems to be an outcome of separating type comparison and box adaptation. What happened here:

• In box adaptation, we see LHS is X and RHS is IO^, both unboxed, so no adaptation happened.
• In type comparer, we widen X to box IO^ and the RHS is IO^, so the subtyping between them is rejected due to the mismatch in the box status.

In theory box adaptation and subtyping are entangled, and it seems that the entanglement does offer us more expressiveness when the adaptation and the subtyping comparison need to be interleaved, like the case here.

There are two possible solutions:

• Widening the type parameter on LHS until we see a concrete type. But this is tricky when unions and intersections come into play. And essentially this is attempting to mimic part of the logic in type comparison.
• Refactor box adaptation into type comparison. This solves the problem in the root. But it potentially complicates the type comparer, and states in capture checker need to be accessible from the type comparer (like the Envs that store captured variables).

We don't really know what action should be taken in this case. What do you think? /cc @odersky