Typing Problems

The question is what problem I am solving by looking at other type inference algorithms.

1. Traditional HM style inference allows for the introduction of non-constructive types.
2. Traditional HM style inference leads to strange awkward fixes such as the monomorphism and value restrictions.
3. Impredicative HM style inference is awkward, I am not convinced that such modalities are needed.
4. Impredicative HM style inference in the general case is undecidable.

I need to elaborate on these points with examples.

1) might be minor. The introduction of non-constructive types might not be a problem since the general excuse for that could be that they cannot be instantiated except with non-terminating terms. Still, I guess the theoretical consequence is that such a type system is inconsistent. I need examples for that.

2) is major. I don't dig the value restriction and think it is nonsense; or rather, a poorly fixed bug of a typing system. Again, I need examples.

3) is just a conjecture.

4) is a major problem though some claim to have solved it.

Question is if and how a shift to type-constructors and constructive types would allow a fix of this. Generalizing what I am doing, I am going for a type system in which universally quantified types like ∀α.∀β. α → β are forbidden but we do allow constructive types such as ∀α.∃f. α → f(α), possibly interpreted as ∀α.∃f.(Λβ → f(β)) α, in the hope that only type arguments need be derived from the term and most 'logical' quantifiers can be used without a real restriction on where they occur in the type and can be dropped/made implicit.

Not sure I am solving any problem here.