Yep, type checking clearly can't be decidable, since the type system is turing complete.

Imo inference is a bit overrated anyway. I find annotations to be very useful.

There's a series of steps here:

- "Static type annotations are too verbose, dynamic languages allow you to avoid the ceremony." - "But Hindler Milner type systems can infer the types, so you usually don't have to write the type annotations!" - "Writing type annotations is useful anyway, because it serves as valuable documentation, makes reasoning about the program easier, and results in more useful type errors."

Thinking about it more now, there's another step: - "If you have good type inference, you can use editor tooling (eg the LSP) to automatically insert the type signatures for you!"

Top level type annotations in Haskell are very helpful, but with no type inference, you would also have to annotate every intermediate term in the program, which would be intolerable. Remember that the programs are essentially typed lambda calculus, so every term must have a type. Normally you let the compiler figure out all or almost all of the types.

Part of the usefulness of top level annotations in Haskell is that if your program has a type error, inference can fail in multiple ways. I.e. the unification algorithm might assign type T to your function F and chug along happily until it runs into a conflict in some unrelated part of the program, then throw an unhelpful error message in the case where T wasn't the type that you intended for F. By annotating F with the type you really want, you get an error message that does a better job pinpointing the problem.

This is less of an issue in ML, since ML's type system is less general than Haskell's, so the inference algorithm can't go as crazy, and you usually get good error messages even without annotations.

Yeah, I definitely wouldn't want to argue against having type inference at all. I agree that you don't want to annotate every single local definition (although I'd probably lean towards annotating more often than most).

I'm more saying that I'm fine with type system features that break global inference, as long as there's still local inference that's usually good enough in practice.

Right, but local inference is also complicated. So the question is how much of it Idris manages to do without manual annotations. It's not even limited to local definitions with names. If you fully annotate "a=b+2" you get something like "a:int = a:int +:(int->int->int) 2:int". The compiler makes an expression tree and every node in the tree has to get an annotation, either from the source text (i.e. manually) or through inference.

One of the most important lessons learned by the Haskell community is that we shouldn't worry about whether complete type inference is possible. We should worry about whether type inference can be maintained in the easy cases, while falling back to explicit annotation for the hard cases. All of rank-n types, GADTs, type families, even basic type classes, break complete type inference. The solution has always been to document the limitations, draw as clear a line in the sand as possible, and then go on and introduce those features. This doesn't affect the usability of the language.

What does affect the usability of the language is when (a) the line in the sand isn't very clear from an end-user point of view [see simplified subsumption in GHC 9, for example], or (b) the line is on the wrong side of simple features [see monomorphic local bindings, for example].

I guess what I'm saying is that Idris having minimal type inference is kind of terrible, and the excuse that it's not decidable for dependent types is a flimsy one.