Hello, what about dropping implicit universal quantification of type variables from the language, meaning that every universal quantification has to be made explicit? One advantage of this would be that spelling mistakes in type variables would be detected by the compiler more often since every type variable would need to be “declared” by a forall (or exists). In addition one could think of different semantics for unbound type variables. Such a variable could refer to a quantification at a higher level which would solve the problem of sometimes not being able to give type declarations for let/where declarations. For example, in the following example, the type variable e in the where clause would refer to the same type as the type variable e in the type declaration of the function example: example :: forall e. Enum e => e -> e example = helper where helper :: e -> e helper = succ I know, these would be rather drastic changes but they seem sensible to me. What do others think? Best wishes, Wolfgang