So, does that mean that ideally we would like it to type check, but for implementation reasons it cannot easily be done without a type signature? I can use the type signature no problem. Keean. Andres Loeh wrote:
Hi there,
The following code should compile (If the constructor is valid, so is the function):
data Test = Test (forall a . a) test a = Test a
However this fails to compile with the following error:
The current implementation of rank-n polymorphism (which is documented in the paper "Pratical type inference for arbitrary-rank types") does not "guess" polymorphic types for lambda-abstracted values.
In this situation, this means that the variable "a" is assumed to have a monorphic type, which then cannot be passed to "Test" as an argument.
Knowledge about polymorphism is passed down/inwards, but not up/outwards.
This definition typechecks only if you add a type signature:
test :: (forall a . a) -> Test
If you want to know the reasons, read the paper. It explains the problems very well.
Cheers, Andres