Reduce is not inlining an atom

Attempting to compile this file with --core-lint fails with the following error:

external val (+) : int -> int -> int = "function(x, y) return x + y end"

type sz_tree =
  | E
  | T of sz_tree * sz_tree

let rec foldr f zero = function
  | E -> zero
  | T (l, r) -> foldr f (f (foldr f zero r)) l

let _ = foldr (1+) 0 E

+#v161 : (| int#t-2, int#t-2 |) -> int#t-2 = foreign
type sz_tree#t2 {
  E#D3 : sz_tree#t2;
  T#D4 : {_1 : sz_tree#t2, _2 : sz_tree#t2} -> sz_tree#t2
}
let gb#v183 : unit#t-5 =
  let fy#v180 : int#t-2 -> int#t-2 =
    λ (gf#v187 : int#t-2).
      let gg#v188 : (| int#t-2, int#t-2 |) =
        (# 1, gf#v187:[int#t-2] #)
      in +#v161:[(| int#t-2, int#t-2 |) -> int#t-2] gg#v188:[(| int#t-2, int#t-2 |)]
  in let rec             
    foldr_sat#v204 : int#t-2 -> sz_tree#t2 -> int#t-2 =
      λ (zero#v205 : int#t-2).
        λ (x#v206 : sz_tree#t2).
          match x#v206:[sz_tree#t2] {
            (T#D4 gz#v207:[{_1 : sz_tree#t2, _2 : sz_tree#t2}]) [] : sz_tree#t2 ->
              match gz#v207:[{_1 : sz_tree#t2, _2 : sz_tree#t2}] {
                {_1 = l#v209:[sz_tree#t2], _2 = r#v208:[sz_tree#t2]} [] : {_1 : sz_tree#t2, _2 : sz_tree#t2} ->
                  let gk#v216 : sz_tree#t2 -> int#t-2 =
                    (* XXX No such variable zero#v196 *)
                    foldr_sat#v204:[int#t-2 -> sz_tree#t2 -> int#t-2] zero#v196:[int#t-2]
                  in let hj#v217 : int#t-2 =
                    gk#v216:[sz_tree#t2 -> int#t-2] r#v208:[sz_tree#t2]
                  in let hk#v218 : int#t-2 =
                    fy#v180:[int#t-2 -> int#t-2] hj#v217:[int#t-2]
                  in let gk#v219 : sz_tree#t2 -> int#t-2 =
                    foldr_sat#v204:[int#t-2 -> sz_tree#t2 -> int#t-2] hk#v218:[int#t-2]
                  in gk#v219:[sz_tree#t2 -> int#t-2] l#v209:[sz_tree#t2]
              };
            E#D3 [] : sz_tree#t2 ->
              zero#v205:[int#t-2]
          }
  in let ga#v182 : sz_tree#t2 -> int#t-2 =
    foldr_sat#v204:[int#t-2 -> sz_tree#t2 -> int#t-2] 0
  in let gc#v184 : int#t-2 =
    ga#v182:[sz_tree#t2 -> int#t-2] E#D3:[sz_tree#t2]
  in unit

Effectively, in a previous pass we generate a binding let zero#v196 = 0 which should be inlined everywhere, and so the binding is automatically removed. However, somehow we're not visiting all nodes, and so this term isn't inlined everywhere.

amuletml / amulet

Reduce is not inlining an atom #264