John: just to check, you do realise that (B) means a) That adding a type signature can change the dynamic semantics of the program. This would be the first and only occurrence of such behaviour. At present, adding a type signature changes both the static semantics and the cost of running a program -- one should already understand that a type signature with a non-empty context means the expression is evaluated at its uses rather than at its definition. Given that one understands that, and that an expression which uses an implicit parameter will have a type signature which explicitly indicates that, I don't think this is really such a big deal. b) That whether or not a definition is unconditionally inlinable at the source-language level cannot be determined by looking at the expression. You have to do something rather like effects analysis: look to see if it calls any function (transitively) that uses an implicit parameter. These seem like pretty dire properties. Are you sure it's worth it? Simon Are you sure this second one really holds? I claim the effects analysis is just type inference! If the expression has a context referring to an implicit parameter, then it cannot be unconditionally inlined -- it's as simple as that, isn't it? Admittedly, this really only solves the problem for the compiler -- the poor programmer may have more trouble doing type inference in his head. (How much easier life would be with = for call-by-name, := for call-by-need...) So maybe not so dire as you made out! John