Re: RULE traverse = traverse_?

On Tue, 31 Mar 2015, Joachim Breitner wrote:

At a first glance, the rule "traverse == traverse_" seems to be sound where the resulting program well-typed, as if it is well-typed in both cases, this means that the result was not used.

Of course, an explicit "traverse_" is still useful, but wouldn’t it nevertheless be nice to have a sufficient smart compiler?

If it works it will still surprise programmers if the magic does not happen for a custom function similar to 'traverse'. E.g. I had a data structure with two type parameters and thus two traverse function parameters. I think it is better to tell programmers about the general problem instead of fixing a selection of instances.