On Wed, 18 Feb 2004, Daan Leijen wrote:
choose :: a -> a -> a choose x y = x
What is the type of "choose id" if your system is impredicative? Either "forall a. (a -> a) -> (a -> a)" or "(forall a. a->a) -> (forall a. a->a)" Note that neither of these types subsumes the other.
This is bad, but it doesn't seem any worse than what we've got already in GHC and Hugs. In fact, what we've got is much worse: not only can't we infer most general types, we can't even determine the meaning of a correct program without looking at explicit type signatures.
Anyway, Ben Rudiak's particular case, namely instantiating arguments of a type with type schemes, is difficult due to another problem. It is very hard to know whether an argument to a type is used contra-variantly or co-variantly (or both, or not at all).
I noticed that problem but didn't think about the difficulties of type constructor parameters. It seems like you could make this work by extending the kind system, but maybe it's not worth it. -- Ben