TRMC across GADT packing

Learning
1

I recently ran into a situation with packed GADTs where technically TRMC is implementable, but I’m not sure if it’s doable with the features OCaml currently provides. Here’s a simplified example:

module List_with_length = struct
  type ('a, 'length) t =
    | [] : ('a, unit) t
    | (::) : 'a * ('a, 'length) t -> ('a, unit * 'length) t

  type 'a packed = T : ('a, _) t -> 'a packed [@@unboxed]

  (* [of_list] can return any length, so we need to return a packed version.
     This seems to mean that I cannot use TMRC.
   *)
  let rec of_list (list : 'a list) =
    match list with
    | [] -> T []
    | hd :: tl ->
      (match of_list tl with
       | T tl -> T (hd :: tl))
  ;;
end

Because packed is unboxed, from a runtime, post type-erasure perspective, this is a classic case TRMC. But because of the packing, I have to match on the recursive call, which means the call is no longer in the tail position. Is this doable? If not should we look into adding support for this specific pattern into the compiler (treat a match on a recursive call where the result of the match is a single branch whose expression is TRMC constructible as a tail call)?

2

Have you tried ? Add the TRMC annotation and check the resulting assembly.

I worked on extensions to TRMC a while ago, but I never touched the implementation that is in the actual compiler. It might be that this could “just work” if the optimisation is late enough and that the proper transformations are made.

There is most likely no difference, but since your match has one branch you could also try let T tl = of_list tl

3

Yes I did try and it complains that it’s not a tail call (even if an annotation is added). And let doesn’t work either. I also looked at the generated lambda, and let and match compile down to the same code.

4

This is a known limitation of the current implementation of the TRMC transformation, which is purely syntactic: OCaml - The “Tail Modulo Constructor” program transformation. In particular, let-bound calls are not eligible to TRMC optimization.

Cheers,
Nicolas

5

Is this worth adding?

6

Improvements are always welcome :slight_smile:

Cheers,
Nicolas