Forbid impossible pattern matching on generic capabilities

[Praetonus]

This changes the capability rules for pattern matching from

"some possible instantiation of the operand is a subtype of some possible instantation of the pattern"

to

"every possible instantiation of the operand is a subtype of every possible instantiation of the pattern".

In practice this makes the compiler issue an error when a pattern can only ever match for some reification of the generic capability. Code that uses this kind of pattern matching should now use iftype instead.

This doesn't fix any safety issues.

[SeanTAllen]

@Praetonus we discussed this during sync and we aren't sure from your commit what this does. we think we know, but we aren't sure. can you give an example of what would be disallowed with this change (and ideally what currently happens in that case).

[jemc]

@Praetonus - I think I understand the goal of this (in that it's an extension of detecting impossible match at runtime), but I'm concerned about recommending iftype as a replacement for such code when it's still in experimental status, and not documented in the tutorial.

[Praetonus]

Let's take this code as an example:

fun foo[A: Any #send](a: A) =>
  match a
  | let a': Any val => print("val")
  else
    print("other")
  end

In the current state of things, a val reification of foo will print val, and an iso or tag reification will print other. The issue is that this is all determined at compile time. If you look at the generated code for e.g. foo[Any val], it won't contain any dynamic pattern matching code, only a call to print("val").

The above code is effectively equivalent to the following version with iftype:

fun foo[A: Any #send](a: A) =>
  iftype A <: Any val then
    print("val")
  else
    print("other")
  end

The main motivation here is to catch potential mistakes with match. If you're not familiar with the behaviour of capabilities at runtime, you could have a wrong idea about what the above code with match does (i.e. since match usually does dynamic checks you could think it does one here too). The problem isn't there with iftype since it never does dynamic checks. Also, it avoids having two different syntaxes that do the same thing.

I don't think recommending iftype instead is problematic. The feature is experimental because it is incomplete (the method-wide iftype is still missing), but it has tests in the compiler and is usable as is. I'll do a tutorial PR soon to add some documentation.

[mfelsche]

Do you think it would make sense to write a testcase that shows an example of what is forbidden now and asserts on the match error?

[Praetonus]

I've added a test.

[Praetonus]

Forgot about that one. Merging now.