Include subtypes in case patterns

[RustanLeino]

This is a proposal to extend how Dafny handles explicitly typed bound variables in case patterns. In particular, the proposal is to make such types part of the pattern, rather than being an assertion about what holds about such a pattern. In other words, the proposal is to change the meaning of x: X in a case pattern from a type assertion (assert ... x is X) to a type test (if ... x is X).

Background

Case patterns can introduce bound variables. Most often, these variables are just named and their types are inferred. For example, given the usual

datatype List<T> = Nil | Cons(head: T, tail: List<T>)

and given xs: List<int>, the statement

match xs
case Nil =>
case Cons(x, rest) =>

infers x to have type int and rest to have type List<int>.

The bound variables are allowed to be given a type explicitly. For example, x can be declared explicitly to have type int as follows:

match xs
case Nil =>
case Cons(x: int, rest) =>

The semantics of giving such a type explicitly is that the program text asserts that any value that fits in the structural pattern given has the indicated type. For example,

match xs
case Nil =>
case Cons(x: nat, rest) =>

is saying that if xs has the form Cons(_, _), then xs.head is a nat. If this match statement is executed with xs being Cons(2, Cons(-3, Nil)), then it will bind x as 2. As another example, the program is in error if this match is reached with xs being Cons(-1, Nil) (as usual, the verifier will generate proof obligations to show that a program does not exhibit such errors).

Proposed new semantics

The proposal is to change the semantics of an explicitly given type to make the case apply only if the corresponding value has the given type. Under the proposed semantics, a case like case Cons(x: nat, rest) => would be taken only if xs is of the Cons variant and the head of the Cons is a nat. For an xs value like Cons(-1, Nil), the case would not be taken; instead, the next case in order will be considered (and, in the usual manner, the program is in error if no case applies).

Use case

Under the proposed semantics, one can write the following:

match xs
case Nil =>
case Cons(x: nat, rest) =>
  // this case is taken if xs.Cons? and xs.head is a nat
case Cons(y, rest) =>
  // this case is taken if the previous cases don't apply and xs.Cons?

Another use case

As another use case, consider the following types:

trait Tr { }
class A extends Tr { }
class B extends Tr { }

and suppose trs has type List<Tr>. Then, the following match statement gives separate cases for the head of the list being an A or a B:

match trs
case Nil =>
case Cons(a: A, rest) =>
case Cons(b: B, rest) =>

Under the proposed semantics, this match statement is semantically equivalent to

if trs == Nil {
} else if trs.Cons? && trs.head is A {
  var a: A := trs.head as A;
  var rest: List<Tr> := trs.tail;
} else if trs.Cons? && trs.head is B {
  var b: B := trs.head as B;
  var rest: List<Tr> := trs.tail;
} else {
  assert false;
}

In contrast, under the current semantics, it is semantically equivalent to

if trs == Nil {
} else if trs.Cons? {
  assert trs.head is A;
  var a: A := trs.head as A;
  var rest: List<Tr> := trs.tail;
} else if trs.Cons? {
  assert trs.head is B;
  var b: B := trs.head as B;
  var rest: List<Tr> := trs.tail;
} else {
  assert false;
}

where the second trs.Cons? case will never be taken.

Some details

Type tests

The proposed semantics involves a type test, rather than a type assertion. Such a type test is not always possible at run time, because the test may involve a ghost expression (in the constraint of a subset type) or may involve non-injective type parameters of reference types. Dafny already restricts such run-time tests elsewhere (for example, in comprehensions where a type test is needed, and in is expressions for reference types). Thus, if the match occurs in a compiled context, then these same restrictions apply to explicitly typed bound variables.

(The last case for a given structure does not require run-time type tests, since anything of that structure is verified to have that type. Nevertheless, I propose we don't treat this special case any differently.)

Redundant cases

The proposal affects the redundant-case checks. In particular, a warning about a redundant case should be generated only if there's a previous case whose types are supertypes. This should be done nominally (that is, without involving the verifier).

For example, given

type Even = x: int | x % 2 == 0
type Odd = x: int | x % 2 == 1

and xs: List<int>, we have

match xs
case Nil =>
case Cons(e: Even, rest) =>
case Cons(e: Even, rest) => // reported as redundant
case Cons(o: Odd, rest) =>
case Cons(x: int, rest) => // not reported as redundant, since this knowledge requires verification

As another example, given

type SmallInt = x: int | 0 <= x < 10
type SmallNat = x: nat | 0 <= x < 100

and again xs: List<int>, we have

match xs
case Nil =>
case Cons(n: nat, rest) =>
case Cons(s: SmallInt, rest) => // not reported as redundant, since the base type of SmallInt is not nat
case Cons(s: SmallNat, rest) => // reported as redundant
case Cons(x: int, rest) =>

[cpitclaudel]

Lovely! But surprising for subset types, at least until #1680 is solved: what's the desugared version of Cons(x: nat, …)? (We don't support is for subset types, nor do we expose their predicate as a function)

[RustanLeino]

There is currently no surface syntax like MySubsetType?(x) or x is MySubsetType, which is what #1680 is requesting. Instead, you may have inline the constraint itself. Having such syntax support would make it more straightforward to give a desugaring of the proposed case semantics in terms of Dafny itself. However, even without surface syntax, both the verifier and (with with upcoming #1604) the compiler can generate expressions that do the type test.

[fabiomadge]

It would be nice to additionally expose this capability to the programmer in a more generic way by allowing a guard in a CaseExpression.

[amaurremi]

I agree that this would be a very useful extension to Dafny. Similarly to @fabiomadge I was wondering whether implementing this would allow us to relatively easily add support for guards in case expressions.

Given that the proposal can report redundant checks, I assume that it would also report errors on non-exhaustive pattern matches, is that correct? E.g. if I write

match trs
case Nil =>
case Cons(a: A, rest) =>

would it report that case Cons(a: B, _) is missing?

And, similarly, if I have the following assertion:

assert trs.Cons? && trs.a is B

would it then accept the pattern match and not report the above case as missing?

Such a type test is not always possible at run time, because the test may involve a ghost expression (in the constraint of a subset type) or may involve non-injective type parameters of reference types

Did this intend to say "not always possible at compile time"?

In contrast, under the current semantics, it is semantically equivalent to ...

This was probably meant for explanation purposes, to contrast the proposal with the current semantics, but I believe that Dafny wouldn't allow me to pattern match on two case patterns that differ only in the type ascriptions, because it currently doesn't them as type checks.

[MikaelMayer]

I keep this in mind while working on #1604

[RustanLeino]

Dafny insists that the given cases are exhaustive. It is an error (in both match constructs and if-case statements) if no case applies. The verifier checks for this. This will not change.

The "redundant case" message is just a warning. It works accurately today, because we can syntactically distinguish the cases.

Under the proposed extension, it becomes more difficult to determine if a case a redundant, since case selection can depend on the types of values. Hence, I suggested that Dafny will use the declared base-type hierarchy of subset types (rather than the constraints given in subset-type declarations) to determine whether or not to give a "redundant case" warning (see the SmallInt example above). This means that there may be some unreachable cases that do not get flagged as "redundant case".

If we take yet another step and let the cases of a match give constraints, then redundant-case warnings become even more difficult to produce. If such constraints make for a useful feature that we decide to add, then I suggest that it take priority over producing accurate redundant-case warnings. In other words, if we (now or in the future) were to allow logical constraints as part of match cases, then I suggest that redundant-case warnings be produced only when it is clear from syntax and the declared base-type hierarchy that a case is redundant. There may then be unreachable cases for which there is no warning (which is also the case in the rest of Dafny).

[RustanLeino]

@amaurremi

Such a type test is not always possible at run time, because the test may involve a ghost expression (in the constraint of a subset type) or may involve non-injective type parameters of reference types

Did this intend to say "not always possible at compile time"?

There are type tests that cannot be performed at run time (and hence the compiler cannot emit code for doing it). For example, consider

datatype Flavor = Strawberry | Licorice | Vanilla
datatype IceCream = IceCream(flavor: Flavor, ghost popular: bool)
type PopularIceCream = c: IceCream | c.popular witness *

method Example(c: IceCream) {
  if c is PopularIceCream { // cannot be tested at run time
  }
}

It is not possible to test c is PopularIceCream at run time, because the ghost field popular is not available at run time.

[RustanLeino]

@amaurremi

In contrast, under the current semantics, it is semantically equivalent to ...

This was probably meant for explanation purposes, to contrast the proposal with the current semantics, but I believe that Dafny wouldn't allow me to pattern match on two case patterns that differ only in the type ascriptions, because it currently doesn't them as type checks.

(There was a typo in my example, where I had written rest instead of trs.trail. I fixed it now, but I don't think this is what led to any confusion. I also clarified the "Another Use Case" section by inserting the phrase "Under the proposed semantics,".)

The match statement I show in the use case as well as both of the desugarings shown are possible to write in Dafny today. However, you will get some verification errors, and the third case also produces a redundant-case warning.

[cpitclaudel]

An alternative to this approach is to some form of path-sensitive typing. We already have something like this in Dafny with null: inside a x != null branch x is known not to be null. We could make it so that inside an x is T branch x has type meet(T, Tx), where Tx is x's previously known type (for reference types) and we could assume the subset predicate within the branch (for subset types).

[RustanLeino]

Dafny does have the effect of path-sensitive typing, like in the example you gave. But it's not the type system that does this. Instead, the type is usually the base type (like T?) and whenever the type needs to be more specific (like T), the verifier checks that it satisfy the necessary subset-type constraint. For example, you can write

method M(b: bool, x: T?)
  requires b ==> x != null
{
  if b {
    // here, you can use x as if it had the non-null type T
  }
}

Note that x != null does not appear syntactically as the guard here.

[robin-aws]

I'm actually quite concerned that interpreting x: T as a type test rather than a type constraint is going to be very confusing for users. The language does not interpret that syntax with the former semantics anywhere else, instead using x is T. Even if changing this meaning is technically backwards compatible, that doesn't mean that Dafny user brains will easily make the switch. :)

I think I prefer the alternative of only supporting guard expressions instead, for clarify and consistency. Something like:

trait Tr { }
class A extends Tr { }
class B extends Tr { }

match trs
case Nil =>
case Cons(a, rest) where a is A =>
case Cons(b, rest) where b is B =>

Exhaustiveness just implies another proof obligation. If the desugared guards on a match statement/expression (assuming we can express a pattern like Const(a, rest) as something like trs.Cons?) are A, B, C and D, then the obligation would be something equivalent to !A && !B && !C ==> D. AFAICT that's the only necessary constraint since cases can overlap (and hence ordering is significant). The challenge then becomes more helpful error messages in the common cases, but I think it would be very compelling to support arbitrary guards with the safety net of a verifier to catch incorrect guards. This would also align nicely with the path-sensitive typing above.

[amaurremi]

The language does not interpret that syntax with the former semantics anywhere else, instead using x is T

I'm curious what kind of cases you have in mind, could you give an example of other Dafny features/patterns that would have a different flavour?

If the verifier provides exhaustiveness errors and redundant-case warnings, would the users not immediately understand what's going on?

[cpitclaudel]

I'm actually quite concerned that interpreting x: T as a type test rather than a type constraint

But the proposal is to interpret it as a type constraint: the branch is only taken if the constraint is satisfied. No?

Using where a is A is also confusing, because a is A is a test, not a cast, so the expectation might be that a will have type Tr in the branch (though arguably there's precedent in C# with path-sensitive types). If we do go that route, then we would have to change the semantics of "is" in a branch, too.

Besides the syntax is going to be pretty heavy:

trait Tr { }
class A extends Tr { }
class B extends Tr { }

match tr
case a where a is A =>
case b where b is B =>

[robin-aws]

I'm actually quite concerned that interpreting x: T as a type test rather than a type constraint

But the proposal is to interpret it as a type constraint: the branch is only taken if the constraint is satisfied. No?

I meant a "constraint" as in type checking - pretend I said "assertion" instead :)