Incoherence

[John Hughes]

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 (:-)?

John Hughes