type conversion not allowed to subtypes of inductive datatypes

[erniecohen]

Type conversion is supposed to be allowed from a base type to a subtype of that type, This currently gets an error if the base type is an inductive datatype:

type T = t:T_ | true ghost witness T()
datatype T_ = T()
function test():T { T() as T } // error "type conversions are not supported to this type (got T)"

[RustanLeino]

The set of types that can follow as is unnecessarily restricted (see, e.g., https://github.com/dafny-lang/dafny/issues/704). However, to accomplish what you want, you can just write T() instead of T() as T, because conversions of subset types happen automatically. If you want to make this explicit in the code, you can use a let expression (instead of T() as T), like this:

var t: T := T(); t

[erniecohen]

Thanks, that is the workaround that I have been using. I was just pointing out the bug.

[robin-aws]

Reopening since it's still a reasonable feature request