Engine: F*: Missing rec qualifier in a mutually recursive top-level let

[W95Psp]

In some situations (likely connected to mutual bundles), mutual recursive functions get translated to let ... and ... bundles, but without the rec.
We need a reproducer here.

[maximebuyse]

Here is a simple reproducer:

mod a {
    pub trait A{
        fn f(&self);
    }
    impl A for i32 {

        fn f(&self){
            g(*self)
        }
    }
    pub fn g(x: i32) {super::b::h(x)}
}
mod b {
    pub fn h(x: impl super::a::A){x.f()}
}

Open this code snippet in the playground

This happens because the trait impl is considered to be part of the item-wise bundle. We should force item-wise bundles to contain either only functions or only types.

[maximebuyse]

This is actually tricky. We can minimize further to:

pub trait A{
    fn f(&self);
}
impl A for i32 {

    fn f(&self){
        g(*self)
    }
}
pub fn g(x: i32) {x.f()}

Open this code snippet in the playground
This is translated to the following F*:

class t_A (v_Self: Type0) = {
  f_f_pre:v_Self -> Type0;
  f_f_post:v_Self -> Prims.unit -> Type0;
  f_f:x0: v_Self
    -> Prims.Pure Prims.unit
        (f_f_pre x0)
        (fun result -> f_f_post x0 result)
}

[@@ FStar.Tactics.Typeclasses.tcinstance]
let impl_A_for_i32: t_A i32 =
  {
    f_f_pre = (fun (self: i32) -> true);
    f_f_post
    =
    (fun (self: i32) (out: Prims.unit) ->
        true);
    f_f = fun (self: i32) -> g self
  }

and g (x: i32) : Prims.unit =
  f_f #i32
    #FStar.Tactics.Typeclasses.solve
    x

Here there is a mutual recursion between a method from a trait impl, and a top-level function. At the item level we have a cyclic dependency between g and impl_A_for_i32 but we cannot declare the impl with a let rec.

I think the only way to solve this would be to hoist the method outside the impl. That can at least give a workaround (hoisting manually).

[maximebuyse]

After more investigation the reproducer is for a different problem. We should investigate more, there could be a bug in how we compute the dependency graph.

[maximebuyse]

Here is a reproducer: #1186.

This is linked to naming (clash of names with bundling).

[franziskuskiefer]

trait T { fn f(); }

pub mod a {
    impl super::T for u8{ fn f(){g()}}
    pub fn g(){super::b::g()}
}

pub mod b {
    impl super::T for i8 { fn f(){}}
    pub fn g(){super::a::g()}
}

Open this code snippet in the playground

[maximebuyse]

Here is another interesting reproducer without bundles:

fn f () {g()}

fn f_2(){f()}

fn g () {f()}

Open this code snippet in the playground

The problem is that mutual recursion is treated by inserting a rec in front of the first item in the mutual recursion and an and in front of the others. But we assume that they will come next to one another in the ordering which is apparently not true. So this is an issue in items sorting.

[maximebuyse]

I tried using #1140 which doesn't fix the problem. We probably need to add some dependencies in the dependency graph to treat a set of mutually recursive items as atomic.

[maximebuyse]

I believe this comes from a bug in ocamlgraph. I opened backtracking/ocamlgraph#149

[maximebuyse]

I implemented a simple fix to ocamlgraph so if we don't get an answer quickly we have something we can use in a fork.

Actually it might be a good thing not to rely on a standard implementation for this (except if we know what it does), because if you think of a graph like a <->c b <->d and want a stable topological sort with lexical order, then a, b, c, d could be considered the best answer but in our case we want elements that belong to the same cycle grouped together. My fork would behave well (for us) with respect to this but let's see if whatever solution that gets into ocamlgraph has this property.