Incoherence

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