Ross Paterson wrote:

I suggest = for bind-by-name, and := for bind-by-need. ...

You're proposing that the =/:= distinction both decides whether constrained type variables are monomorphic and whether the binding should be implemented using sharing. If it only did the former (and the expectation was that all pattern bindings with unconstrained types used sharing), then existing legal programs would still be legal, and the examples that currently trip over the MR would be legal but inefficient. (Also, what does the shared/unshared distinction mean for functions?) Not just constrained type variables. All type variables. Because changes in the program elsewhere can easily change the status of a type variable from unconstrained to constrained, thus triggering monomorphism unexpectedly--that was the point of my comment about introducing an equality test in a function called from the definition. Changing the status of a type variable should not change the way it is treated by any replacement for the M-R. I don't quite follow what you're suggesting above. The main point of a =/:= distinction is to distinguish between sharing and non-sharing, isn't it? And sharing means you have to be monomorphic, at least for constrained type variables, and (by the argument above) thus for unconstrained ones too. How can sharing/unsharing and monomorphic/overloaded be separated? I'd really like to avoid ANOTHER rule that "guesses" what method to use, based on the form of the definition (your reference to pattern bindings above). That leads to surprises for the programmer, at least the less-than-expert one, when a definition is replaced by something that LOOKS equivalent, but type-checking or sharing suddenly behaves differently. Much preferable is a simple and obvious rule: = means unshared and polymorphic, := means shared and monomorphic. Shared/unshared doesn't matter for function definitions, but monomorphic/polymorphic can still be important. There is an interaction with implicit parameters here--which I suppose might make it into Haskell'. A := definition says: resolve all overloading here. Thus, if there is an implicit parameter in the RHS of such a definition, then it refers to the instance of that parameter in scope at the point of definition. With a = definition, it refers to the instance in scope at the point of use. This is an important distinction whether you're defining a function or anything else. This is discussed in my paper on Global Variables in Haskell, which suggested using implicit parameters to refer to global variables, rather than an unsafe unsafePerformIO applied to a newIORef. What if one has mutually recursive bindings, some using = and some := ? Does monomorphism kick in if some of the variables in a binding group use :=, or would we just require that all bindings in the same group use the same binder? (At first I couldn't see why one would ever use := with function bindings, but perhaps that's the reason.) I don't think there's really a problem in allowing a mixture of = and := in the same mutually recursive group, even if it could be quite confusing to do so! = just means that type variables and dictionaries should be abstracted, and that the binding should be by-name... let's assume that we're translating to System F, and we always insert at least a \()-> on such bindings in the translation. := means, on the other hand, that type variables and dictionaries are not abstracted, and so must be inherited from an enclosing scope. So in a group of the form f = ...g... g := ...f... then any type variables in the definition of g must refer to the enclosing scope, which means that they cannot be generalised in the definition of f either (since they are "free in the context"). But if there are type variables in the definition of f which do NOT occur in the type of g, then they can be generalised as usual. Meanwhile f can be bound by name, and g by need--there's no difficulty with that. This would be an odd thing to do, but I think it makes perfect sense. (I wonder what happens today, if you write mutually recursive definitions where the M-R applies to some, but not others?) Of course, polymorphic recursion would REQUIRE an = binding, but that shouldn't surprise anybody. John