Solution to the monomorphism restriction/implicit parameter problem

[Ben Rudiak-Gould]

On Tue, 5 Aug 2003, Simon Peyton-Jones wrote:

> I'm afraid that I have not read all of the recent exciting flood of
> messages carefully,

Hi, I'm glad to see that you're around, and I'm very much looking forward
to any comments you may have about my proposal.


> You say that "All implementations should be changed so that they do the
> right thing".  If only we knew what the Right Thing is!

My solution *is* the Right Thing. :-) It really did exist all along. I
think that once you read and understand my implicit parameter proposal
this will become clear.


> 		Comments from TcSimplify
> 
> Question 3: monomorphism
> ~~~~~~~~~~~~~~~~~~~~~~~~
> There's a nasty corner case when the monomorphism restriction bites:
> 
> 	z = (x::Int) + ?y
> 
> The argument above suggests that we *must* generalise
> over the ?y parameter, to get
> 	z :: (?y::Int) => Int,

No, it's not necessary that z have that type, just that it behave exactly
as though it had that type. The reason the expression

    let f = (<) in (f 'a' 'b', f 'a' 'b')

is not rejected even with the monomorphism restriction turned on is that
there's a monomorphic specialization of f that behaves exactly as the
polymorphic f would have *in this particular expression* -- and that's
what actually gets used.

Similarly, the expression

> 	let z = x + ?y in z+z

need not be rejected, because there's a monomorphic "specialization" of z
that behaves exactly as the polymorphic version would have in this
expression -- namely

    z = (x + ?y) {?y = @y}.

(See my implicit parameter proposal for a definition of the new syntax.)


-- Ben