Open ranjitjhala opened 8 months ago
I'm assuming there are no GADT shenanigans possible?
Yes, there are no GADTs in Rust and I doubt it will ever be possible because of monomorphization. Although, in theory, you could change the type if it has the same layout. I guess you could change the refinement in each variant.
If we do remove the type from the syntax, I suppose it looks weird to specify the indices by position and maybe we should write the names.
#[flux::refined_by(is_some: bool)]
enum Option<T> {
#[flux::variant([is_some: false])]
None,
#[flux::variant((T) -> [is_some: true])]
Some(T)
}
This starts to look awfully close to the "external" index/measure notation with the difference that you write all the indices/measures at once.
The only reason we need to check this is that we allow you to write the "return type" for a variant. If we instead had:
then, this wouldn't cause any problems. Not in this PR, but we should consider changing the syntax.
_Originally posted by @nilehmann in https://github.com/flux-rs/flux/pull/586#discussion_r1437115186_