Thank you for the recommendation. I think I found the paper that introduced the idea: http://www.it.uu.se/research/group/hipe/papers/succ_types.pd...

If I understand correctly, success typing rejects only programs that will lead to a type error at runtime, but allows all programs that it can't prove incorrect. I think that's an interesting idea and definitely better than no type checks at all, but I'd still like to have a type system that can prove some programs to be type safe, if possible.

I agree. Yet I want as much inference as possible as you described upthread