A sound and complete type for Enumerable#inject

Kicking the wheels on RBS, Enumerable#inject seemed a good method to start with. I see its block form as () { (Elem, Elem) -> Elem } -> Elem. Though matching how we usually use #inject, I think it misses cases. Perhaps the correct type is [T] () { (Elem | T, Elem) -> T } -> (Elem | T)?; however, I could still easily be missing something. Let me explain why I think this is a better type as well as my concerns, and please direct me to the proper forum if a GitHub issue is the wrong place to bring this up.

Consider calling #inject on an empty collection. It returns nil rather than an Elem, so I expect (1..0).inject{2} * 3 to type check under the current definition even though the expression raises "NoMethodError: undefined method *' for nil:NilClass"`. In other words, the definition is unsound.

Now consider [1, 2, 3].inject{_1.to_f / _2}. It returns 0.16666666666666666, but I expect a type checker to complain since Elem is an Integer and the block should return an Elem whereas it clearly returns a Float. In other words, the definition is incomplete.

Now suppose we use [T] () { (Elem | T, Elem) -> T } -> (Elem | T)? to type #inject. The question mark accounts for #inject returning nil when the enumerable is empty. Having Elem in the return type accounts for a single element collection that just passes through the element. Otherwise, #inject returns whatever the block returns.

As for the block, it's initially called with the first two elements of the collection. On successive calls the first memo argument will have whatever type the block returned previously, and the second argument will be the next Elem from the enumerable.

So it might be hard to infer T. Take the simpler example [1, 2, 3].inject{_1.to_f}. We can say that T = Float | T.to_f where T.to_f means the result of calling #to_f on an object of type T. But to fully fix T = Float, we need the extra, inductive fact that any call to {_1.to_f} will be the result of a previous call to {_1.to_f}.

Also note that instead of [A] (A initial) { (A, Elem) -> A } -> A, the single argument form of #inject could be [A] (A initial) { (A | T, Elem) -> T } -> (A | T). This form doesn't usually need to handle returning nil.

Start with the Enumerable#inject signature in core/enumerable.rbs referenced by the issue, then examine how RBS represents the block and accumulator types. Compare candidate signatures against the empty, singleton, and changing-accumulator examples; done means reaching an agreed sound and complete type, with corresponding validation for those cases.