Recursive constraint dep

[keyboardDrummer]

What was changed?

• Allow type definitions to refer to the same type if the type is not a type synonym
• Allow wildcards and assume statements to be parsed in the binary format

How has this been tested?

• Added a few tests

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[RustanLeino]

I don't understand this line. In fact, if I remove it, the new test example still goes through.

This line looks to me as if it would be true for any SCC of size 1. If so, this if condition would always be true. Here's my reasoning: If the SCC where dd is has size 1, then the only successor of dd is dd itself.

If you think this line is necessary, please add a comment describing what it does.

[RustanLeino]

With this change, you have removed one of the recursive constraint dependency error messages. But there must be more places in the code that generate it. Case in point: the cycles.dfy test case (below) generates such a message.

As I will argue (in a comment that I'm about to post on the PR), I think we should remove those messages, too.

(But we do need to still check for cycles that consist solely of type synonyms, as you still do here on LL 4229-4232.)

[RustanLeino]

Great example! (I think you got this from me. :)) But I would like to see this program go through. The cycles.dfy.expect file below shows that an error is still generated for this program.

[RustanLeino]

A recent change in Dafny was to make verification error messages more consistent. I believe those verification error messages now start with a lower-case letter. I'm not suggesting we change all resolution errors the same way (or at least not in this PR), but I think it would be nice to change this one.

[RustanLeino]

I'm puzzled by this PR. I think its main objective is to remove the recursive constraint dependency restriction, but it somehow manages to do so only for cycles that go through type-parameter bounds. There must be some other place in the code that also checks for this, and I suggest we change that place, too, to remove the recursive constraint dependency restriction (which I think is not needed).

I have written some test cases to help me think of both the situation that is fixed by the current PR and some other situations that I would like to see changed in the same way. I'll post the examples as comments here. The first batch of examples can be added as additional test cases for this change. And then I'll include another example (in addition to cycles.dfy) that I would like to see go through.

[RustanLeino]

These examples show the thinking I used to try to analyze the situation with the type bounds. I think these would make good test cases (with the comments in the code as shown -- or corrections, if my thinking is wrong).

// The PR does not affect things in this module. (Good!)
module GeneralTraitBase {
  trait Base<T extends Base<T>> {}

  datatype D extends Base<D> = Ctor {}

  datatype E_ extends Base<E> = ECtor {}
  type E = d: E_ | true witness ECtor

  class C extends Base<C> {}
  // class K extends Base<K?> {} // error:  K extends Base<K?>, not Base<K>
}

// The PR does not affect things in this module, either. (Good!)
module ReferenceTraitBaseWithNullableBound {
  // Note, what follows `extends` in Dafny is a type bound is a trait _type_ or a subset type thereof
  // (that is, not necessarily a parameterized trait _name_).
  trait Base<T extends Base?<T>> extends object {}

  class C extends Base<C> {} // allowed, because C satisfies the type bound Base?<C>
  class K extends Base<K?> {} // allowed, because K? satisfies the type bound Base?<K?>

  // The following is not allowed, because what follows `extends` in a type declaration is expected to
  // be a trait name (possibly with type parameters), not a type.
  // class M extends Base?<M> {} // error
}

module ReferenceTraitBase {
  // The following declaration was previously not allowed, but the PR makes it allowed.
  //
  // Why?
  // By the rules of what follows `extends` in a type bound, `extends Base<T>` would be allowed,
  // since `Base` is a subset type of a trait (namely, the non-null subset type of type `Base?`).
  // However, before this PR, Dafny would flag this as an error, because the dependency cycle
  // Base -> Base? -> Base (or, in my more detail, "the non-null subset type Base depends on its
  // base type Base?" and "a type bound of the nullable Base? type mentions the non-null type Base")
  // involves a subset type (namely, the non-null subset type Base).
  //
  // When this issue was brought into light recently, it seemed that there is no reason to forbid
  // dependency cycles that involve subset types. The PR thus removes this restriction, but only in
  // a limited way.
  trait Base<T extends Base<T>> extends object {}

  class C extends Base<C> {}

  // The following is not allowed (and should remain disallowed), because K? extends Base<K?>,
  // not Base<K> as requires by the type bound in trait Base.
  // class K extends Base<K?> {} // error
}

module MySubsetType {
  // In the following example, I'm defining a general trait (that is, not a reference trait) Base_.
  // Except for that no reference types are involved, Base_ and Base are have the exact same
  // relationship as Base? and Base in module ReferenceTraitBase above.
  //
  // This example was not allowed previous, but it is now allowed by the PR.
  trait Base_<T extends Base<T>> {}
  type Base<T extends Base<T>> = b: Base_<T> | true witness *

  // Note that this is still not allowed, because C extends Base_, not its subset type Base.
  // class C extends Base_<C> {} // error
  //
  // And the following is also not allowed, because what follows `class ... extends` is supposed
  // to be a trait name, which Base is not.
  // class C' extends Base<C'> {} // error
}

module MultistepCycle {
  // Before this PR, the following example also gave the same error about the dependency cycle involving a subset type.
  // After the PR, it is allowed.
  trait Base0<T extends Base3<T>> {}
  type Base1<T extends Base3<T>> = b: Base0<T> | true witness * // subset type
  type Base2<T extends Base3<T>> = Base1<T> // type synonym
  type Base3<T extends Base3<T>> = b: Base2<T> | true witness * // subset type
}

[RustanLeino]

I would like the example in cycles.dfy to go through without error. Likewise, I would like the following example to go through without error:

trait LinkedList /* WITH OR WITHOUT THIS: extends object */ {
  const length: nat
  ghost predicate Valid()
    decreases length
}

class NilList extends LinkedList {
  ghost predicate Valid()
    decreases length
  {
    length == 0
  }

  constructor ()
    ensures Valid()
  {
    length := 0;
  }
}

class ConstList extends LinkedList {
  const value: int
  // By declaring "next" to have type "ValidList", Dafny currently gives a "recursive constraint dependecy" error.
  // I think there is no reason for it to complain about such a recursive dependency.
  const next: ValidList

  ghost predicate Valid()
    decreases length
  {
    && length == next.length + 1
    && next.Valid()
  }

  constructor (value: int, next: ValidList)
    ensures Valid()
  {
    this.length := next.length + 1;
    this.next := next;
    this.value := value;
  }
}

type ValidList = list: LinkedList | list.Valid() witness *