I'd imagine that in this context (i.e. one where a 1-arity function initializes a tail-recursive 2-arity function) the 1-arity function is the only one that'd be exposed outside of the module, in which case you can know with reasonable certainty that only things within the current module will ever call it.

If you really do need to export the 2-arity version, you could always do a meaningless addition to force it to typecheck to a number, like so:

    count([], C) -> C+0;
    count([_|T], C) -> count(T, C+1);

Which should then result in the following:

    erl> c(test_count).
    {ok,test_count}
    erl> test_count:count([], bang).
    ** exception error: an error occurred when evaluating an arithmetic expression
         in function  test_count:count/2 (test_count.erl, line 8)

Or alternately, use guards (though in the context of BEAM-level introspection I haven't the slightest idea if this would produce an equivalent check):

    count([],    C) when is_integer(C) -> C;
    count([_|T], C) when is_integer(C) -> count(T, C+1);

Which then gets you a somewhat clearer error message:

    10> c(test_count).
    {ok,test_count}
    11> test_count:count([], bang).
    ** exception error: no function clause matching test_count:count([],bang) (test_count.erl, line 8)

Yes, if you look at my reply to the sibling comment, you'll see that if count/2 is unexported, TypEr (apparently, that's the proper capitalization) infers the types with non_negative_integer().

In fact, I've just looked at the original TypEr paper [0], and wow, they use exactly this example in the section 6: "One might even jump to the conclusion that success typings are unnecessarily general and, as such, quite useless. However, notice that this success typing succinctly captures all possible applications of length_3 which will not result in a type error. [...] Still, we also find the situation sub-optimal and we will improve on it as explained below", and then they use exactly your proposal, recognizing that non-exported functions are only called from the exported functions, and perform dataflow analysis to constrain the types even further.

[0] Tobias Lindahl and Konstantinos Sagonas, "Practical type inference based on success typings", https://www.it.uu.se/research/group/hipe/dialyzer/publicatio...

Yeah, I mean that it will properly identify that the only time you can do that is when you have an empty list. The final spec will be (in elixir syntax):

    (nonempty_list, number -> number) | ([], any -> any)

It should also be able to correctly infer that the count/1 function must be

    (nonempty_list -> pos_integer) | ([] -> 0)

I am using an old version of erlang, so typer infers the following types:

    -spec count([any()],_) -> any().
    -spec count([any(),...]) -> any().

If I unexport count/2, it infers

    -spec count([any(),...]) -> non_neg_integer().
    -spec count([any()],non_neg_integer()) -> non_neg_integer().

I did say "should be able to" without regard to any of the existing type inference engines =D I'll be sure to make this as explicit test in Mavis Inference, which is the one I'm working on. https://github.com/ityonemo/mavis_inference/issues/47