[AST-77][AST-89] Fix correct check_ir.check_pat

[crusso]

correct check_ir.check_pat subtyping checks; fix bug in source intepretation of variants; add test

Note the coverage checker complains about some patterns that seem complete to me. Gabor, please take a look at the test output. I expect the coverage checker might not be taking account of subtyping...

[ggreif]

Just for the heck of it, I also tried:

func baz (a : Int) = switch a {
   case (25 : Nat) ();
   case _ ()
}

And I got:

$ ./asc ../test/run/ir-litpat-subtype.as
ir-litpat-subtype.as:2.10-2.18: type error, pattern of type
  Nat
cannot consume expected type
  Int

Here nothing looks type-unsafe (after all 25 : Nat, and the clause matches a subset of the inputs), still we get an error. I guess that pattern matching of sum types and subtyping are not concepts that go well together.

Note, I don't suggest to change the the typechecker. Just wondering.

[ggreif]

Looks good to me. Some comments. The important point is that the front-end and IR type-checkers don't contradict each other. Otherwise the users find themselves between a rock and a hard place.

[crusso]

Just for the heck of it, I also tried:
func baz (a : Int) = switch a {
case (25 : Nat) ();
case _ ()
}
And I got:
$ ./asc ../test/run/ir-litpat-subtype.as
ir-litpat-subtype.as:2.10-2.18: type error, pattern of type
Nat
cannot consume expected type
Int

Here nothing looks type-unsafe (after all 25 : Nat, and the clause matches a subset of the inputs), still we get an error. I guess that pattern matching of sum types and subtyping are not concepts that go well together.
Note, I don't suggest to change the the typechecker. Just wondering.

@gabor I'm don't think we want to allow this. Consider the slightly more general:

func baz (a : Int) : Nat = switch a {
  case (x : Nat) x;    
 }

then the pattern matching should be doing a range check on a for this to be sound, which is not what we expect for variable patterns.

@rossberg? Bisst Du damit einverstanden?

[rossberg]

@crusso, interesting example. @gabor, I think it's not so much pattern matching and subtyping are at odds, but that it is somewhat tricky to interpret type annotations in a pattern correctly in the presence of subtyping. I think this example has to be rejected on the grounds that x has type Int, which is not a subtype of the annotation.