Having just talked to Leo about this, it might be that in fact (kind of conversely) the existing Invariant_params semantics might be ok, but the logic for determining which recursive calls are to be repointed to the specialised version might not match up with it. I am going to investigate that too.

Right, so it looks like the way things work at the moment, we are going to freshen up all occurrences of the recursively-bound identifiers during simplification after specialisation---meaning that we probably do need to fix Invariant_params as per this patch.

However the case that used to be assert false should indeed still be assert false. I will fix this now

@chambart I'm unsure whether the function variable <-> symbol mapping construction could still be at toplevel only. Leo suspects maybe it could be since we'll never replace a recursive call via a symbol in a subfunction during specialisation.

@chambart Looking at Freshening.rewrite_recursive_calls_with_symbols it looks like we actually only rewrite symbols to fun_vars at toplevel, so in which case, I think I'm going to leave the toplevel-only iteration for constructing function_variable_alias in Invariant_params. Let me know if you disagree.

Yes only toplevel application are rewritten since this function was not supposed to find compatible deep function calls.

Also the current substitution effectively does not allow non invariant recursive calls, so Invariant_params really need to be an overapproximation as you noticed. The original rationale was that I had absolutely no idea of what would be the heuristic deciding whether some recursive calls where important or not to allow specializing functions with only some recursive calls that were kept. So I went for the simple substitution version (that don't need to look at the aliases of arguments to decide how to substitute).

By the way in the subpart

      let fail _ = Conv.failf "no variable allowed in sub-term under %s" id in
      let _ = term_to_tptp fail t in
      T.app (get_or_create_id id) (List.map (term_to_tptp fail) l)

Both recursive calls were did not preserve their arguments, why did this one not prevent the rewriting already ?

      let _ = term_to_tptp fail t in

Also I couldn't review carefully the change yet.

Oh, sorry, I pasted the wrong version of the code!
The extra line let _ was my test to confirm what was going on. It works if that line is there, but it doesn't if it's removed. (I've updated the main code fragment at the top of this pull request)

I think I know why we didn't spot it. Originally, inline_by_copying_function_declaration (or the name it had at the time) Applied a round of Flambda_utils.toplevel_substitution before running simplification, and was running simplification freshening. In particular, it had no freshening for the function itself. Hence in a situation like that, it was ok to specialize the recursive function as the specialisation was happening only toplevel, and deep recursive calls below functions where not changed. I think I forgot that when we made that change. Probably a lot of the testing related to that kind of cases were before that change.

Also, for it to trigger in a noticeable way, it had to trigger in a situation where the only call preventing specialisation is below a function that was not inlined or specialised at definition point, but became when the whole function became specialised. This might be quite unfrequent.

This fix will do for now.
But the general fix might be to check at the recursive call site whether to substitute the function for the specialised version or not. I will think a bit more on how to do this properly.

I tried to change a bit the handling of specialised recursive calls such that it would be safe to accept some recursive calls that does not keep the invariant parameters.

The simple version is to add the original closure to the environment of the function and substitute every uses that are not a direct call to use that one instead. In this example that would mean that in the specialised version of the function (which is useless here, but this is another problem) the closure passed to list map would bind the original closure instead of the specialised one.
Since local calls (toplevel in the recursive function) would not be missed, this is sufficient.

The change for that is quite minimal, but requires applying a potentially costly Flambda_utils.toplevel_substitution during the specialisation.

The not so simple version could push that idea a bit further and remember the original closure from which the specialised version comes from. When an application to the original closure is encountered inside the specialised function, if the arguments matches (are aliases) the call is rewritten to be a direct recursive one. This allows to also discover specialised calls opportunities after inlining inside the function, oppening the way for specialisation when doing some open recursions:

type t =
  | One of t
  | Two of t
  | Three of t

type op =
  { one : op -> (op -> t -> t) -> t -> t;
    two : op -> (op -> t -> t) -> t -> t; }

let rec f op t =
  match t with
  | One x ->
    (op.one [@inlined]) op f x
  | Two x ->
    op.two op f x
  | Three x ->
    Three (f op x)

let one op f x =
  let recursed_one = f op x in
  One recursed_one
  [@@inline]

let two op f x =
  let recursed_two = f op x in
  Two recursed_two
  [@@inline never]

let op =
  { one;
    two }

let identity t =
  (f [@specialised]) op t

In this case, when one is inlined, the call to f is rewritten to a recursive call.

The simple one might be acceptable this late in the release, but the second one is certainly too complicated.

I don't think that the additional substitution is too costly in that case (compared to the two calls to simplify on the expression just after), so I might propose the simple version as a pull request tomorrow (after some cleanup).

@chambart OK, let's see the simple version as a separate pull request, and then we can decide which fix is less risky. I think we need one or the other for 4.04.

@mshinwell I have pushed a first proposition for the 'simple' solution. It might be a bit too much for a change this late in the release.

We think this is going to be superceded by #780