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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
