Fix type and coverage checking for patterns

[rossberg]

This introduces a compatibility relation that partitions types into subsets with compatible representations that can be matched against each other. Pattern matches are rejected when they mix patterns of incompatible types, e.g., Nat vs Any.

On the way, ran into various bugs with type and coverage checking for patterns, as well as handling Non in compiler.

Summary:

• Restrict type inference for alt patterns to disallow joining incompatible types. This also includes objects of different shape (previously, we typed func({a=0} or {b=1}) {} as {} -> (), which was unsound under a non-reflective interpretation of object patterns.)
• Fix checking of type annotations in patterns to disallow out-of-bounds values from supertypes that would break coverage checker (previously, we would have accepted switch (x : Nat) { case (-1 : Int) ... }).
• Abstract operator typing and fix typing of unop in patterns.
• Fix incorrect use of short-cutting && in abstract interpretation in coverage checker.
• Fix coverage checking for unary variants.
• Simplify coverage checking for objects.
• Fix IR checker for patterns, which had some cases the wrong way round.
• Handle Non as function type in calling convention conversion.
• Handle Non as operand type for arithmetic operators.
• Handle empty switch case lists.
• Print Non as "None" now.

[crusso]

For nat, does this just trap on non-zero values?

[ggreif]

No, negation has Nat -> Int type in the type checker. See special_unop_typing (literals).

[rossberg]

No, negation has type Int -> Int. But by subsumption you can also apply it to Nat.

And because -n has type Int ij patterns as well, trying to match a Nat against a signed literal is a type error. So no runtime error can occur.

[crusso]

Hmm, I'm a little confused. I can understand not allowing this:

> func f(x:Any) : Bool = switch x { case (_:Bool) true; case _ false};
stdin:12.41-12.47: type error, pattern of type
  Bool
cannot consume expected type
  Any

But I'm surprised this works:

> func f(x:Any) : Bool = switch x { case (true or false) true; case _ false};
let f : Any -> Bool = func
> f true;
true : Bool

Should I be?

[rossberg]

Yes, you should be. That's a bug.

[crusso]

Should all the cases (and scrutineer) have compatible types? I notice that only alt-patterns enforce this.

[rossberg]

Crap, I shouldn't be using check_lit for patterns, that does a sub test that's too relaxed.

[rossberg]

Er, actually, your example is rejected for me:

> func f(x:Any) : Bool = switch x { case (true or false) true; case _ false};
stdin:1.41-1.45: type error, literal pattern cannot consume expected type
  Any

What version did you try?

[rossberg]

Should all the cases (and scrutineer) have compatible types? I notice that only alt-patterns enforces this.

AFAICS, alt-patterns are the only place where incompatible types could arise for infer_pat. And in check_pat the property is implied by the requirement that the scrutinee's type is a subtype of the pattern type. But I may well be missing something.

[crusso]

Er, actually, your example is rejected for me:

func f(x:Any) : Bool = switch x { case (true or false) true; case _ false};
stdin:1.41-1.45: type error, literal pattern cannot consume expected type
Any

What version did you try?

I'm pretty sure I just checkout out your branch and built it. Lemme double check

[crusso]

Er, actually, your example is rejected for me:

func f(x:Any) : Bool = switch x { case (true or false) true; case _ false};
stdin:1.41-1.45: type error, literal pattern cannot consume expected type
Any

What version did you try?

My fault. I must have a stray asc on my nix path. I had build it but invoked the wrong compiler:

[nix-shell:~/actorscript/src]$ asc
ActorScript 0.1 interpreter
> func f(x:Any) : Bool = switch x { case (true or false) true; case _ false};
let f : Any -> Bool = func
> ^C

[nix-shell:~/actorscript/src]$ ./asc
ActorScript 0.1 interpreter
> func f(x:Any) : Bool = switch x { case (true or false) true; case _ false};
stdin:1.41-1.45: type error, literal pattern cannot consume expected type
  Any
> 

[nomeata]

nix-env -e asc if that’s where the asc in the PATH is coming from and you don't actually want it there

[crusso]

This is a bit ugly check_pat_fields env s [] pfs ve at - are you just trying force into the previous error case?

[rossberg]

Yes, no reason to duplicate the error case.

[crusso]

I'd find this easier to read if tfs and pfs were matched in the same order as passed in...

[rossberg]

Done

[crusso]

Is this really the correct compare to use since (in types) the fields are sorted by compare_field?

[rossberg]

Oh dear. Can't use compare_field, since there is no type field for the pattern. Solved with an extra case for now.

[crusso]

This feels kinda arbitrary - is it actually safe to do this?

[rossberg]

It is arbitrary, because it is unreachable code. The only thing that matters is that it leads to well-typed IR code. I was assuming that unary parameters/results always type-check, is that wrong?

[crusso]

Why Sharable? that seems a bit arbitrary.

[rossberg]

Because that implies the least constraints, so is kind of principal (I think). What else would you pick?

[crusso]

I took a look - might be worth getting Gabor and Joachim to comment on coverage and compilation.

[rossberg]

Addressed/answered @crusso's comments. Added @nomeata for backend bits. Pinging @ggreif. :)

[nomeata]

not sure about the changes to compile.ml, but I don't have a full picture. Are there now more cases where we have types Non floating around?

If so, the proper solution is for the back-end to never compile code that deals with values of type Non.

Probably not worth holding this up, but please see my comment about the change to branch.

[nomeata]

Why are you turning a static error to a dynamic one here?

If this is really intentional, then you shouln’t change branch, but change the use to branch_default with G.i Unreachable as the default.

[nomeata]

This is fishy. of_type should only be used for types that have operations. And Non does not have a stack representation, it should never happen. So if there are now more situations where Non shows up, maybe the backend should detect that earlier.

[rossberg]

I don't think this change adds more cases allowing None, it merely adds/activates more tests that exercise them, so these are essentially bug fixes. Happy to fix them in more adequate ways with some guidance. My poor attempt was to default in some suitable way -- since this is always dead code it shouldn't matter what is generated, as long as it validates.

[nomeata]

since this is always dead code it shouldn't matter what is generated, as long as it validates.

Returning Vanilla for Non will push the issue further out, but yeah, there might be a bigger existing issue lurking here, so no need to hold up this PR.

[nomeata]

I see that StackRep.of_type (which is worrying me here) was added by @ggreif, and only in relation to overloaded bits and implementation of primitives, e.g.

       | "Nat->Nat32"
       | "Nat->Nat16"
       | "Nat->Nat8" ->
         let ty = exp.note.note_typ in
         StackRep.of_type ty,

Gabor: I think using the source note here is not appropriate, and it would be cleaner to choose the stack rep based on the name of the primitive. (But this is probably not what’s biting here)

The other uses of of_type are in operations and relations, where the t is the “operator type” as stored in the AST (not the note), which we assumed would always be a primitive type. If that type can be Non, then… well, then the code in the PR is ok.

Might be worth having a dedicated stack rep for unreachable. Oh, we have that! An operator at type Non should expect its arguments in stack rep Vanilla (the top of the lattice), and return Non.

I can do that separately.

[rossberg]

Ping @ggreif

[ggreif]

Ping @ggreif

I just came back, having a look.