Use SubSet type as constructor

[seebees]

It would be nice to be able to just use a SubSet type in the same way as the underlying datatype.

datatype Foo = Foo(bar: string)

type ShortFoo = f: Foo | |f.bar| < 20

// What I want
var good := ShortFoo("This is longer than 20 so just do it!");
var bad := ShortFoo("Too Short, error");

[MikaelMayer]

Thanks for suggesting improvements. I see the value when the datatype has only one constructor and that constructor has the same name, but this is a narrow case.
This suggestions needs refinement. I will close it for now until there is a consensus.
For example, What if you have multiple constructors?

datatype Foo = Foo(bar: string) | Foo2(bar: string)

type ShortFoo = f: Foo | |f.bar| < 20 witness Foo("")

var good := ShortFoo("This is longer than 20 so error"); // What does it mean? Foo or Foo2?
var bad := ShortFoo("It's working");

[seebees]

Leaving this here: we can make the requirement regarding ShortFoo into a predicate. This makes it more portable, but there is still only an implicit binding between these two things.

Another way I might think about it would be to be able to extract the requirements about the SubSet type
directly from said SubSet type.

Perhaps we could use is? Like good is ShortFoo == true?

[MikaelMayer]

To extract the requirements about the subset type, you can already do this:

var bad: ShortFoo := Foo("This is longer than 20 and will raise an error");

Were you thinking of something else?

[seebees]

Yes. The above is a static check. What if I am making (or given) a Foo from arbitrary data that I can not reason about statically?

var maybeBad: ShortFoo := Foo(myStringThatMayOrMayNotBeGood);

It is obviously possible to do because I can investigate what the condition is that makes something a ShortFoo,
but this... "brakes encapsulation".

[MikaelMayer]

Oh, I see. Actually, it looks like you are defining a use case that would go along this PR:

#1522

In this PR, we explicitly allow the use of subset types in comprehensions, and we compile the condition in the loop. We can do this because if the subset constraint is not satisfied, we can just skip the element.

The problem of doing it on one single element is the failure handling. If you say it cannot be checked statically and you want a dynamic check, since Dafny is meant to be sound, it has to handle failure gracefully.

In this case, you would use the elephant operator :- and the following code:

function method CreateShortFoo(x: string): Outcome<ShortFoo> { if |x| < 20 then Success(ShortFoo(x)) else Failure("Length exceeded 20"); }

method f() returns (r: Outcome<....>) {
  var maybeBad: ShortFoo :- CreateshortFoo("My long string that will generate an error");
}