Surely we could use *zero* extra identifiers by writing:

(ia) let ?x = foo in bar (iia) bar where ?x = foo

i.e., s/dlet/let/ and s/with/where/ .

I thought this was mentioned at the Haskell Implementors' Meeting.

I believe that is the favoured change amongst those that want change. I've recently come across a new twist in the story though: o let and where have a "letrec" semantics. That is: let x = 1 in (let x=x in x) is an infinite loop because it can be alpha renamed to: let x = 1 in (let y=y in y) o with and dlet have a non-recursive "let" semantics. That is: dlet ?x=1 in (dlet ?x=?x in ?x) has the value 1 because it can be renamed to: dlet ?x=1 in (dlet ?y=?x in ?y) The problem is that if they have the same syntax, then they probably ought to have the same semantics wrt recursive/non-recursive bindings. The semantics of dlet/with is entirely intentional on the part of the designers of implicit parameters. For example, if you use implicit parameters in an interpreter, you can use code like this to extend the environment when processing a let expression: eval (Let v e1 e2) = eval e2 with ?env = (v, eval e1) : ?env (The IP paper has a different example based on pretty-printers but I happen to find this one more compelling since I write code like this all the time.) -- Alastair ps I don't happen to agree with the IP designers but I hope I understand their argument well enough to have given a fair example of why a non-recursive dlet/with is desirable. Apologies if not.