ICE on FnDef

[ranjitjhala]

Code like the below

#[flux::sig(fn (x:usize) -> usize[x+1])]
fn inc(x: usize) -> usize {
    x + 1
}

#[flux::sig(fn(c: Option<usize[10]>) -> Option<usize[11]>)]
pub fn test(c: Option<usize>) -> Option<usize> {
    c.map(inc)
}

triggers

error[E0999]: unsupported terminator
 --> tests/tests/todo/fndef.rs:8:5
  |
8 |     c.map(inc)
  |     ^^^^^^^^^^
-Ztrack-diagnostics: created at crates/flux-middle/src/rustc/lowering.rs:274:34
  |
  = note: unsupported type `FnDef(DefId(0:3 ~ fndef[f288]::inc), [])`

Seems to be an issue in both vtock and zkevm...

[ranjitjhala]

@nilehmann do you anticipate anything super hard about this one?

[nilehmann]

Related to https://github.com/flux-rs/flux/pull/789. We will need to prove that the function implements the Fn trait, but the argument that there's nothing refined doesn't hold anymore. The bound on map doesn't have refinements but the signature of inc does. Not sure how the interaction works

[ranjitjhala]

Good point - I’ll just try to push along and see what happens …

• Ranjit.

On Thu, Sep 12, 2024 at 4:38 PM Nico Lehmann @.***> wrote:

Related to #789 https://urldefense.com/v3/__https://github.com/flux-rs/flux/pull/789__;!!Mih3wA!ErZ0wGPhA75NlSwAIflm_cmzXbo4NvTQvEN_fUMI9riYb1hNQLJKt8tCH72MxIQI7iFsXrXGod0nLzUwXx-JbZVP$. We will need to prove that the function implements the Fn trait, but the argument that there's nothing refined doesn't hold anymore. The bound on map doesn't have refinements but the signature of inc does. Not sure how the interaction works

— Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/flux-rs/flux/issues/793*issuecomment-2347413682__;Iw!!Mih3wA!ErZ0wGPhA75NlSwAIflm_cmzXbo4NvTQvEN_fUMI9riYb1hNQLJKt8tCH72MxIQI7iFsXrXGod0nLzUwX1QUyDzL$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OFNWUJVYHNK4UOSEHDZWIQVTAVCNFSM6AAAAABOEHZLGKVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDGNBXGQYTGNRYGI__;!!Mih3wA!ErZ0wGPhA75NlSwAIflm_cmzXbo4NvTQvEN_fUMI9riYb1hNQLJKt8tCH72MxIQI7iFsXrXGod0nLzUwX0lxK8py$ . You are receiving this because you were assigned.Message ID: @.***>

[nilehmann]

The type of Option::map is

forall T,U,F: FnOnce(T) -> U. fn(Option<T>, F) -> Option<U>

If we add support for TyKind::FnDef and everything else is left as is we would instantiate the signature to

fn(Option<i32{v: $k1}>, {inc}) -> Option<i32{v: $k2}>

plus the obligation {inc}: FnOnce(i32{v: $k1}) -> i32{v: $k2} where {inc} is the (singleton) type of the inc function.

If we drop the obligation (we don't check function subtyping) $k2 would be unconstrained which would be very bad.

[ranjitjhala]

Yes indeed that would be bad.

It should suffice to generate a “function subtyping” obligation between

• the (already known) sig for inc
• the template generated for map (with k1, k2 etc)

which itself should be a stepping stone towards the proper handling of closures?

• Ranjit.

On Thu, Sep 12, 2024 at 4:49 PM Nico Lehmann @.***> wrote:

The type of Option::map is

forall T,U,F: FnOnce(T) -> U. fn(Option, F) -> U

If we add support for TyKind::FnDef we would instantiate the signature to

fn(Option<i32{v: $k1}>, {inc}) -> i32{v: $k2}

plus the obligation {inc}: FnOnce(i32{v: $k1}) -> i32{v: $k2} where {inc} is the (singleton) type of the inc function.

If we drop the obligation (we don't check function subtyping) $k2 would be unconstrained which would be very bad.

— Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/flux-rs/flux/issues/793*issuecomment-2347422442__;Iw!!Mih3wA!HfoanxR36iCtFajs7s-w9FFwhhld-ec4oWlfr-6CIERIMmM1SOUKdFl97BaLXd4o0ita5z2j9WK_0GpYrZrET43B$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OCEPOOXE3MG2WHIWF3ZWIR6VAVCNFSM6AAAAABOEHZLGKVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDGNBXGQZDENBUGI__;!!Mih3wA!HfoanxR36iCtFajs7s-w9FFwhhld-ec4oWlfr-6CIERIMmM1SOUKdFl97BaLXd4o0ita5z2j9WK_0GpYrYRiGiVk$ . You are receiving this because you were assigned.Message ID: @.***>