Incoherence

[Jeffrey R Lewis]

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