What are the strongest known type systems for which inference is decidable?

It's well known that Hindley–Milner type inference (the simply-typed $\lambda$-calculus with polymorphism) has decidable type inference: you can reconstruct principle types for any programs without any annotations.

Adding Haskell-style typeclasses seem to preserve this decidability, but further additions makes inference without annotations undecidable (type families, GADTs, dependent-types, Rank-N types, System $\omega$, etc.)

I'm wondering: what is the strongest known type system with completely decidable inference? It's going to lie somewhere between Hindley–Milner (completely decidable) and dependent-types (completely undecidable). Are there aspects of DTs which can be added which preserve inference decidability? What research has been done to see how far this can be pushed?

I realize that there is not a single strongest system: that there are likely infinite small, incremental changes that can be added to HM keeping inference. But there are likely a few practical candidates of systems that have been discovered.

Edit: given that there is no "strongest" system, I will accept an answer that outlines the notable systems that extend Hindley–Milner with decidable inference. Examples could be Liquid Types, Rank-2, etc.

[EDIT: Voilà a few words on each]

There are several ways of extending HM type inference. My answer is based on many, more or less successful, attempts at implementing some of them.
The first one I stumbled upon is parametric polymorphism. Type systems trying to extend HM in this direction tend toward System F and so require type annotations. Two notable extensions in this direction I came across are :

-
HMF, it allows type inference for all System-F types, which means that you can have universal quantification "in the middle" of a type, their appearance is not implicitly situated at the highest scope like for HM polymorphic types. The paper clearly states that no clear rule exists as to how many and where type annotations may be needed. Also the types being those of System F, terms usually don't have a principal type.

-
MLF is not only an extension of HM, it's also an extension of System F that regain the principal type property of HM by introducing a kind of bounded quantification over types. A comparison has been made by the authors, MLF is strictly more powerful than HMF and annotations are only required for parameters used polymorphically.

Another way of extending HM is through variation of the constraint domain.

-
HM(X) is Hindley-Milner parameterised over a constraint domain X. In this approach, HM algorithm generates the constraints that are sent to a domain solver for X. For the usual HM, the domain solver is the unification procedure and the domain consists of the set of terms build from the types and the type variables.

Another example for X could be constraints expressed in the language of Presburger arithmetic ( in which case type inference / checking is decidable ) or in the language of Peano arithmetic ( no longer decidable ). X varies along a spectrum of theories, each with its own requirements regarding the amount and localisation of type annotations needed and ranging from not at all to all of them.

-
Haskell's type classes are also a kind of extension of the constraint domain by adding type predicates of the form MyClass(MyType) ( meaning that there exists an instance of MyClass for the type MyType ).

Type classes preserve type inference because they are basically an (almost) orthogonal concepts they implements adhoc polymorphism.

As an example, take a symbol val of type val :: MyClass a => a for which you can have instances MyClass A, MyClass B etc. When you refer to that symbol in your code, it's actually because type inference is already performed that the compiler can infer which instance of the class to use. This means that the type of val depends on the context in which it is used. That's also why running a single val statements leads to an ambiguous type error : the compiler can't infer any type based on the context.

For more advanced type systems like GADTs, type families, Dependent types, System (F)ω, etc., type are not anymore "types" they become complex computational objects. For example it means that two types not looking the same are not necessarily different. So type equality becomes not trivial ( at all ).

To give you an example of the actual complexity let's consider the dependent type of list : NList a n where a is the type of objects in the list and n is its length.

The append function would have type append :: NList a n -> NList a m -> NList a (n + m) and the zip function would be zip :: NList a n -> NList b n -> NList (a, b) n.

Imagine now we have the lambda \a: NList t n, b: NList t m -> zip (append a b) (append b a). Here the first argument of zip is of type NList t (n + m) and the second of type NList t (m + n).

Almost the same, but unless the type checker knows that "+" commutes on natural numbers, it must reject the function because (n + m) is not literally (m + n). It's no longer about type inference / type checking, it's about theorem proving.

Liquid types seem to be doing some dependent type inference. But as I understand it, it's not really dependent type, more something like usual HM types on which additional inference is made to compute static bounds.

I hope this helps.

StackExchange Computer Science Q#44054, answer score: 7