suggesting that the same arithmetic expression is both 1 and 0.
In GHC, there is a dedicated flag to spot such cases (-fwarn-type-defaults).
In general, the guarentees that the type system actually gives and also the ways to specify them appear somewhat unfinished and are also quite hard to understand, often necessitating semantic restrictions and syntactic extensions. For further examples, see for instance:
They’re not the same expression though. The first gets defaulted to Integer, the second is specialized to Int by the (!!) function. (Integer is unbounded, Int is bounded)
The rest of your argument is fairly vague and unspecific. But I would suggest trying to understand the underlying type theory instead of focusing on the affordances that the type system makes for practicality and usability concerns. In my experience that makes it a lot clearer why the type inference works the ways it does in some of the weird cases. (That’s not to say that Haskell doesn’t have it’s warts..)
