Fix support for (plain) rust type aliases

[ranjitjhala]

This code is surprisingly hard to get to work with our current resolver pipeline.

#![feature(register_tool)]
#![register_tool(flux)]

type MyResult<T> = Result<T, ()>;

#[flux::sig(fn() -> MyResult<i32>)]
pub fn test() -> MyResult<i32> {
    Ok(10)
}

The trouble is that by the time we get to it, we have to resolve

• path = MyResult with args = [i32]

with what rust has (at that point in rustc_middle -- NOT at hir) namely,

• path = Result with args = [i32, ()]

Of course we do have the alias-definition (can save it in the call-chain around insert_res_for_ident) but we actually do the zipping AFTER rustc has done the expansion which makes things very tedious AFAICT.

[nilehmann]

I think the following would work:

1. Add an extra case to surface::Res for type aliases here https://github.com/liquid-rust/flux/blob/0dfecc33f2c209ed3936ca09472da512fb8284d3/flux-syntax/src/surface.rs#L182
2. Proceed to generate a surface::Res::AliasTy here instead of following the alias here https://github.com/liquid-rust/flux/blob/0dfecc33f2c209ed3936ca09472da512fb8284d3/flux-desugar/src/table_resolver.rs#L347
3. During annot_check raise an error if the alias is refined in any way (just to simplify) and use tcx.type_of in zip_path to get the real type and check it is equal to the type we are zipping against.
4. During desugaring use tcx.type_of again to the get type in desugar_path and generate a type from it and raise an error if it's not supported. For that we could reuse this function https://github.com/liquid-rust/flux/blob/0dfecc33f2c209ed3936ca09472da512fb8284d3/flux-desugar/src/table_resolver.rs#L313

My hunch though is that a more elegant fix would be to do annot_check on fhir and not surface.

[nilehmann]

Actually, even simpler. In step 4. I think everything boils down to follow the alias here and here raising an error if not supported, that way the alias could be refined the same as the type it alias.

[ranjitjhala]

Yes I’m trying that route but the hassle is that in step 3 you basically have to “redo” the rustc alias expansion prior to the zipping (because the flux sig has the alias but the rust sig is expanded…)

On Fri, Nov 11, 2022 at 5:28 PM Nico Lehmann @.***> wrote:

I think the following would work:

1. Add an extra case to surface::Res for type aliases here https://github.com/liquid-rust/flux/blob/0dfecc33f2c209ed3936ca09472da512fb8284d3/flux-syntax/src/surface.rs#L182 https://urldefense.com/v3/__https://github.com/liquid-rust/flux/blob/0dfecc33f2c209ed3936ca09472da512fb8284d3/flux-syntax/src/surface.rs*L182__;Iw!!Mih3wA!CLySV2VAMMQbYbXnAYbZ-8lpjsUF36Dd6HTGOVlrY5GUsVPlfbHptPmkainH7LyXxCvs39mm0DPNwhznSW1AfnKR$
2. Keep the information that it's an alias here https://github.com/liquid-rust/flux/blob/0dfecc33f2c209ed3936ca09472da512fb8284d3/flux-desugar/src/table_resolver.rs#L347 https://urldefense.com/v3/__https://github.com/liquid-rust/flux/blob/0dfecc33f2c209ed3936ca09472da512fb8284d3/flux-desugar/src/table_resolver.rs*L347__;Iw!!Mih3wA!CLySV2VAMMQbYbXnAYbZ-8lpjsUF36Dd6HTGOVlrY5GUsVPlfbHptPmkainH7LyXxCvs39mm0DPNwhznSVAGF2n8$
3. During annot_check raise an error if the alias is refined in any way (just to simplify) and use tcx.type_of in zip_path https://urldefense.com/v3/__https://github.com/liquid-rust/flux/blob/main/flux-desugar/src/annot_check.rs*L209__;Iw!!Mih3wA!CLySV2VAMMQbYbXnAYbZ-8lpjsUF36Dd6HTGOVlrY5GUsVPlfbHptPmkainH7LyXxCvs39mm0DPNwhznSSuClc8i$ to get the real type and check it is equal to the type we are zipping against.
4. During desugaring use tcx.type_of again to the get type in desugar_path https://urldefense.com/v3/__https://github.com/liquid-rust/flux/blob/main/flux-desugar/src/desugar.rs*L396__;Iw!!Mih3wA!CLySV2VAMMQbYbXnAYbZ-8lpjsUF36Dd6HTGOVlrY5GUsVPlfbHptPmkainH7LyXxCvs39mm0DPNwhznSXJEgieR$ and generate a type from it and raise an error if it's not supported. For that we could reuse this function https://github.com/liquid-rust/flux/blob/0dfecc33f2c209ed3936ca09472da512fb8284d3/flux-desugar/src/table_resolver.rs#L313 https://urldefense.com/v3/__https://github.com/liquid-rust/flux/blob/0dfecc33f2c209ed3936ca09472da512fb8284d3/flux-desugar/src/table_resolver.rs*L313__;Iw!!Mih3wA!CLySV2VAMMQbYbXnAYbZ-8lpjsUF36Dd6HTGOVlrY5GUsVPlfbHptPmkainH7LyXxCvs39mm0DPNwhznSS65SHNI$

My hunch though is that a more elegant fix would be to do annot_check on fhir and not surface.

— Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/liquid-rust/flux/issues/227*issuecomment-1312301951__;Iw!!Mih3wA!CLySV2VAMMQbYbXnAYbZ-8lpjsUF36Dd6HTGOVlrY5GUsVPlfbHptPmkainH7LyXxCvs39mm0DPNwhznSRol7zuG$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OFIBF5YA3M234VOBUDWH3XB7ANCNFSM6AAAAAAR6AOMC4__;!!Mih3wA!CLySV2VAMMQbYbXnAYbZ-8lpjsUF36Dd6HTGOVlrY5GUsVPlfbHptPmkainH7LyXxCvs39mm0DPNwhznSVRrOtC3$ . You are receiving this because you authored the thread.Message ID: @.***>

[nilehmann]

Yeah, step 3 is the ugly/hacky step, that we would avoid if annot_check was done in fhir instead of surface.

[nilehmann]

In any case, except for step 3, I think this is the right route. In desugaring, we need to know how a type is refined to proceed. Eventually, we want the possibility for aliases to be refined differently from the type they point to, so having the information that some path is an alias during desugaring is a step in the right direction.

[ranjitjhala]

Ok let me continue (I had already started along this and was at 3) -- btw the hir route sounds appealing but won't work if (or rather, when) we want to slap signatures onto imported functions from other crates...

On Fri, Nov 11, 2022 at 5:46 PM Nico Lehmann @.***> wrote:

In any case, except for step 3, I think this is the right route. In desugaring, we need to know how a type is refined to proceed. Eventually, we want the possibility for aliases to be refined differently from the type they point to, so having the information that some path is an alias during desugaring is a step in the right direction.

— Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/liquid-rust/flux/issues/227*issuecomment-1312309865__;Iw!!Mih3wA!HNJ6V9Gxp_eEpH60l4nTq5rboSUNe60relCXhp8o7Gs0pkm2DW8xCXZkB7HJQvoarrOT3Xc72MQFcjDEDEtmFn3o$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OH62UN3HVXST67XXF3WH3ZHRANCNFSM6AAAAAAR6AOMC4__;!!Mih3wA!HNJ6V9Gxp_eEpH60l4nTq5rboSUNe60relCXhp8o7Gs0pkm2DW8xCXZkB7HJQvoarrOT3Xc72MQFcjDEDAY1jMs9$ . You are receiving this because you authored the thread.Message ID: @.***>

[nilehmann]

I finally got into studying how prusti does extern specs and they use a pretty clever trick that we should probably copy. If we use their trick then none of this would matter. It involves using procedural macros which would take some time to set up but once we do it all of our problems will be solved.

[ranjitjhala]

We don’t have any api for “subst” in the flux types yes? Otherwise the way to do 3 is to “lower” a version of the alias def to flux, apply the subst to get the expanded sig and then zip…

On Fri, Nov 11, 2022 at 7:47 PM Nico Lehmann @.***> wrote:

I finally got into studying how prusti does extern specs and they use a pretty clever trick that we should probably copy. If we use their trick then none of this would matter. It involves using procedural macros which would take some time to set up but once we do all of our problems will be solved.

— Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/liquid-rust/flux/issues/227*issuecomment-1312349070__;Iw!!Mih3wA!A-NjV9PdGahU6X63Uz8Pjkkj9q3DWB0y2XY1Z6wNm0FhBTF36HF7jl92zkeJVNEnWgMIZ0alKiacR1MY972gpa5D$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OF5S4VAIMUEPL6DHRTWH4HNFANCNFSM6AAAAAAR6AOMC4__;!!Mih3wA!A-NjV9PdGahU6X63Uz8Pjkkj9q3DWB0y2XY1Z6wNm0FhBTF36HF7jl92zkeJVNEnWgMIZ0alKiacR1MY98DE5HTo$ . You are receiving this because you authored the thread.Message ID: @.***>

[nilehmann]

oh yeah yikes, I think now I'm seeing the problem. I don't see an easy route. we could get the hir type alias definition (https://doc.rust-lang.org/nightly/nightly-rustc/rustc_hir/hir/enum.ItemKind.html#variant.TyAlias) and then convert from hir::ty to rustc_middle::ty (https://doc.rust-lang.org/nightly/nightly-rustc/rustc_hir_analysis/collect/struct.ItemCtxt.html and https://doc.rust-lang.org/nightly/nightly-rustc/rustc_hir_analysis/astconv/trait.AstConv.html) but that sounds gross. I really do think the solution is to move annot_check to fhir

[ranjitjhala]

Will moving to fhir solve the main issue though ? Ultimately I think we have to reimplement some form of the rustc expansion, no?

On Fri, Nov 11, 2022 at 8:40 PM Nico Lehmann @.***> wrote:

oh yeah yikes, I think now I'm seeing the problem. I don't see an easy route. we could get the hir type alias definition ( https://doc.rust-lang.org/nightly/nightly-rustc/rustc_hir/hir/enum.ItemKind.html#variant.TyAlias https://urldefense.com/v3/__https://doc.rust-lang.org/nightly/nightly-rustc/rustc_hir/hir/enum.ItemKind.html*variant.TyAlias__;Iw!!Mih3wA!BfYorfytGG3gj3PFGqNYld35Ifq5_7kzuBeggbG6RSHAKdbyQroPjMJVwgHEvO8U_7AY1t8_7u3mj0DFh-xgtjtz$) and then convert from hir::ty to rustc_middle::ty ( https://doc.rust-lang.org/nightly/nightly-rustc/rustc_hir_analysis/collect/struct.ItemCtxt.html https://urldefense.com/v3/__https://doc.rust-lang.org/nightly/nightly-rustc/rustc_hir_analysis/collect/struct.ItemCtxt.html__;!!Mih3wA!BfYorfytGG3gj3PFGqNYld35Ifq5_7kzuBeggbG6RSHAKdbyQroPjMJVwgHEvO8U_7AY1t8_7u3mj0DFh2GlU6M4$ and https://doc.rust-lang.org/nightly/nightly-rustc/rustc_hir_analysis/astconv/trait.AstConv.html https://urldefense.com/v3/__https://doc.rust-lang.org/nightly/nightly-rustc/rustc_hir_analysis/astconv/trait.AstConv.html__;!!Mih3wA!BfYorfytGG3gj3PFGqNYld35Ifq5_7kzuBeggbG6RSHAKdbyQroPjMJVwgHEvO8U_7AY1t8_7u3mj0DFh42yhiJ0$) but that sounds gross. I really do think the solution is to move annot_check to fhir https://urldefense.com/v3/__https://github.com/liquid-rust/flux/blob/main/flux-middle/src/fhir.rs__;!!Mih3wA!BfYorfytGG3gj3PFGqNYld35Ifq5_7kzuBeggbG6RSHAKdbyQroPjMJVwgHEvO8U_7AY1t8_7u3mj0DFh0cLQCRZ$

— Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/liquid-rust/flux/issues/227*issuecomment-1312361775__;Iw!!Mih3wA!BfYorfytGG3gj3PFGqNYld35Ifq5_7kzuBeggbG6RSHAKdbyQroPjMJVwgHEvO8U_7AY1t8_7u3mj0DFh_Vzwhkn$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OH3NQWKVMMJNIRBKBLWH4NT7ANCNFSM6AAAAAAR6AOMC4__;!!Mih3wA!BfYorfytGG3gj3PFGqNYld35Ifq5_7kzuBeggbG6RSHAKdbyQroPjMJVwgHEvO8U_7AY1t8_7u3mj0DFhx9gWJNL$ . You are receiving this because you authored the thread.Message ID: @.***>

[nilehmann]

yeah, we would have to reimplement the rustc expansion anyways but that would happen during desugaring into fhir. In fhir, since we don't have aliases anymore, we could do annot_check against the rustc:Ty. What doing annot_check in fhir fixes is not doing the expansion twice.

[nilehmann]

More generally I've been thinking about how we support aliases for types with abstract refinements. Consider,

#[flux::refined_by(a: int, b: int, p: (int, int) -> bool)]
struct Pair {
    #[flux::field(i32[@a])]
    fst: i32,
    #[flux::field(i32[@b])]
    snd: i32,
}

Obviously, you don't want to spell out p explicitly every time you want to talk about, e.g., OrderedPairs, but you may want to talk about a and b, so you would want something like:

#[flux::alias(type OrderedPair[a, b] = Pair[@a, @b, |a, b| a < b)]
type OrderedPair = Pair;

Now the question becomes, how we desugar uses of OrderedPair. I was thinking that during desugaring we could treat OrderedPair as a type on its own right with a separated refined_by (a: int, b: int) so the following uses would work

  fn(pair: OrderedPair[@a, @b]) -> i32[a]

  desugars to 

  fn<a0: int, a1: int>(Pair[a0, a1, |a2, a3| a2 < a3) -> i32[a0];

fn(pair: OrderedPair) -> i32[pair.a] 

desugars to

fn<a0: int, a1: int>(Pair[a0, a1, |a2, a3| a2 < a3) -> i32[a0];

This would require having the alias during desugaring.

note: desugaring this fn(OrderedPair{v: v.a == v.b}) would be fun because it requires the existential to be partially applied

[nilehmann]

This was fixed in https://github.com/liquid-rust/flux/pull/350