Claus Reinke wrote:
The point is that the GHC type checker relies on automatic inference. Hence, there'll always be cases where certain "reasonable" type signatures are rejected. .. To conclude, any system with automatic inference will necessary reject certain type signatures/instances in order to guarantee soundness, completeness and termination.
i think Lennart's complaint is mainly about cases where GHC does not accept the very type signature it infers itself. all of which cases i'd consider bugs myself, independent of what type system feature they are related to.
there are also the related cases of type signatures which cannot be expressed in the language but which might occur behind the scenes. all of these cases i'd consider language limitations that ought to be removed.
the latter cases also mean that type errors are reported either in a syntax that can not be used in programs or in a misleading external syntax that does not fully represent the internal type.
in this example, ghci infers a type for foo' that it rejects as a type signature for foo'. so, either the inferred type is inaccurately presented, or there's a gap in the type system, between inferred and declared types, right?
Good point(s) which I missed earlier. Type inference (no annotations) is easy but type checking is much harder. Type checking is not all about pure checking, we also perform some inference, the Hindley/Milner unification variables which arise out of the program text (we need to satisfy these constraints via the annotation). To make type checking easier we should impose restrictions on inference. We (Tom/SimonPJ/Manuel) thought about this possibility. The problem is that it's hard to give an intuitive, declarative description of those restrictions. Martin