Incoherence

[John Hughes]

	John Hughes wrote:

	> I noticed today that the presence or absence of a type signature can
	> change the RESULT of an expression in Hugs and GHC nowadays. Here's an
	> example:
	>
	>     a = (let x = ?x in
	>          x with ?x = 1)
	>         with ?x = 2
	>     -- a == 2
	>
	>     b = (let x :: (?x :: Integer) => Integer
	>              x = ?x in
	>          x with ?x = 1)
	>         with ?x = 2
	>     -- b == 1
	>
	> It's the infamous monomorphism restriction at work, again, of course. Now,
	> what are the proof rules for reasoning about implicit parameters again (:-)?

	As you observed, the dreaded monomorphism is at work here, and that's
	where the problem lies, not really with implicit parameters.  It has
	been proposed that implicitly parameterized definitions not be subject
	to the monomorphism restriction, precisely to avoid the problem you
	highlight, but this unpleasantly makes the monomorphism restriction
	even more clumsy.  The best solution is to find a good way to
	eliminate the DMR.

	--Jeff

Turning off the MR for definitions with implicit parameters wouldn't really
be a good solution either. Observe that you may WANT the behaviour of the
first example! Suppose you want to change the value of an implicit parameter
in a subexpression, but nevertheless refer to the enclosing value of the
parameter there. It's natural to write

	  let oldx = ?x in (...?x...oldx... with ?x = newx)

which does indeed make the enclosing value of ?x available in the body...
PROVIDED the MR applies to the definition of oldx! Without the MR, you can't
regain this behaviour with any type signature: declaring x to be Integer in
the examples above leads to a type error (maybe it shouldn't?).

What we need is different binding syntax for monomorphic and polymorphic
bindings. Roll on := and = ...

John